From: Thomas Walker Lynch Date: Tue, 18 Aug 2026 12:28:31 +0000 (+0000) Subject: . X-Git-Url: https://git.reasoningtechnology.com/%28%5B%5E?a=commitdiff_plain;h=ea0a95ab63a716bfa13341cc639900d25437caa2;p=TM-2026 . --- diff --git a/document/book/TM-2026.html b/document/book/TM-2026.html index 3214c22..c1adab3 100644 --- a/document/book/TM-2026.html +++ b/document/book/TM-2026.html @@ -51,6 +51,17 @@

All communication builds upon a foundation of common knowledge, so let us begin by searching for some common ground.

+ + Fields of study + +

Number Theory consists of the analysis of Peano Number related structures. It gives properties to these structures, e.g. the familiar 'odd' and 'even'. It gives properties to the relationship between numbers and operations on those numbers, e.g. proving that an odd number squared is odd. It deals with the solution of mixed integer equations, and systems of such equations, and sets the rules for modulus arithmetic. For example, encryption algorithms belong to Number Theory.

+ +

Numerical Analysis is built on two axioms. The first axiom limits computing to vectors of Peano Numbers, where a vector represents a number. A common representation is a number pair, where one number of the pair scales the other number, thus making it possible to represent fractional values. The second axiom states the actual intention of the programmer is to perform computation over a Real field. As Real Numbers fall on a continuum, it follows that some Real Numbers can not be represented with a vector of Peano Numbers. The objective of Numerical Analysis is then to establish the relationship between Peano Number results with the corresponding exact Real Number results. The difference between the two is called error. People who work in numerical algorithm design often spend a great deal of time trying to keep some metric of error low over a given domain.

+ +

Computation Theory consists of proofs over what can, and cannot be computed, the time and space complexity of algorithms, and the fundamental structure of computation. Number Theory is a kind of Computation Theory applied to Peano Structures before Church, Turing, and their contemporaries gave computation theory its name.

+ + + Notation @@ -105,200 +116,229 @@

Dates and times are given in the ISO 8601 format. The components run from the most-significant to the least-significant, year, then month, then day, in the same order the digits of a Hindu-Arabic numeral run. Two consequences follow from that ordering, and both are the reason for choosing it. A lexicographic comparison of two such dates agrees with their chronological comparison, so a list of them sorts correctly with no collation rules particular to dates. And the format is unambiguous, whereas a date such as 03/04/2026 is read as the third of April by some readers and the fourth of March by others. A time of day, when one is given, follows the date, and a trailing Z marks the time as UTC. Hence 2026-06-01 08:28:00Z. ISO 8601 itself separates the date from the time with a T, which is difficult to read. RFC 3339 anticipates the objection and permits a space in its place, and that is the option taken here.Graham Klyne and Chris Newman, Date and Time on the Internet: Timestamps, RFC 3339, July 2002, §5.6. Where a date appears without a time, the date alone is intended, e.g. 2026-06-01. As per the standard, if the day is not to be specified, it is simply dropped, e.g. 2026-06.

 - - Number types + + Symbol and binding -

Several words in this book carry a formal definition that displaces their ordinary English sense, and those are capitalized: Peano Number, Integer, Rational, Real. The word real is the best example of why this is done. It was too much of an ask by mathematics to take a common English adjective and hold it to a technical meaning, and a reader is entitled to know which sense is in play. So a Real is the object mathematics defines, and a real problem or a real difficulty is the ordinary English word. Integer suffers no such ambiguity. It is capitalized for consistency with its siblings.

+

A math object is anything mathematics is willing to name: a number, a set, a function, a formula, or a symbol. Nothing further is meant by it. A value, where the term is used without qualification, is synonymous with math object.

-

The leading capital letter on the mathematical number types does not distinguish the classical notion from the one constructed herein, because this book denies that the two are distinct in the first place. A Real is a Real whether a mathematician defines it or a machine produces the definition.

+

A symbol is a designated math object, where each symbol is distinct from every other symbol, and such that each symbol can be represented. We don't write down a symbol directly. What a person sees on a piece of paper, or on the computer screen, is an instance of a symbol representation. Most mathematicians prefer to represent each symbol using a single letter of the English, Greek, or sometimes some other alphabet. Mathematicians don't often use the terminology of representation and instance, but might instead refer to an instance of a symbol representation as a sign, a letter, or a mark.Philosophy calls this the distinction between a type and its tokens, following Peirce. The fit is close but not exact, as that pair has no middle layer answering to what is here called a representation. Charles S. Peirce, Collected Papers, vol. 4, §537. Chapter takes up this topic in more detail.

-

What mathematics calls the natural numbers are called Peano Numbers in this book. A Peano Number is what a Peano Machine outputs. This convention frees the word 'Natural' to refer to the philosophy only, so a reader never has to work out which of the two is meant. Note that herein Peano Numbers are taken to begin at zero, while Counting Numbers begin at one, and the two are not the same.Peano's own axioms began at one. Modern presentations of Peano arithmetic begin at zero, and that is the convention followed here. Giuseppe Peano, Arithmetices principia, nova methodo exposita (Turin: Bocca, 1889), §1. An Integer, a Rational, and a Real are likewise the outputs of machines, each constructed in its turn.

- +

An evaluation context is a situation held still. A step of a procedure is an evaluation context, and so, for example, step 1, step 2, etc. are separate evaluation contexts. In a system carrying time, each interval between one event and the next is a context, and events occurring simultaneously belong to the same evaluation context. The example most applicable to this section is that a quantifier running a symbol over a collection gives one context per value it runs over.

- - Fields of study +

A math context is a proof, an algorithm, or a math problem taken as a whole. It is the set of all the evaluation contexts belonging to that proof, algorithm, or problem.

-

Number Theory consists of the analysis of Peano Number related structures. It gives properties to these structures, e.g. the familiar 'odd' and 'even'. It gives properties to the relationship between numbers and operations on those numbers, e.g. proving that an odd number squared is odd. It deals with the solution of mixed integer equations, and systems of such equations, and sets the rules for modulus arithmetic. For example, encryption algorithms belong to Number Theory.

+

The definitions that follow compare what holds in one evaluation context against what holds in others, so each is stated over a set of evaluation contexts. That set need not be the whole of a math context. A narrower interest selects a few of them, while a class of math contexts, a proof form being one such class, gathers them from every math context of the class. Both are legitimate, and either changes what the definitions below report. This section takes the set to be the math context throughout, and says so here rather than at each definition.

-

Numerical Analysis is built on two axioms. The first axiom limits computing to vectors of Peano Numbers, where a vector represents a number. A common representation is a number pair, where one number of the pair scales the other number, thus making it possible to represent fractional values. The second axiom states the actual intention of the programmer is to perform computation over a Real field. As Real Numbers fall on a continuum, it follows that some Real Numbers can not be represented with a vector of Peano Numbers. The objective of Numerical Analysis is then to establish the relationship between Peano Number results with the corresponding exact Real Number results. The difference between the two is called error. People who work in numerical algorithm design often spend a great deal of time trying to keep some metric of error low over a given domain.

- -

Computation Theory consists of proofs over what can, and cannot be computed, the time and space complexity of algorithms, and the fundamental structure of computation. Number Theory is a kind of Computation Theory applied to Peano Structures before Church, Turing, and their contemporaries gave computation theory its name.

- - - - - Logic - -

A symbol is an abstract concept, of which the following will hold: each symbol exists as a singular entity, it is distinct from every other symbol, it can be represented, and multiple recognizable instances can be made of the representation. We don't write down the symbol directly. What we see on a piece of paper, or on the computer screen, is a representation of the symbol. A symbol doesn't require a representation, though when it has one, there can be many instances of it, and every instance must be recognizable as being of that symbol and of no other. Most mathematicians prefer a single letter of the English, Greek, or sometimes some other alphabet as a symbol representation. Then, within a math context, it is quite easy to recognize when multiple symbol representation instances represent the same symbol. In a math article a symbol instance might be called a sign, a letter, or a mark. Philosophy calls this the distinction between a type and its tokens, following Peirce. The fit is close but not exact, as that pair has no middle layer answering to what is here called a representation. Charles S. Peirce, Collected Papers, vol. 4, §537.

+

A constant is a value that is the same in every evaluation context of a math context.

-

A proposition is a statement that is given no arguments and carries a truth value, that being one of exactly two things, written true and false. A proposition is not predicated upon anything, so settling it requires nothing to be looked up and no value to be supplied. "The moon is made of green cheese" is a proposition, and it is false. "Seven is prime" is a proposition, and it is true. In either case the statement stands complete as it is written. Nothing in the calculus that follows looks inside a proposition or has any means of altering one. A proposition enters the calculus carrying its truth value, and the calculus makes use of nothing else about it.

+

A symbol can be bound to any value, including another symbol. This binding can be expressed as a predicate, bind(s, v), where s is the symbol and v is the value it is bound to. Chapter discusses binding in more detail.

-

The connectives are symbols, and instances of their representations are these: ∧ (and), ∨ (or), ¬ (not), → (implies), and ↔ (if and only if). Alongside them stand the parentheses, ( and ), which group. Each connective is fixed, in that what it does is settled once for the whole calculus and nothing later on is at liberty to change it. What each one does is combine truth values to give a truth value, so ∧ gives true exactly when both of the truth values given to it are true, ¬ gives the truth value it was not given, and so on for the rest.

+

Within an evaluation context a symbol is in one of two binding states: it is bound to a value, or it is unbound. Comparing those states across a math context sorts the symbols of that context into three cases. Where a symbol is bound to the same value in every evaluation context, its binding is a constant, and the symbol is a fixed symbol. Where a symbol is bound to different values in different evaluation contexts, or is bound in some and unbound in others, it is a variable. Where a symbol is unbound in every evaluation context, it is purely symbolic. This third case is not resolved into the other two by the math context, since a symbol that nothing binds and a variable that nothing happened to bind look alike within it, and telling them apart is a matter for the wider set.

-

Beside the connectives stand the proposition symbols. Common examples of their representations include p, q, and r. A proposition symbol has no meaning of its own. It marks a place where a proposition is later supplied, and it is the only thing in this calculus that awaits anything.Many texts call these propositional variables. The word 'variable' is reserved in this book for a symbol that a quantifier is able to claim, and the propositional calculus holds no quantifier that could claim anything. The case of the representing letter follows the notation convention of section , applied to whatever the symbol marks a place for: a proposition is not a container, so the letter is lower case, while a formula is a string and therefore a container, so the letters standing for formulas below are capitals.

- -

Symbol instances are strung together according to the formation rules, and what the rules build is called a formula. The rules are three, and the third is what closes the definition. The Greek letters Φ and Ψ are used below to represent whole formulas. They belong to this discussion rather than to the calculus being discussed.

+ - - -
    -
  1. A proposition symbol standing alone is a formula. Such a formula is called atomic, meaning the formation rules cannot break it down further.
    2. -
  2. If Φ and Ψ are formulas, then ¬Φ is a formula, and so is (Φ ∘ Ψ) for each binary connective ∘.
    3. -
  3. Nothing is a formula except by finitely many applications of rules 1 and 2.
    4. -
- List . Formation rules of the propositional calculus - + + Number types -

For example, (p ∧ ¬q) is a formula. Rule 1 supplies the base of the construction and rule 2 supplies the negation, ¬q, then rule 2 applied again supplies the connective, p ∧ ¬q. In this example rule 2 is applied a third time to place the parenthesis. Rule 3 then terminates the process by saying nothing more can be added. Every formula arrives through this same method.

+

Several words in this book carry a formal definition that displaces their ordinary English sense, and those are capitalized: Peano Number, Integer, Rational, Real. The word real is the best example of why this is done. It was too much of an ask by mathematics to take a common English adjective and hold it to a technical meaning, and a reader is entitled to know which sense is in play. So a Real is the object mathematics defines, and a real problem or a real difficulty is the ordinary English word. Integer suffers no such ambiguity. It is capitalized for consistency with its siblings.

-

A computer scientist would see the formation rules as forming a grammar. However, a parser can reject a string while issuing syntax errors. Thus a parser would create two categories, that for a well formed formula, and that for a malformed formula. Take for example the string p ¬ ∧ q. It would not parse. A logician would point out this string is not a result of applying the formulation rules so it is simply not a formula at all. Yet the traditional term used by logicians for a formula is well formed formula, shortened to wff, and along with formula all three terms are used interchangeably, so the adjective well formed creates an implication of the existence of its opposite, just ask Hegel. Of all people, a person would think that logicians would have noticed this. Herbert B. Enderton, A Mathematical Introduction to Logic, 2nd ed. (San Diego: Harcourt/Academic Press, 2001), §1.1, which introduces the three words as alternatives for one thing. Texts that keep the adjective and texts that drop it are describing the same objects.A C++ committee borrowed the terminology for a well formed program but then found it necessary to define a term for the a not well formed program, which became the ill formed one.ISO/IEC 14882, §1.3, which pairs the two definitions: a well-formed program is one constructed according to the syntax rules, the diagnosable semantic rules, and the One Definition Rule, and an ill-formed program is one that is not well formed.

+

The leading capital letter on the mathematical number types does not distinguish the classical notion from the one constructed herein, because this book denies that the two are distinct in the first place. A Real is a Real whether a mathematician defines it or a machine produces the definition.

-

An interpretation supplies what each proposition symbol lacks. It gives every proposition symbol of a formula a proposition. Since each connective combines truth values and inspects nothing else, an interpretation carries no more information than the truth value each supplied proposition holds, and the formula then holds or fails according to those truth values alone. Let p be given "the clock line is high" and q "the enable line is high"; whether (p ∧ ¬q) holds follows from those two truth values and from nothing else. Note what an interpretation does not do. It does not alter the formula, which was fixed before any interpretation was considered, and it does not reach inside a proposition, which was settled before it was supplied.

+

What mathematics calls the natural numbers are called Peano Numbers in this book. A Peano Number is what a Peano Machine outputs. This convention frees the word 'Natural' to refer to the philosophy only, so a reader never has to work out which of the two is meant. Note that herein Peano Numbers are taken to begin at zero, while Counting Numbers begin at one, and the two are not the same.Peano's own axioms began at one. Modern presentations of Peano arithmetic begin at zero, and that is the convention followed here. Giuseppe Peano, Arithmetices principia, nova methodo exposita (Turin: Bocca, 1889), §1. An Integer, a Rational, and a Real are likewise the outputs of machines, each constructed in its turn.

+ -

A propositional calculus therefore consists of math objects that occur on an abstraction stack, which collects what has been said so far.

- - -
    -
  1. interpretation -
      -
    • supplies a proposition, and so a truth value, for each proposition symbol
      • -
    -
    2. -
  2. formula -
      -
    • built from the level 0 symbols by the formation rules
      • -
    -
    3. -
  3. symbol -
      -
    • fixed: connective, parenthesis
      • -
    • awaiting an interpretation: proposition symbol
      • -
    -
    4. -
- List . The propositional logic abstraction stack - + + Logic -

Each level is settled without reference to the one above it. The symbols at level 0 are fixed before any formula is written, the formula at level 1 is an arrangement of them and is fixed before any interpretation is considered, and the interpretation at level 2 supplies what the symbols were marking places for. Nothing at a lower level is disturbed by what happens above it, which is why the same formula serves under every interpretation and the same symbols serve in every formula. Computer science people would call the items at level 0 primitive. Hardware designers might think of them as being native, because they are built into the system, and would recognize the level 1 formula as a gate network drawn before any signal has been applied to it.

+ + + The propositional calculus -

Now suppose that a proposition could be predicated on something else. A predicate is a logic function. It is given values for its arguments, and it then evaluates to true or to false. Give a predicate its arguments and what results is a proposition, so the predicate is the general case and the proposition is the settled one. Prime(x) is a predicate of one argument, and Prime(7) is true while Prime(8) is false. LessThan(x ,y) is a predicate of two arguments, which is how a relation is written. The arguments are drawn from a domain, a set holding at least one member, and that set is whatever mathematics cares to name: the Peano Numbers, the points of a plane, the strings over an alphabet. The arguments are not themselves truth values. Only the result of the predicate is a truth value.

+

A proposition is a statement that is given no arguments and carries a truth value, that being one of exactly two things, written true and false. A proposition is not predicated upon anything, so settling it requires nothing to be looked up and no value to be supplied. "The moon is made of green cheese" is a proposition, and it is false. "Seven is prime" is a proposition, and it is true. In either case the statement stands complete as it is written. Nothing in the calculus that follows looks inside a proposition or has any means of altering one. A proposition enters the calculus carrying its truth value, and the calculus makes use of nothing else about it.

-

The first-order predicate calculus also begins with expressions of symbols, and its base level holds three groups rather than two. The fixed group gains the quantifiers, ∀ (for all) and ∃ (there exists), alongside the connectives and parentheses already in it. The awaiting group, whose members each mark a place for something an interpretation later supplies, now holds three kinds of symbol: the predicate symbol, written F, G, R, which carries a fixed number of argument places and marks a place for a predicate of that many arguments; the name, written a, b, c, which marks a place for one member of the domain; and the function symbol, written f, g, s, which carries a fixed number of argument places and marks a place for a function carrying that many domain members to one domain member. The third group is new. A variable is a symbol that a quantifier is able to claim, and this calculus has one kind, the domain variable, written x, y, z.Many texts call the p, q, r of the propositional calculus propositional variables. This book keeps 'variable' for a symbol a quantifier is able to claim, and the propositional calculus holds no quantifier that could claim anything, which is why those symbols were not called variables above. The proposition symbol is gone, having no work left to do: a predicate symbol given its arguments occupies the place where a proposition once stood.

+

The connectives are symbols, and instances of their representations are these: ∧ (and), ∨ (or), ¬ (not), → (implies), and ↔ (if and only if). Alongside them stand the parentheses, ( and ), which group. Each connective is fixed, in that what it does is settled once for the whole calculus and nothing later on is at liberty to change it. What each one does is combine truth values to give a truth value, so ∧ gives true exactly when both of the truth values given to it are true, ¬ gives the truth value it was not given, and so on for the rest.

-

A function applied to domain members yields another domain member, so the expressions that mark out a member of the domain have to be settled before the formulas can be. A term is a domain variable, or a name, or a function symbol of n places applied to n terms, and nothing else is a term. A term marks out a member of the domain and carries no truth value of its own. So x, a, and f(s(a) ,x) are terms.

+

Beside the connectives stand the proposition symbols, whose representations are commonly p, q, and r. These are variables. A proposition symbol has no meaning of its own, and marks a place where a proposition is later bound to it. It is the only kind of symbol in this calculus that is not fixed.The letters follow the notation convention of section , applied to whatever the symbol marks a place for. A proposition is not a container, so the letter is lower case. A formula is a string and therefore a container, so the letters standing for formulas below are capitals.

- - -
    -
  1. A predicate symbol of n places applied to n terms is a formula, and it is atomic.
    2. -
  2. If Φ and Ψ are formulas, then ¬Φ is a formula, and so is (Φ ∘ Ψ) for each binary connective ∘.
    3. -
  3. If Φ is a formula and x is a domain variable, then ∀x \, Φ and ∃x \, Φ are formulas.
    4. -
  4. No expression is a formula except by finitely many applications of rules 1 through 3.
    5. -
- List . Formation rules of the first-order predicate calculus - +

Symbol instances are strung together according to the formation rules, and what the rules build is called a formula. The rules are three, and the third is what closes the definition. The Greek letters Φ and Ψ stand for whole formulas below, and ∘ stands for any one of the binary connectives. All three belong to this discussion rather than to the calculus being discussed.

-

So ∀x \, F(x) and ∀x ∃y \, R(x ,y) are formulas of the calculus.

+ + +
    +
  1. A proposition symbol standing alone is a formula. Such a formula is called atomic, meaning no formation rule builds it out of smaller formulas.
    2. +
  2. If Φ and Ψ are formulas, then ¬Φ is a formula, and so is (Φ ∘ Ψ) for each binary connective ∘.
    3. +
  3. Nothing is a formula except by finitely many applications of rules 1 and 2.
    4. +
+ List . Formation rules of the propositional calculus + -

A quantifier claims the domain variable written after it, and its claim reaches over the formula that rule 3 was applied to and no further. That formula is the quantifier's scope. Where a variable appears within the scope of a quantifier claiming it, that appearance is bound; where it appears within no such scope, that appearance is free.The words bound and free are the standard ones, and are given here so that a reader can find the literature. The word claims is used alongside them in this book because it names the agency, which is what the reader needs to see. A bound appearance is spoken for, and nothing supplies it a value, because the quantifier is what runs it over the domain, passing the formula over every member in the universal case and over at least one member in the existential case. A free appearance is left for an interpretation to supply. There are these two fates and no third, and no appearance meets both.

+

For example, (p ∧ ¬q) is a formula. Rule 1 supplies p, and supplies q. Rule 2 applied to q supplies the negation, ¬q. Rule 2 applied again, this time to the pair, supplies (p ∧ ¬q), and the parentheses arrive with that application rather than by any step of their own, because the rule writes them. Rule 3 then terminates the process by saying nothing more can be added. Every formula arrives through this same method.

+ +

A computer scientist would see the formation rules as forming a grammar, and a parser built from them would sort strings into two categories, the well formed formula and the malformed formula. Take the string p ¬ ∧ q, which would not parse. A logician would point out that this string is not a result of applying the formation rules, so it is simply not a formula at all, and there is no second category for it to fall into. Yet the traditional term used by logicians for a formula is well formed formula, shortened to wff, and along with formula all three are used interchangeably.Herbert B. Enderton, A Mathematical Introduction to Logic, 2nd ed. (San Diego: Harcourt/Academic Press, 2001), §1.1, which introduces the three words as alternatives for one thing. Texts that keep the adjective and texts that drop it are describing the same objects. The adjective invites the reading that a determination carries its own negation along with it, so that well formed implies something for it to be distinguished from; the point is Hegel's, taken over from Spinoza's omnis determinatio est negatio. G. W. F. Hegel, Wissenschaft der Logik (Nuremberg: Schrag, 1812–1816), Book One, on determinate being; Baruch Spinoza to Jarig Jelles, June 2, 1674, Letter 50.A C++ committee borrowed the terminology for a well formed program, and then found it necessary to name the opposite, which became the ill formed program. ISO/IEC 14882, [defns.well.formed] and [defns.ill.formed], which pair the two definitions: a well formed program is one constructed according to the syntax rules, the diagnosable semantic rules, and the One Definition Rule, and an ill formed program is one that is not well formed. There the pair does work, because a compiler is required to say which side a given input falls on. This book uses formula.

+ +

An interpretation binds a proposition to each proposition symbol of a formula. Since each connective combines truth values and inspects nothing else, an interpretation carries no more information than the truth value each bound proposition holds, and the formula then holds or fails according to those truth values alone. Let p be bound to "the clock line is high" and q to "the enable line is high"; whether (p ∧ ¬q) holds follows from those two truth values and from nothing else. An interpretation does not alter the formula, which was settled before any interpretation was considered, and it does not reach inside a proposition, which was settled before it was bound.

+ +

A propositional calculus therefore consists of math objects that occur on an abstraction stack, which collects what has been said so far.

+ + + +
    +
  1. interpretation +
      +
    • binds a proposition, and so a truth value, to each proposition symbol
      • +
    +
    2. +
  2. formula +
      +
    • built from the level 0 symbols by the formation rules
      • +
    +
    3. +
  3. symbol +
      +
    • fixed: connective, parenthesis
      • +
    • variable, bound by an interpretation: proposition symbol
      • +
    +
    4. +
+ List . The propositional logic abstraction stack + -

The fates belong to appearances and not to variables, and a reader who forgets that will be caught by two ordinary formulas. In ∀x \, (F(x) ∧ ∃x \, G(x)) the inner quantifier claims the appearance inside G, and the outer one does not reach past it, so a claim is able to be shadowed by a nearer claim on the same variable. In (F(x) ∧ ∀x \, G(x)) the same variable appears free in the left conjunct and bound in the right. Both are well formed, and both are legible only by tracking appearances one at a time. A calculus that means to avoid the bookkeeping imposes a hygiene condition, requiring that no variable be claimed twice and that no variable appear both free and bound, and it then renames variables as needed to meet the condition. Renaming a bound variable throughout its scope changes nothing, since the quantifier runs it over the domain either way. Renaming a free variable changes what the formula is about.

+

Each level is settled without reference to the one above it. The symbols at level 0 are settled before any formula is written, the formula at level 1 is an arrangement of them and is settled before any interpretation is considered, and the interpretation at level 2 binds values to the variables among them. This is why the same formula serves under every interpretation and the same symbols serve in every formula. A hardware designer would recognize the level 1 formula as a gate network drawn before any signal has been applied to it.

-

Here at last is the word set aside earlier. A sentence is a formula in which no variable appears free. So ∀x ∃y \, R(x ,y) is a sentence, and ∃y \, R(x ,y) is a formula that is not one. A sentence makes an outright claim once its predicate symbols, names, and function symbols are supplied, whereas a formula with a free appearance holds or fails according to what that appearance is given, so its truth value varies where a sentence's does not. The propositional calculus has no variables at all, so no formula of it has a free appearance, so every formula of that calculus is a sentence. This is why nothing was lost by withholding the word until now.

+ -

An interpretation of a first-order formula supplies four things. It supplies a domain, which holds at least one member.Standard first-order logic does not admit the empty domain, and the reason is visible in the formulas. Over an empty domain ∀x \, F(x) would hold and ∃x \, F(x) would fail, so (∀x \, F(x) → ∃x \, F(x)) would not be valid; it is counted a validity of this calculus, and admitting the empty domain would cost that. It supplies a predicate over that domain for each predicate symbol, of the matching number of arguments, since no quantifier of this calculus is able to claim a predicate symbol and every one of them awaits an interpretation. It supplies a member of the domain for each name, and a function over the domain for each function symbol. And it supplies a member of the domain for each free appearance of a variable, passing over the bound appearances, which are already spoken for - The notation is not settled across the sources surveyed in this book. Hilbert and Ackermann write (x) for the universal quantifier and (Ex) for the existential, and they mark negation with an overbar rather than with ¬. A reader going to their book should be prepared for this.. - Take the Peano Numbers as the domain and LessThan for R: the sentence ∀x ∃y \, R(x ,y) then states that every Peano Number has a larger one, and under that interpretation it holds. Every appearance in it is bound, so the only things the interpretation had to supply were the domain and the predicate, which is what being a sentence buys.

+ + + The predicate calculus -

Validity and satisfiability are defined exactly as before, as holding under every interpretation and under at least one. What has changed is how much an interpretation now varies. In the propositional calculus it selected among 2^n assignments of truth values. Here it selects a domain of any size whatever, and then a predicate over that domain for each predicate symbol, so no table can be drawn over the interpretations and no tabulation settles the question. This is the calculus in which nearly all axiomatic mathematics is written, and it is the calculus of the Entscheidungsproblem as Hilbert and Ackermann posed it, as described in section . The calculus is sound and complete, so every validity has a derivation and a machine that enumerates derivations finds any one of them eventually. What such a machine does not have is a means of stopping when there is nothing to find, and that gap is the subject of the chapters ahead.

+

Now suppose that a proposition could be predicated on something else. A predicate is a logic function. It is given values for its arguments, and it then evaluates to true or to false. Give a predicate its arguments and what results is a proposition, so the predicate is the general case and the proposition is the settled one. prime(x) is a predicate of one argument, and prime(7) is true while prime(8) is false. less-than(x, y) is a predicate of two arguments, which is how a relation is written. The arguments are drawn from a domain, a set holding at least one member, and that set is whatever mathematics cares to name: the Peano Numbers, the points of a plane, the strings over an alphabet. The arguments are not themselves truth values. However, the result of the predicate is required to be a truth value.

-

The same three levels carry the first-order calculus. What a quantifier claims is a fact about the formula, so it is stated at level 1.

+

A property is a predicate of one argument. It is not a new kind of object; it is the one-argument case of the predicate already defined. even is a property of the Peano Numbers, holding of 4 and failing of 5, and prime is another. To give a property over a domain is to mark off which members of that domain it holds of, so the properties of a domain stand in exact correspondence with the sub-collections of it, and a domain of n members carries 2^n properties.This correspondence counts two predicates holding of the same members as the same property, a convention called extensionality. It sets aside the sense in which 'is an equilateral triangle' and 'is an equiangular triangle' are different properties that happen to hold of the same figures. The properties of a domain form a collection of their own, distinct from the domain, so a quantifier ranging over the one is not ranging over the other.

- - -
    -
  1. interpretation -
      -
    • supplies a domain, a predicate for each predicate symbol, a domain member for each name, a function for each function symbol, and a domain member for each free appearance of a variable
      • -
    -
    2. -
  2. formula -
      -
    • a quantifier in it claims a domain variable
      • -
    • a formula with no free appearance is a sentence
      • -
    -
    3. -
  3. symbol -
      -
    • fixed: connective, parenthesis, quantifier
      • -
    • awaiting an interpretation: predicate symbol, name, function symbol
      • -
    • claimable by a quantifier: domain variable
      • -
    -
    4. -
- List . The first order predicate logic stack - +

The first-order predicate calculus also begins with symbols, and its base level holds three groups rather than two. The fixed group gains the quantifiers, ∀ (for all) and ∃ (there exists), alongside the connectives and parentheses already in it. Three kinds of variable are bound by an interpretation: the predicate symbol, written F, G, R, which carries a fixed number of argument places and marks a place for a predicate of that many arguments; the name, written a, b, c, which marks a place for one member of the domain; and the function symbol, written f, g, s, which carries a fixed number of argument places and marks a place for a function carrying that many domain members to one domain member.The capitals for predicate symbols are the traditional letters, and are kept so that a reader can find the literature. The third group is new, and holds the variables a quantifier is able to claim. This calculus has one kind, the domain variable, written x, y, z. The proposition symbol is gone, having no work left to do: a predicate symbol given its arguments occupies the place where a proposition once stood.

-

A property is a predicate of one argument. It is not a new kind of object; it is the one-argument case of the predicate already defined. Even is a property of the Peano Numbers, holding of 4 and failing of 5, and Prime is another. To give a property over a domain is to mark off which members of that domain it holds of, so the properties of a domain stand in exact correspondence with the sub-collections of it, and a domain of n members carries 2^n properties. That correspondence counts two predicates holding of the same members as the same property, which is a decision and not a discovery.The decision is called extensionality. It sets aside the sense in which 'is an equilateral triangle' and 'is an equiangular triangle' are different properties that happen to hold of the same figures. Nothing in the calculus below is able to tell them apart, and nothing in it needs to. What matters for the calculus that follows is that the properties of a domain form a collection of their own, distinct from the domain, and that a quantifier ranging over the one is not ranging over the other.

+

A function applied to domain members yields another domain member, so the expressions that mark out a member of the domain have to be settled before the formulas can be. A term is a domain variable, or a name, or a function symbol of n places applied to n terms, and nothing else is a term. A term marks out a member of the domain and carries no truth value of its own. So x, a, and f(s(a), x) are terms.The word is used elsewhere in this book in its ordinary sense, for one of the parts of a compound expression, as when the two conjuncts of a set-defining condition are called its terms in chapter . Where the calculus is under discussion, the definition given here is the one intended.

-

In the first-order calculus a quantifier claims a domain variable and nothing else. Each predicate symbol awaits an interpretation, so a person supplies a particular predicate for F and asks what follows, and no formula of that calculus ranges over the predicates themselves. The second-order predicate calculus lifts that restriction by admitting a second kind of variable, the predicate variable, which a quantifier is able to claim and which carries a fixed number of argument places. The two fates are as before, and they now apply to this second kind of symbol as well. In ∀F \, Φ the quantifier has claimed F, so no interpretation supplies a predicate for it, and the quantifier runs it over the properties of the domain in the same way that ∀x runs a domain variable over the domain itself. An interpretation of a second-order formula supplies everything it supplied before, and then a property of the domain for each free appearance of a predicate variable. A second-order sentence is again a formula with no free appearance of a variable of either kind.

+ + +
    +
  1. A predicate symbol of n places applied to n terms is a formula, and it is atomic.
    2. +
  2. If Φ and Ψ are formulas, then ¬Φ is a formula, and so is (Φ ∘ Ψ) for each binary connective ∘.
    3. +
  3. If Φ is a formula and x is a domain variable, then ∀x \, Φ and ∃x \, Φ are formulas.
    4. +
  4. No expression is a formula except by finitely many applications of rules 1 through 3.
    5. +
+ List . Formation rules of the first-order predicate calculus + -

With second-order logic, statements are able to be about properties. Mathematical induction provides a good example as to why this is useful. In the first-order calculus, induction is written as an infinite family of axioms, one for each formula a person might induct upon, because that calculus has no way to say "for every property". In the second-order calculus it is one axiom:

+

So ∀x \, F(x) and ∀x ∃y \, R(x, y) are formulas of the calculus.

+ +

A quantifier claims the domain variable written after it, and its claim reaches over the formula that rule 3 was applied to and no further. That formula is the quantifier's scope. Where a variable appears within the scope of a quantifier claiming it, that appearance is bound; where it appears within no such scope, that appearance is free.The words bound and free are the standard ones, and are given here so that a reader can find the literature. The word claims is used alongside them in this book because it names the agency. An interpretation binds nothing to a bound appearance, because the quantifier is what runs it over the domain, passing the formula over every member in the universal case and over at least one member in the existential case. A free appearance is left for an interpretation to bind. There are these two fates and no third, and no appearance meets both.

+ +

The fates belong to appearances and not to variables, as two ordinary formulas show. In ∀x \, (F(x) ∧ ∃x \, G(x)) the inner quantifier claims the appearance inside G, and the outer one does not reach past it, so a claim is able to be shadowed by a nearer claim on the same variable. In (F(x) ∧ ∀x \, G(x)) the same variable appears free in the left conjunct and bound in the right. Both are formulas, and both are legible only by tracking appearances one at a time. A calculus that means to avoid the bookkeeping imposes a hygiene condition, requiring that no variable be claimed twice and that no variable appear both free and bound, and it then renames variables as needed to meet the condition. Renaming a bound variable throughout its scope changes nothing, since the quantifier runs it over the domain either way. Renaming a free variable changes what the formula is about.

+ +

A formula in which no variable appears free, also called a sentence, makes an outright claim once its predicate symbols, names, and function symbols are bound. A formula with a free appearance holds or fails according to what is bound to that appearance, so its truth value varies where the other's does not. So ∀x ∃y \, R(x, y) is one and ∃y \, R(x, y) is not. The distinction has no work to do in the propositional calculus, which holds no quantifier and so no free appearances.

+ +

An interpretation of a first-order formula binds four things. It supplies a domain, which holds at least one member.Standard first-order logic does not admit the empty domain, and the reason is visible in the formulas. Over an empty domain ∀x \, F(x) would hold and ∃x \, F(x) would fail, so (∀x \, F(x) → ∃x \, F(x)) would not be valid; it is counted a validity of this calculus, and admitting the empty domain would cost that. It binds a predicate over that domain to each predicate symbol, of the matching number of arguments. It binds a member of the domain to each name, and a function over the domain to each function symbol. And it binds a member of the domain to each free appearance of a domain variable, passing over the bound appearances, which the quantifier has already claimed.The notation is not settled across the sources surveyed in this book. Hilbert and Ackermann write (x) for the universal quantifier and (Ex) for the existential, and they mark negation with an overbar rather than with ¬. A reader going to their book should be prepared for this. Take the Peano Numbers as the domain and less-than for R: the formula ∀x ∃y \, R(x, y) then states that every Peano Number has a larger one, and under that interpretation it holds. Every appearance in it is bound by a quantifier, so the only things the interpretation had to bind were the domain and the predicate.

+ +

The same three levels carry the first-order calculus. What a quantifier claims is a fact about the formula, so it is stated at level 1.

+ + + +
    +
  1. interpretation +
      +
    • supplies a domain, and binds a predicate to each predicate symbol, a domain member to each name, a function to each function symbol, and a domain member to each free appearance of a domain variable
      • +
    +
    2. +
  2. formula +
      +
    • a quantifier in it claims a domain variable
      • +
    • a formula with no free appearance makes an outright claim
      • +
    +
    3. +
  3. symbol +
      +
    • fixed: connective, parenthesis, quantifier
      • +
    • variable, bound by an interpretation: predicate symbol, name, function symbol
      • +
    • variable, claimable by a quantifier and otherwise bound by an interpretation: domain variable
      • +
    +
    4. +
+ List . The first order predicate logic stack + -

∀F \, \big( (F(0) ∧ ∀x \, (F(x) → F(s(x)))) → ∀x \, F(x) \big)

+

In the first-order calculus a quantifier claims a domain variable and nothing else. Each predicate symbol is bound by an interpretation, so a person supplies a particular predicate for F and asks what follows, and no formula of that calculus ranges over the predicates themselves. The second-order predicate calculus lifts that restriction by admitting a second kind of claimable variable, the predicate variable, which carries a fixed number of argument places. The two fates are as before, and now apply to this second kind of symbol as well. In ∀F \, Φ the quantifier has claimed F, so no interpretation binds a predicate to it, and the quantifier runs it over the properties of the domain in the same way that ∀x runs a domain variable over the domain itself.

+ +

Mathematical induction shows what this buys. In the first-order calculus, induction is written as an infinite family of axioms, one for each formula a person might induct upon, because that calculus has no way to say "for every property". In the second-order calculus it is one axiom:

+ +

∀F \, \big( (F(0) ∧ ∀x \, (F(x) → F(s(x)))) → ∀x \, F(x) \big)

+ +

where 0 is a name marking the place of zero and s is a function symbol of one place marking the place of the successor function, both of which the formation rules admit within terms. The outermost quantifier has claimed the predicate variable, so the axiom states that any property holding of zero and carried from each Peano Number to its successor holds of every Peano Number.

+ +

One cell of the abstraction stack changes, and it is the cell at level 0.

+ + + +
    +
  1. interpretation +
      +
    • supplies a domain, and binds a predicate to each predicate symbol, a domain member to each name, a function to each function symbol, a domain member to each free appearance of a domain variable, and a property to each free appearance of a predicate variable
      • +
    +
    2. +
  2. formula +
      +
    • a quantifier in it claims a domain variable or a predicate variable
      • +
    • a formula with no free appearance of either kind makes an outright claim
      • +
    +
    3. +
  3. symbol +
      +
    • fixed: connective, parenthesis, quantifier
      • +
    • variable, bound by an interpretation: predicate symbol, name, function symbol
      • +
    • variable, claimable by a quantifier and otherwise bound by an interpretation: domain variable, predicate variable
      • +
    +
    4. +
+ List . The second order predicate logic stack + -

where 0 is a name marking the place of zero and s is a function symbol of one place marking the place of the successor function, both of which the formation rules admit within terms. The outermost quantifier has claimed the predicate variable, so the axiom states that any property holding of zero and carried from each Peano Number to its successor holds of every Peano Number.

+

Reading ∀F as running over every property of the domain is the reading intended above, and it is called the standard semantics.The alternative is to let an interpretation nominate a smaller collection of properties for the quantifier to run over, which is the Henkin semantics. Leon Henkin, "Completeness in the Theory of Types", Journal of Symbolic Logic 15, no. 2 (1950): 81−91.

-

One cell of the abstraction stack changes, and it is the cell at level 1.

+ - - -
    -
  1. interpretation -
      -
    • supplies a domain, a predicate for each predicate symbol, a domain member for each name, a function for each function symbol, a domain member for each free appearance of a domain variable, and a property for each free appearance of a predicate variable
      • -
    -
    2. -
  2. formula -
      -
    • a quantifier in it claims a domain variable or a predicate variable
      • -
    • a formula with no free appearance of either kind is a sentence
      • -
    -
    3. -
  3. symbol -
      -
    • fixed: connective, parenthesis, quantifier
      • -
    • awaiting an interpretation: predicate symbol, name, function symbol
      • -
    • claimable by a quantifier: domain variable, predicate variable
      • -
    -
    4. -
- List . The second order predicate logic stack - + + + Assessment -

The gain is paid for. Read ∀F as running over every property of the domain, which is the reading intended above and is called the standard semantics, and there is then no set of axioms and rules that is at once sound, complete, and mechanically checkable. Some validity of the calculus escapes any such set, so here the two accounts come apart and ⊨ outruns ⊢ permanently.The alternative is to let an interpretation nominate a smaller collection of properties for the quantifier to run over, which is the Henkin semantics. Under it the calculus is complete again, at the cost of becoming a first-order calculus of two sorts wearing second-order notation. Leon Henkin, "Completeness in the Theory of Types", Journal of Symbolic Logic 15, no. 2 (1950): 81−91. This is the first place in the book where expressive power and mechanical reach are seen to trade against each other, and it will not be the last.

+

The words below are for saying what a formula is worth, and they stand above the stack rather than on it, since each of them quantifies over interpretations rather than being one.

-

The word order counts something different in each of the two places this book uses it, and the two scales are independent of each other. In the predicate calculus, the order counts what a quantifier runs over: a domain member at the first order, and a property of domain members at the second. In the orders of analysis set out in section , the order counts the depth of machines examining machines: running a machine is the first order, examining a machine's definition is the second, and examining an examiner is the third. A second-order analysis of a machine that computes over the first-order predicate calculus is an ordinary thing, and nothing about it is second-order logic. The same warning applies to metamathematics. A statement about a first-order system is made in the metalanguage, and that alone does not make it a second-order statement.

+

A formula that holds under every interpretation is valid, and in the propositional calculus such a formula is also called a tautology. A formula that holds under at least one interpretation is satisfiable. So ((p ∧ p) ↔ p) is valid, (p ∧ q) is satisfiable and not valid, and (p ∧ ¬p) is neither. The two are duals: a formula is valid exactly when its negation is unsatisfiable.

-

The purpose of this section was to establish that the reader and author are speaking the same language. This discussion is far from being complete. The quantifier is a binding symbol, and the treatment given here was particular to the quantifier rather than general to binding, so the binding symbol as a construct in its own right was left aside. Issues for a sequential construction were not discussed, such as the question that binding symbols are needed for the propositional logic, but require the predicate logic to express. Perhaps after this entire book is finished, these issues will be closed, or at least reduced to some specific questions.

+

Say a formula of the propositional calculus holds n distinct proposition symbols. An interpretation binds a proposition to each of them, and there is no counting the propositions, but the calculus reads nothing from a proposition except its truth value. What the formula answers to is therefore the induced binding of a truth value to each proposition symbol, and of those there are exactly 2^n. A truth table is an enumeration of them, one per row.

- +

A derivation is a finite arrangement of formulas built from a stated collection of axioms by stated rules, ending at the formula being derived. Where validity asks what holds under every interpretation, derivation asks what can be reached by rearranging marks, and it consults no interpretation at all. The two are written as follows.

- - Machines + + + + Φ holds under every interpretation. + A derivation of Φ exists from the stated axioms and rules. + + List . The two assessments of a formula + -

This book discusses four theoretical computing machines: two types of Turing Machine, which are not realizable, and two types of RT Machine, which are. What blocks realization of the first pair, and what removes the block from the second, is the subject of the chapters that follow.

+

A collection of axioms and rules is sound when everything it derives is valid, so ⊢ never outruns ⊨, and complete when everything valid is derivable, so ⊨ never outruns ⊢.The turnstile ⊢ is reused later in this book, subscripted with a machine, for the relation between one instantaneous description of a Turing Machine and the next. The subscript keeps the two apart on the page. A calculus together with a collection of axioms is a theory. Completeness is a property of the axioms and rules relative to the validities of a calculus, and is not the same question as whether a theory settles every statement it can express; the second question is taken up in chapter .

-

The first type of Turing Machine has a fixed controller, and that controller determines the machine's behavior. Colloquially, a person could say that the program it runs is built-in. There can be many instances of this type, each with a different built-in program, which is why the term Turing Machine is sometimes used in the sense of a computer program, and is sometimes plural. The program of such a machine cannot be changed, though the same input tape can be mounted on another Turing Machine having a different controller.

+

The Entscheidungsproblem asks for a mechanical procedure that decides, in finitely many steps, whether a given formula is valid. Enumerating the 2^n rows of a truth table is such a procedure for the propositional calculus. For the first-order calculus an interpretation selects a domain of any size whatever, so there is no finite set of rows to enumerate. Chapter gives the history of the problem and its answer.Hilbert and Ackermann review the tabulation procedure for the propositional calculus in the first chapter of the 1928 book, before raising the same question for the first-order calculus. Their two formulations of the problem are distinguished by domains: the first asks for which domains of individuals a given expression is valid, and the second asks only whether it is valid for all of them.

-

The second type is the Universal Turing Machine, which reads its program from its tape. Each tape then gives the machine its own personality, so the built-in controller of a Universal Turing Machine is an interpreter. There is no reason there could not be several Universal Turing Machines, each with a different interpreter for reading the program from the tape. Hence, where this text speaks of a Turing Machine reading a program from a tape, it refers to a Universal Turing Machine; and where it speaks of a program, it refers to data that, when written to a tape, could be executed by a Universal Turing Machine.

+

Finally, the word order counts something different in each of the two places this book uses it, and the two scales are independent of each other. In the predicate calculus, the order counts what a quantifier runs over: a domain member at the first order, and a property of domain members at the second. In the orders of analysis set out in section , the order counts the depth of machines examining machines: running a machine is the first order, examining a machine's definition is the second, and examining an examiner is the third. A second-order analysis of a machine that computes over the first-order predicate calculus is an ordinary thing, and nothing about it is second-order logic. Where a later chapter of this book speaks of second-order arithmetic, it is the orders of analysis that are meant. The same warning applies to metamathematics: a statement about a first-order system is made in the metalanguage, and that alone does not make it a second-order statement.

-

The RT Machine is a variation on the Turing Machine, and it comes in the same two types: one with a built-in controller, and one that reads its program from the tape. Unlike the Turing Machine, the RT Machine belongs to a class of realizable machines.

+ - + Preface