<RT·section id="Section·common-ground">
<RT·name>Common Ground</RT·name>
- <p>All communication builds upon a foundation of common knowledge, so let us begin by searching for some common ground.</p>
-
- <RT·section id="Section·grounding_fields-of-study">
- <RT·name>Fields of study</RT·name>
-
- <p>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.</p>
-
- <p>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 <RT·term>error</RT·term>. 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.</p>
-
- <p>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.</p>
- </RT·section>
-
+ <p>All communication builds upon a foundation of common knowledge, so let us begin by searching for some common ground. This section discusses the terminology and conventions the rest of the book is based upon. It is a chapter for getting accustom to the language used. However, this chapter is not intended to present new material, nor to serve as a tutorial for the discussed subjects.</p>
<RT·section id="Section·grounding_notation">
<RT·name>Notation</RT·name>
<p>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 <RT·code>Z</RT·code> marks the time as UTC. Hence <RT·code>2026-06-01 08:28:00Z</RT·code>. ISO 8601 itself separates the date from the time with a <RT·code>T</RT·code>, which is difficult to read. RFC 3339 anticipates the objection and permits a space in its place, and that is the option taken here.<RT·endnote>Graham Klyne and Chris Newman, <em>Date and Time on the Internet: Timestamps</em>, RFC 3339, July 2002, §5.6.</RT·endnote> Where a date appears without a time, the date alone is intended, e.g. <RT·code>2026-06-01</RT·code>. As per the standard, if the day is not to be specified, it is simply dropped, e.g. <RT·code>2026-06</RT·code>.</p>
</RT·section>
- <RT·section id="Section·grounding_logic_symbol">
- <RT·name>Symbol and binding</RT·name>
+ <RT·section id="Section·grounding_number-types">
+ <RT·name>Number types</RT·name>
- <p>A <em>math object</em> 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 <RT·term>value</RT·term>, where the term is used without qualification, is synonymous with math object.</p>
+ <p>Several words in this book carry a formal definition that displaces their ordinary English sense, and those are capitalized: <RT·term-em>Peano Number</RT·term-em>, <RT·term>Integer</RT·term>, <RT·term>Rational</RT·term>, <RT·term>Real</RT·term>. The word <em>real</em> 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.</p>
+
+ <p>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.</p>
+
+ <p>What mathematics calls the natural numbers are called <RT·term>Peano Number</RT·term>s 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 <RT·term>Counting Numbers</RT·term> begin at one, and the two are not the same.<RT·endnote>Peano's own axioms began at one. Modern presentations of Peano arithmetic begin at zero, and that is the convention followed here. Giuseppe Peano, <em>Arithmetices principia, nova methodo exposita</em> (Turin: Bocca, 1889), §1.</RT·endnote> An Integer, a Rational, and a Real are likewise the outputs of machines, each constructed in its turn.</p>
+ </RT·section>
+
+ <RT·section id="Section·grounding_fields-of-study">
+ <RT·name>Fields of study</RT·name>
+
+ <p>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.</p>
+
+ <p>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 <RT·term>error</RT·term>. 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.</p>
+
+ <p>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.</p>
+ </RT·section>
- <p>A <RT·term>symbol</RT·term> 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 <RT·term>representation</RT·term>. 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 <em>representation</em> and <em>instance</em>, but might instead refer to an instance of a symbol representation as a <em>sign</em>, a <em>letter</em>, or a <em>mark</em>.<RT·endnote>Philosophy calls this the distinction between a <em>type</em> and its <em>tokens</em>, 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, <em>Collected Papers</em>, vol. 4, §537.</RT·endnote> Chapter <RT·Counter·read snapshot="Section·symbol_in-computing"></RT·Counter·read> takes up this topic in more detail.</p>
+ <RT·section id="Section·symbol_and-function">
+ <RT·name>Symbol</RT·name>
+
+ <p>A <em>math object</em> 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 <RT·term>value</RT·term>, where the term is used without qualification, is synonymous with math object.</p>
<p>An <RT·term>evaluation context</RT·term> 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.</p>
- <p>A <RT·term>math context</RT·term> 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.</p>
+ <p>A <RT·term>math context</RT·term> 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. An even larger context is that of a <RT·term>math context class</RT·term>, which contains multiple math contexts. An example would be a general proof form, where instances are specific proofs.</p>
- <p>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.</p>
+ <p>A <RT·term>symbol scope</RT·term>, or when the context of the usage is clear, simply <RT·term>scope</RT·term>, is a set of evaluation contexts. The members of the set are specified by the author who presents the math. A commonly specified scope is that of the math context. This is what most people will think of when the terms we are about to discuss are used. Applying this reading will produce correct definitions, though not the only possible definitions.</p>
- <p>A <RT·term>constant</RT·term> is a value that is the same in every evaluation context of a math context.</p>
+ <p>A <RT·term>symbol</RT·term> is a designated math object, where each symbol is distinct from every other symbol within scope, 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 <RT·term>representation</RT·term>. 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 <em>representation</em> and <em>instance</em>, but might instead refer to an instance of a symbol representation as a <em>sign</em>, a <em>letter</em>, or a <em>mark</em>.<RT·endnote>Philosophy calls this the distinction between a <em>type</em> and its <em>tokens</em>, 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, <em>Collected Papers</em>, vol. 4, §537.</RT·endnote></p>
- <p>A symbol can be bound to any value, including another symbol. This binding can be expressed as a predicate, <RT·math>bind(s, v)</RT·math>, where <RT·math>s</RT·math> is the symbol and <RT·math>v</RT·math> is the value it is bound to. Chapter <RT·Counter·read snapshot="Section·binding"></RT·Counter·read> discusses binding in more detail.</p>
+ <p>A symbol can be bound to any value, including another symbol. This binding can be expressed as a predicate, <RT·math>\text{bind}(s, v)</RT·math>, where <RT·math>s</RT·math> is the symbol and <RT·math>v</RT·math> is the value it is bound to. Each distinct pair of arguments gives a distinct binding, so a binding is an object in its own right, and two bindings of the same symbol to different values are two objects rather than one object altered.</p>
- <p>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 <RT·term>fixed symbol</RT·term>. Where a symbol is bound to different values in different evaluation contexts, or is bound in some and unbound in others, it is a <RT·term>variable</RT·term>. Where a symbol is unbound in every evaluation context, it is <RT·term-em>purely symbolic</RT·term-em>. 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.</p>
+ <p>Within an evaluation context a symbol is in one of two binding states: it is bound to a value, or it is unbound. In each evaluation context a symbol can be separately unbound or bound, and in cases where it is bound, it can potentially have different bindings. Comparing symbol bindings across a scope sorts the symbols of that scope into three cases. Where a symbol is bound to the same value in every evaluation context it is a <RT·term>fixed symbol</RT·term>. Where a symbol is bound to different values in different evaluation contexts, or is bound in some and unbound in others, it is a <RT·term>variable</RT·term>. Where a symbol is unbound in every evaluation context, it is <RT·term-em>purely symbolic</RT·term-em>.</p>
- </RT·section>
+ <p>It follows that what is fixed, variable, or purely symbolic in one scope, might not be so in another scope. An interesting situation occurs when scopes are nested. This creates an ambiguity in binding membership. Some of the outer bindings are said to also belong to the inner scope. These are <RT·term>inherited</RT·term>. Some of the inner bindings will be said not to belong to the outer scope, and these are <RT·term>local</RT·term>. And typically one binding from the inner scope will be said to also belong to the outer scope, this being said to define a <RT·term>return value</RT·term>.</p>
- <RT·section id="Section·grounding_number-types">
- <RT·name>Number types</RT·name>
+ <p>A <RT·term>function</RT·term> is a sort of general template that places an inner scope when instantiated. All the symbols in the template remain local and distinct between instances. Symbols that are intended to be inherited from the outer scope are left purely symbolic in the function body, and the function definition provides a list of them called a <RT·term>parameter list</RT·term>. Instantiating the function binds each parameter to a value found in the outer scope, and that value is called an <RT·term>argument</RT·term>. One further parameter is intended to be bound to a symbol in the outer scope, and that outer scope symbol is bound to the function return value. Quantifying over the instantiations of a function, one evaluation context per full binding of the parameter list, maps arguments to return values. This map is the conventional math definition of a function, so there are two readings, the template, and its quantification.</p>
- <p>Several words in this book carry a formal definition that displaces their ordinary English sense, and those are capitalized: <RT·term-em>Peano Number</RT·term-em>, <RT·term>Integer</RT·term>, <RT·term>Rational</RT·term>, <RT·term>Real</RT·term>. The word <em>real</em> 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.</p>
+ <p>Because a function annotates what goes in and out of an inner scope, any evaluation context, or set of evaluation contexts, can be interpreted as being a function.</p>
- <p>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.</p>
+ <p>The term <RT·term>constant</RT·term> is a property ascribed to an object when a primary aspect of that object under discussion does not change across evaluation contexts. Different primary aspects are conventionally considered. Of a fixed symbol, the aspect is its binding as an object. Of a function, it is the return value, which for a constant function is the same for every evaluation. Of a primitive math object such as an individual Peano Number, it is the object itself. This latter usage would mean that the term <em>constant</em> is the same as a <em>math object</em>, and thus the same as <em>value</em>.</p>
- <p>What mathematics calls the natural numbers are called <RT·term>Peano Number</RT·term>s 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 <RT·term>Counting Numbers</RT·term> begin at one, and the two are not the same.<RT·endnote>Peano's own axioms began at one. Modern presentations of Peano arithmetic begin at zero, and that is the convention followed here. Giuseppe Peano, <em>Arithmetices principia, nova methodo exposita</em> (Turin: Bocca, 1889), §1.</RT·endnote> An Integer, a Rational, and a Real are likewise the outputs of machines, each constructed in its turn.</p>
</RT·section>
-
- <RT·section id="Section·grounding_logic">
+ <RT·section id="Section·Grounding·Logic">
<RT·name>Logic</RT·name>
- <!------------------------------------------------------------------------------->
- <RT·section id="Section·grounding_logic_propositional">
- <RT·name>The propositional calculus</RT·name>
+ <RT·section id="Section·Grounding·Propositional_calculus">
+ <RT·name>Propositional calculus</RT·name>
<p>A <RT·term>proposition</RT·term> is a statement that is given no arguments and carries a <RT·term>truth value</RT·term>, that being one of exactly two things, written <RT·term-em>true</RT·term-em> and <RT·term-em>false</RT·term-em>. 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.</p>
<p>For example, <RT·math>(p ∧ ¬q)</RT·math> is a formula. Rule 1 supplies <RT·math>p</RT·math>, and supplies <RT·math>q</RT·math>. Rule 2 applied to <RT·math>q</RT·math> supplies the negation, <RT·math>¬q</RT·math>. Rule 2 applied again, this time to the pair, supplies <RT·math>(p ∧ ¬q)</RT·math>, 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.</p>
- <p>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 <em>well formed formula</em> and the <em>malformed formula</em>. Take the string <RT·math>p ¬ ∧ q</RT·math>, 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 <RT·term-em>well formed formula</RT·term-em>, shortened to <RT·term-em>wff</RT·term-em>, and along with <em>formula</em> all three are used interchangeably.<RT·endnote>Herbert B. Enderton, <em>A Mathematical Introduction to Logic</em>, 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 <em>well formed</em> implies something for it to be distinguished from; the point is Hegel's, taken over from Spinoza's <em>omnis determinatio est negatio</em>. G. W. F. Hegel, <em>Wissenschaft der Logik</em> (Nuremberg: Schrag, 1812–1816), Book One, on determinate being; Baruch Spinoza to Jarig Jelles, June 2, 1674, Letter 50.</RT·endnote><RT·endnote>A C++ committee borrowed the terminology for a <em>well formed program</em>, and then found it necessary to name the opposite, which became the <em>ill formed</em> 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.</RT·endnote> This book uses <em>formula</em>.</p>
+ <p>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 <em>well formed formula</em> and the <em>malformed formula</em>. Take the string <RT·math>p ¬ ∧ q</RT·math>, 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 called <em>malformed formula</em> for it to fall into. Yet the traditional term used by logicians for a formula is <RT·term-em>well formed formula</RT·term-em>, shortened to <RT·term-em>wff</RT·term-em>, and along with <em>formula</em> all three are used interchangeably.<RT·endnote>Herbert B. Enderton, <em>A Mathematical Introduction to Logic</em>, 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 <em>well formed</em> implies something for it to be distinguished from; the point is Hegel's, taken over from Spinoza's <em>omnis determinatio est negatio</em>. G. W. F. Hegel, <em>Wissenschaft der Logik</em> (Nuremberg: Schrag, 1812–1816), Book One, on determinate being; Baruch Spinoza to Jarig Jelles, June 2, 1674, Letter 50.</RT·endnote><RT·endnote>A C++ committee borrowed the terminology for a <em>well formed program</em>, and then found it necessary to name the opposite, which became the <em>ill formed</em> 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.</RT·endnote> This book uses <em>formula</em>.</p>
<p>An <RT·term>interpretation</RT·term> 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 <RT·math>p</RT·math> be bound to "the clock line is high" and <RT·math>q</RT·math> to "the enable line is high"; whether <RT·math>(p ∧ ¬q)</RT·math> 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.</p>
</RT·section>
<!------------------------------------------------------------------------------->
- <RT·section id="Section·grounding_logic_predicate">
- <RT·name>The predicate calculus</RT·name>
+ <RT·section id="Section·Grounding·First-order_predicate_calculus">
+ <RT·name>First-order predicate calculus</RT·name>
- <p>Now suppose that a proposition could be predicated on something else. A <RT·term>predicate</RT·term> 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. <RT·math>prime(x)</RT·math> is a predicate of one argument, and <RT·math>prime(7)</RT·math> is true while <RT·math>prime(8)</RT·math> is false. <RT·math>less-than(x, y)</RT·math> is a predicate of two arguments, which is how a relation is written. The arguments are drawn from a <RT·term>domain</RT·term>, 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.</p>
+ <p>Now suppose that a proposition could be predicated on something else. A <RT·term>predicate</RT·term> 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. <RT·math>\text{prime}(x)</RT·math> is a predicate of one argument, and <RT·math>\text{prime}(7)</RT·math> is true while <RT·math>\text{prime}(8)</RT·math> is false. <RT·math><(x, y)</RT·math> is a predicate of two arguments, which is how a relation is written. Thus <RT·math><(3, 5)</RT·math> is true, while <RT·math><(5, 3)</RT·math> is false. Predicate arguments are drawn from a <RT·term>domain</RT·term>, 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. Nothing requires the arguments to be truth values, and nothing forbids it. What is required is that the result be a truth value.</p>
- <p>A <RT·term>property</RT·term> 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. <RT·math>even</RT·math> is a property of the Peano Numbers, holding of 4 and failing of 5, and <RT·math>prime</RT·math> 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 <RT·math>n</RT·math> members carries <RT·math>2^n</RT·math> properties.<RT·endnote>This correspondence counts two predicates holding of the same members as the same property, a convention called <em>extensionality</em>. 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.</RT·endnote> 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.</p>
+ <p>A <RT·term>property</RT·term> 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. <RT·math>\text{even}</RT·math> is a property of the Peano Numbers, holding of 4 and failing of 5, and <RT·math>\text{prime}</RT·math> 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 <RT·math>n</RT·math> members carries <RT·math>2^n</RT·math> properties.<RT·endnote>This correspondence counts two predicates holding of the same members as the same property, a convention called <em>extensionality</em>. 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.</RT·endnote> 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.</p>
- <p>The <RT·term>first-order predicate calculus</RT·term> also begins with symbols, and its base level holds three groups rather than two. The fixed group gains the <RT·term>quantifier</RT·term>s, <RT·math>∀</RT·math> (for all) and <RT·math>∃</RT·math> (there exists), alongside the connectives and parentheses already in it. Three kinds of variable are bound by an interpretation: the <RT·term>predicate symbol</RT·term>, written <RT·math>F</RT·math>, <RT·math>G</RT·math>, <RT·math>R</RT·math>, which carries a fixed number of argument places and marks a place for a predicate of that many arguments; the <RT·term>name</RT·term>, written <RT·math>a</RT·math>, <RT·math>b</RT·math>, <RT·math>c</RT·math>, which marks a place for one member of the domain; and the <RT·term>function symbol</RT·term>, written <RT·math>f</RT·math>, <RT·math>g</RT·math>, <RT·math>s</RT·math>, which carries a fixed number of argument places and marks a place for a function carrying that many domain members to one domain member.<RT·endnote>The capitals for predicate symbols are the traditional letters, and are kept so that a reader can find the literature.</RT·endnote> The third group is new, and holds the variables a quantifier is able to claim. This calculus has one kind, the <RT·term>domain variable</RT·term>, written <RT·math>x</RT·math>, <RT·math>y</RT·math>, <RT·math>z</RT·math>. 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.</p>
+ <p>The <RT·term>first-order predicate calculus</RT·term> also begins with symbols, and its base level holds three groups rather than two. The fixed group gains the <RT·term>quantifier</RT·term>s, <RT·math>∀</RT·math> (for all) and <RT·math>∃</RT·math> (there exists), alongside the connectives and parentheses already in it. The second group holds the variables an interpretation binds, and there are three kinds of them. A <RT·term>predicate symbol</RT·term> is a variable to be bound to a predicate, and it carries a fixed number of argument places, so that the predicate bound to it is one of that many arguments; its representations are commonly <RT·math>F</RT·math>, <RT·math>G</RT·math>, and <RT·math>R</RT·math>. A <RT·term>name</RT·term> is a variable to be bound to one member of the domain; its representations are commonly <RT·math>a</RT·math>, <RT·math>b</RT·math>, and <RT·math>c</RT·math>. A <RT·term>function symbol</RT·term> is a variable to be bound to a function carrying some fixed number of domain members to one domain member, and it carries that many argument places; its representations are commonly <RT·math>f</RT·math>, <RT·math>g</RT·math>, and <RT·math>s</RT·math>.<RT·endnote>The capitals are the traditional letters for predicate symbols, and are kept so that a reader can find the literature.</RT·endnote> The third group is new, and holds the variables a quantifier is able to claim. This calculus has one kind, the <RT·term>domain variable</RT·term>, whose representations are commonly <RT·math>x</RT·math>, <RT·math>y</RT·math>, and <RT·math>z</RT·math>. 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.</p>
<p>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 <RT·term>term</RT·term> is a domain variable, or a name, or a function symbol of <RT·math>n</RT·math> places applied to <RT·math>n</RT·math> 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 <RT·math>x</RT·math>, <RT·math>a</RT·math>, and <RT·math>f(s(a), x)</RT·math> are terms.<RT·endnote>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 <RT·Counter·read snapshot="Section·search-for_Turing-Machine"></RT·Counter·read>. Where the calculus is under discussion, the definition given here is the one intended.</RT·endnote></p>
<p>A formula in which no variable appears free, also called a <RT·term-em>sentence</RT·term-em>, 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 <RT·math>∀x ∃y \, R(x, y)</RT·math> is one and <RT·math>∃y \, R(x, y)</RT·math> is not. The distinction has no work to do in the propositional calculus, which holds no quantifier and so no free appearances.</p>
- <p>An interpretation of a first-order formula binds four things. It supplies a domain, which holds at least one member.<RT·endnote>Standard first-order logic does not admit the empty domain, and the reason is visible in the formulas. Over an empty domain <RT·math>∀x \, F(x)</RT·math> would hold and <RT·math>∃x \, F(x)</RT·math> would fail, so <RT·math>(∀x \, F(x) → ∃x \, F(x))</RT·math> would not be valid; it is counted a validity of this calculus, and admitting the empty domain would cost that.</RT·endnote> 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.<RT·endnote>The notation is not settled across the sources surveyed in this book. Hilbert and Ackermann write <RT·math>(x)</RT·math> for the universal quantifier and <RT·math>(Ex)</RT·math> for the existential, and they mark negation with an overbar rather than with <RT·math>¬</RT·math>. A reader going to their book should be prepared for this.</RT·endnote> Take the Peano Numbers as the domain and <RT·math>less-than</RT·math> for <RT·math>R</RT·math>: the formula <RT·math>∀x ∃y \, R(x, y)</RT·math> 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.</p>
+ <p>An interpretation of a first-order formula supplies a domain, which holds at least one member.<RT·endnote>Standard first-order logic does not admit the empty domain, and the reason is visible in the formulas. Over an empty domain <RT·math>∀x \, F(x)</RT·math> would hold and <RT·math>∃x \, F(x)</RT·math> would fail, so <RT·math>(∀x \, F(x) → ∃x \, F(x))</RT·math> would not be valid; it is counted a validity of this calculus, and admitting the empty domain would cost that.</RT·endnote> It then binds, to each variable of the formula, a value of the kind that variable marks a place for: a predicate over the domain to each predicate symbol, of the matching number of arguments; a member of the domain to each name; a function over the domain to each function symbol; and a member of the domain to each free appearance of a domain variable, passing over the bound appearances, which the quantifier has already claimed.<RT·endnote>The notation is not settled across the sources surveyed in this book. Hilbert and Ackermann write <RT·math>(x)</RT·math> for the universal quantifier and <RT·math>(Ex)</RT·math> for the existential, and they mark negation with an overbar rather than with <RT·math>¬</RT·math>. A reader going to their book should be prepared for this.</RT·endnote> Take the Peano Numbers as the domain and bind <RT·math><</RT·math> to <RT·math>R</RT·math>: the formula <RT·math>∀x ∃y \, R(x, y)</RT·math> then states that every Peano Number has a larger one, and under that interpretation it holds. Every appearance in it is claimed by a quantifier, so the only things the interpretation had to give were the domain and the predicate.</p>
<p>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.</p>
</ol>
List <RT·Counter·read snapshot="List·first-order-predicate-logic_stack"></RT·Counter·read>. <RT·name>The first order predicate logic stack</RT·name>
</RT·Counter·step>
+ </RT·section>
+ <RT·section id="Section·Grounding·Second-order_predicate_calculus">
+ <RT·name>Second-order predicate calculus</RT·name>
<p>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 <RT·math>F</RT·math> and asks what follows, and no formula of that calculus ranges over the predicates themselves. The <RT·term>second-order predicate calculus</RT·term> lifts that restriction by admitting a second kind of claimable variable, the <RT·term>predicate variable</RT·term>, 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 <RT·math>∀F \, Φ</RT·math> the quantifier has claimed <RT·math>F</RT·math>, so no interpretation binds a predicate to it, and the quantifier runs it over the properties of the domain in the same way that <RT·math>∀x</RT·math> runs a domain variable over the domain itself.</p>
</RT·section>
<!------------------------------------------------------------------------------->
- <RT·section id="Section·grounding_logic_assessment">
- <RT·name>Assessment</RT·name>
+ <RT·section id="Section·Grounding·More_logic_terminology">
+ <RT·name>More logic terminology</RT·name>
+
+ <p>A formula that holds under every interpretation is <RT·term>valid</RT·term>, and in the propositional calculus such a formula is also called a <RT·term-em>tautology</RT·term-em>. A formula that holds under at least one interpretation is <RT·term>satisfiable</RT·term>. So <RT·math>((p ∧ p) ↔ p)</RT·math> is valid, <RT·math>(p ∧ q)</RT·math> is satisfiable and not valid, and <RT·math>(p ∧ ¬p)</RT·math> is neither. The two are duals: a formula is valid exactly when its negation is unsatisfiable.</p>
+
+ <p>Say a formula of the propositional calculus holds <RT·math>n</RT·math> 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 <RT·math>2^n</RT·math>. A <RT·term>truth table</RT·term> is an enumeration of them, one per row.</p>
- <p>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.</p>
+ <p>A <RT·term>derivation</RT·term> 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. Each is written with a symbol of its own, the <RT·term>double turnstile</RT·term> and the <RT·term>turnstile</RT·term>.</p>
+
+ <RT·Counter·step counter="RT·List·counter" id="List·logic_turnstile">
+ <RT·Counter·snapshot counter="RT·List·counter" snapshot="List·logic_assessment"></RT·Counter·snapshot>
+ <RT·dictionary key="notation" definition="reading">
+ <RT·entry key="⊨ Φ">Double turnstile. <RT·math>Φ</RT·math> holds under every interpretation.</RT·entry>
+ <RT·entry key="⊢ Φ">Turnstile. A derivation of <RT·math>Φ</RT·math> exists from the stated axioms and rules.</RT·entry>
+ </RT·dictionary>
+ List <RT·Counter·read snapshot="List·logic_turnstile"></RT·Counter·read>. <RT·name>The two assessments of a formula</RT·name>
+ </RT·Counter·step>
+
+ <p>A collection of axioms and rules is <RT·term>sound</RT·term> when everything it derives is valid, so <RT·math>⊢</RT·math> never outruns <RT·math>⊨</RT·math>, and <RT·term>complete</RT·term> when everything valid is derivable, so <RT·math>⊨</RT·math> never outruns <RT·math>⊢</RT·math>.<RT·endnote>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.</RT·endnote> A calculus together with a collection of axioms is a <RT·term>theory</RT·term>. 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.</p>
+
+ <p>The <RT·term>Entscheidungsproblem</RT·term> asks for a mechanical procedure that decides, in finitely many steps, whether a given formula is valid. Enumerating the <RT·math>2^n</RT·math> 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 <RT·Counter·read snapshot="Section·search-for_Turing-Machine"></RT·Counter·read> gives the history of the problem and its answer.<RT·endnote>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.</RT·endnote></p>
+
+ <p>Finally, the word <em>order</em> 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 <RT·term>orders of analysis</RT·term> set out in section <RT·Counter·read snapshot="Section·orders-of-analysis"></RT·Counter·read>, 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.</p>
+
+ </RT·section>
+
+ <!------------------------------------------------------------------------------->
+ <RT·section id="Section·Grounding·More_logic_terminology">
+ <RT·name>More logic terminology</RT·name>
<p>A formula that holds under every interpretation is <RT·term>valid</RT·term>, and in the propositional calculus such a formula is also called a <RT·term-em>tautology</RT·term-em>. A formula that holds under at least one interpretation is <RT·term>satisfiable</RT·term>. So <RT·math>((p ∧ p) ↔ p)</RT·math> is valid, <RT·math>(p ∧ q)</RT·math> is satisfiable and not valid, and <RT·math>(p ∧ ¬p)</RT·math> is neither. The two are duals: a formula is valid exactly when its negation is unsatisfiable.</p>
List <RT·Counter·read snapshot="List·logic_assessment"></RT·Counter·read>. <RT·name>The two assessments of a formula</RT·name>
</RT·Counter·step>
- <p>A collection of axioms and rules is <RT·term>sound</RT·term> when everything it derives is valid, so <RT·math>⊢</RT·math> never outruns <RT·math>⊨</RT·math>, and <RT·term>complete</RT·term> when everything valid is derivable, so <RT·math>⊨</RT·math> never outruns <RT·math>⊢</RT·math>.<RT·endnote>The turnstile <RT·math>⊢</RT·math> 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.</RT·endnote> A calculus together with a collection of axioms is a <RT·term>theory</RT·term>. 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 <RT·Counter·read snapshot="Section·search-for_Turing-Machine"></RT·Counter·read>.</p>
+ <p>A collection of axioms and rules is <RT·term>sound</RT·term> when everything it derives is valid, so <RT·math>⊢</RT·math> never outruns <RT·math>⊨</RT·math>, and <RT·term>complete</RT·term> when everything valid is derivable, so <RT·math>⊨</RT·math> never outruns <RT·math>⊢</RT·math>.<RT·endnote>The turnstile <RT·math>⊢</RT·math> 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.</RT·endnote> A calculus together with a collection of axioms is a <RT·term>theory</RT·term>. 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.</p>
<p>The <RT·term>Entscheidungsproblem</RT·term> asks for a mechanical procedure that decides, in finitely many steps, whether a given formula is valid. Enumerating the <RT·math>2^n</RT·math> 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 <RT·Counter·read snapshot="Section·search-for_Turing-Machine"></RT·Counter·read> gives the history of the problem and its answer.<RT·endnote>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.</RT·endnote></p>
</RT·section>
</RT·section>
+
</RT·section>
projects / TM-2026 / commitdiff