- <!DOCTYPE html>
+<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
</RT·section>
- <!--------------------------------------------------------------------------------->
+<!--------------------------------------------------------------------------------->
<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 with the all too common discussion of terminology, type face, and other grounding.</p>
- <p>In math spans and blocks, each container, such as a sequence or a set, is represented with a single capital letter, even when in Greek. Each object that is not a container is represented with a single lower case letter. Character pairs or full symbol names can also be used to represent math objects, in which case the same convention is followed for the first letter of the symbol, while the remaining letters are lower case. The context will make it clear if a non-letter Unicode character represents a container or a non-container.</p>
+ <RT·section id="Section·grounding_notation">
+ <RT·name>Notation</RT·name>
- <p>Code blocks and spans follow the RT code format conventions, which resemble the math conventions above but are not identical to them.<RT·endnote>For the complete specification, refer to RT-code-format.html and RT-code-format-Lisp.html located at https://github.com/Thomas-Walker-Lynch/RT-Style/tree/core-developer_branch/developer/document.</RT·endnote> For example, unlike for math scopes, comma-separated lists apply a space before the comma and bind the punctuation directly to the item being appended to the list:</p>
+ <p>In math spans and blocks, each container, such as a sequence or a set, is represented with a single capital letter, even when in Greek. Each object that is not a container is represented with a single lower case letter. Character pairs or full symbol names can also be used to represent math objects, in which case the same convention is followed for the first letter of the symbol, while the remaining letters are lower case. The context will make it clear if a non-letter Unicode character represents a container or a non-container.</p>
- <RT·Counter·step counter="RT·Code·counter" id="Code·comma-list_example">
- <RT·Counter·snapshot counter="RT·Code·counter" snapshot="Code·comma-list_example"></RT·Counter·snapshot>
- <RT·code>
- int x ,y ,z;
- </RT·code>
- Code <RT·Counter·read snapshot="Code·comma-list_example"></RT·Counter·read>. <RT·name>A horizontal comma-separated list</RT·name>
- </RT·Counter·step>
+ <p>Code blocks and spans follow the RT code format conventions, which resemble the math conventions above but are not identical to them.<RT·endnote>For the complete specification, refer to RT-code-format.html and RT-code-format-Lisp.html located at https://github.com/Thomas-Walker-Lynch/RT-Style/tree/core-developer_branch/developer/document.</RT·endnote> For example, unlike for math scopes, comma-separated lists apply a space before the comma and bind the punctuation directly to the item being appended to the list:</p>
- <p>Multi-level enclosures receive a single space of padding only on the outermost boundary:</p>
+ <RT·Counter·step counter="RT·Code·counter" id="Code·comma-list_example">
+ <RT·Counter·snapshot counter="RT·Code·counter" snapshot="Code·comma-list_example"></RT·Counter·snapshot>
+ <RT·code>
+ int x ,y ,z;
+ </RT·code>
+ Code <RT·Counter·read snapshot="Code·comma-list_example"></RT·Counter·read>. <RT·name>A horizontal comma-separated list</RT·name>
+ </RT·Counter·step>
- <RT·Counter·step counter="RT·Code·counter" id="Code·enclosure-padding_example">
- <RT·Counter·snapshot counter="RT·Code·counter" snapshot="Code·enclosure-padding_example"></RT·Counter·snapshot>
- <RT·code>
- if( f(g(x)) ){
- do_something();
- }
- </RT·code>
- Code <RT·Counter·read snapshot="Code·enclosure-padding_example"></RT·Counter·read>. <RT·name>Padding applied to the outermost enclosure only</RT·name>
- </RT·Counter·step>
+ <p>Multi-level enclosures receive a single space of padding only on the outermost boundary:</p>
- <p>Code identifiers follow a parallel convention, though what counts as a container differs from the mathematical case. In code, a container is a namespace, a module, or a type, i.e. something that holds definitions, and these are written in PascalCase. Every other identifier is snake-kebab_case, and that includes the data structures that hold elements rather than definitions, so a list or a dictionary carries a lower case name. Both separators are in use so that a hyphen binds tighter than an underscore, which establishes semantic precedence. An example of this is:</p>
+ <RT·Counter·step counter="RT·Code·counter" id="Code·enclosure-padding_example">
+ <RT·Counter·snapshot counter="RT·Code·counter" snapshot="Code·enclosure-padding_example"></RT·Counter·snapshot>
+ <RT·code>
+ if( f(g(x)) ){
+ do_something();
+ }
+ </RT·code>
+ Code <RT·Counter·read snapshot="Code·enclosure-padding_example"></RT·Counter·read>. <RT·name>Padding applied to the outermost enclosure only</RT·name>
+ </RT·Counter·step>
- <RT·Counter·step counter="RT·Code·counter" id="Code·identifier-separator_example">
- <RT·Counter·snapshot counter="RT·Code·counter" snapshot="Code·identifier-separator_example"></RT·Counter·snapshot>
- <RT·code>
- rounded_x-coordinate
- </RT·code>
- Code <RT·Counter·read snapshot="Code·identifier-separator_example"></RT·Counter·read>. <RT·name>A hyphen binding tighter than an underscore within an identifier</RT·name>
- </RT·Counter·step>
+ <p>Code identifiers follow a parallel convention, though what counts as a container differs from the mathematical case. In code, a container is a namespace, a module, or a type, i.e. something that holds definitions, and these are written in PascalCase. Every other identifier is snake-kebab_case, and that includes the data structures that hold elements rather than definitions, so a list or a dictionary carries a lower case name. Both separators are in use so that a hyphen binds tighter than an underscore, which establishes semantic precedence. An example of this is:</p>
- <p>Throughout, this text uses native Unicode characters rather than escape sequences. Where a mathematical or Greek symbol is wanted, the character itself appears, so the text carries 'δ' rather than <RT·code>\delta</RT·code>. This might lead to some small typesetting variations compared to what MathJax might otherwise have output.</p>
+ <RT·Counter·step counter="RT·Code·counter" id="Code·identifier-separator_example">
+ <RT·Counter·snapshot counter="RT·Code·counter" snapshot="Code·identifier-separator_example"></RT·Counter·snapshot>
+ <RT·code>
+ rounded_x-coordinate
+ </RT·code>
+ Code <RT·Counter·read snapshot="Code·identifier-separator_example"></RT·Counter·read>. <RT·name>A hyphen binding tighter than an underscore within an identifier</RT·name>
+ </RT·Counter·step>
- <p>The Unicode middle dot, ·, is used as an ad hoc namespace operator in identifiers. Hence <RT·code>N·x</RT·code> would be the variable <RT·code>x</RT·code> from the <RT·code>N</RT·code> namespace. This is a typographic symbol with a long history of use as a separator. It appears in dictionaries where words are broken into syllables, e.g. 'op·er·a·tor'. It is a letter of the Catalan alphabet, the <em>punt volat</em>, which distinguishes the geminate <RT·code>l·l</RT·code> of 'col·legi' from the digraph <RT·code>ll</RT·code>. And Japanese uses it, as the <em>nakaguro</em>, to separate the components of a transliterated foreign name. It is accepted in identifiers by modern C compilers,<RT·endnote>C11 permits the character anywhere in an identifier, including as the first character: it falls in the 00B7−00BA range of Annex D.1, and appears in none of the ranges disallowed initially in D.2. C23 restates the rule in terms of Unicode UAX #31, where the character belongs to Other_ID_Continue and so remains permitted, though no longer in first position. ISO/IEC 9899:2011, Annex D; ISO/IEC 9899:2024, §6.4.2.</RT·endnote> and it is part of the RT·gcc compiler mods as an ad hoc namespace operator.</p>
+ <p>Throughout, this text uses native Unicode characters rather than escape sequences. Where a mathematical or Greek symbol is wanted, the character itself appears, so the text carries 'δ' rather than <RT·code>\delta</RT·code>. This might lead to some small typesetting variations compared to what MathJax might otherwise have output.</p>
- <p>In the RT coding culture, we say that argument values are <em>given</em> to a function. Functions do not <em>take</em> arguments, as it is the caller that has authority over making the call, and thus over sending the arguments. A function is only said to <em>accept</em> or <em>reject</em> a value in the context of guard code evaluating argument validity, something it has authority to do. Similarly, machines, factories, and software <em>make</em> objects by assembling components they are given; they do not <em>create</em> them, since bringing components into being is not within an engineer's authority. That leaves 'creation' to imply a more fundamental synthesis outside the scope of engineering, perhaps done by artists or supernatural beings.</p>
+ <p>The Unicode middle dot, ·, is used as an ad hoc namespace operator in identifiers. Hence <RT·code>N·x</RT·code> would be the variable <RT·code>x</RT·code> from the <RT·code>N</RT·code> namespace. This is a typographic symbol with a long history of use as a separator. It appears in dictionaries where words are broken into syllables, e.g. 'op·er·a·tor'. It is a letter of the Catalan alphabet, the <em>punt volat</em>, which distinguishes the geminate <RT·code>l·l</RT·code> of 'col·legi' from the digraph <RT·code>ll</RT·code>. And Japanese uses it, as the <em>nakaguro</em>, to separate the components of a transliterated foreign name. It is accepted in identifiers by modern C compilers,<RT·endnote>C11 permits the character anywhere in an identifier, including as the first character: it falls in the 00B7−00BA range of Annex D.1, and appears in none of the ranges disallowed initially in D.2. C23 restates the rule in terms of Unicode UAX #31, where the character belongs to Other_ID_Continue and so remains permitted, though no longer in first position. ISO/IEC 9899:2011, Annex D; ISO/IEC 9899:2024, §6.4.2.</RT·endnote> and it is part of the RT·gcc compiler mods as an ad hoc namespace operator.</p>
+ </RT·section>
- <p>I have experimented with modern gender forms in technical language in past writings. For example, I used the plural-as-singular style in one piece, and was applauded by some, though categorized as illiterate by others. Since then, I have evolved a writing style that emphasizes using roles as subjects: the mathematician, the author, the programmer. Such subjects are singular, so for grammatical agreement, I use the <em>inclusive he</em>. It is structurally much cleaner to use <em>he</em> as inclusive of all people than it is to gray out an entire category of plural agreement pronouns by forcing words such as 'they' to take on a singular form. I use 'a person' when the subject is an unknown third party, who might even be an AI. I prefer this over the 'one' of 'One does this, or one does that', so that 'one' can be reserved to unambiguously refer to the number.</p>
+ <RT·section id="Section·grounding_usage">
+ <RT·name>Usage</RT·name>
- <p>In the prior edition of this book, the preface included a discussion on the meaning of the word 'may' according to RFC 2119, which fixes the requirement level key words used in specification writing. There is an important distinction between the 'may' of options or permission, and the more colloquial 'may' of probability. However, distinguishing between the two was too much of an ask of readers, most of whom skip the preface anyway. So in this edition, I avoid the temptation to use 'may' and replace it with a direct statement of what I mean. "It is of high probability that..." or "There are options for...". Directly saying what is meant, who would have thought of it? The RFC series has since narrowed the word further. RFC 8174 amended RFC 2119 so that the key words carry their defined meanings only when written in capitals, which leaves a lower case 'may' in an RFC with no normative force at all.<RT·endnote>Scott Bradner, <em>Key words for use in RFCs to Indicate Requirement Levels</em>, RFC 2119, March 1997. Barry Leiba, <em>Ambiguity of Uppercase vs Lowercase in RFC 2119 Key Words</em>, RFC 8174, May 2017.</RT·endnote></p>
+ <p>In the RT coding culture, we say that argument values are <em>given</em> to a function. Functions do not <em>take</em> arguments, as it is the caller that has authority over making the call, and thus over sending the arguments. A function is only said to <em>accept</em> or <em>reject</em> a value in the context of guard code evaluating argument validity, something it has authority to do. Similarly, machines, factories, and software <em>make</em> objects by assembling components they are given; they do not <em>create</em> them, since bringing components into being is not within an engineer's authority. That leaves 'creation' to imply a more fundamental synthesis outside the scope of engineering, perhaps done by artists or supernatural beings.</p>
- <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>
+ <p>I have experimented with modern gender forms in technical language in past writings. For example, I used the plural-as-singular style in one piece, and was applauded by some, though categorized as illiterate by others. Since then, I have evolved a writing style that emphasizes using roles as subjects: the mathematician, the author, the programmer. Such subjects are singular, so for grammatical agreement, I use the <em>inclusive he</em>. It is structurally much cleaner to use <em>he</em> as inclusive of all people than it is to gray out an entire category of plural agreement pronouns by forcing words such as 'they' to take on a singular form. I use 'a person' when the subject is an unknown third party, who might even be an AI. I prefer this over the 'one' of 'One does this, or one does that', so that 'one' can be reserved to unambiguously refer to the number.</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>In the prior edition of this book, the preface included a discussion on the meaning of the word 'may' according to RFC 2119, which fixes the requirement level key words used in specification writing. There is an important distinction between the 'may' of options or permission, and the more colloquial 'may' of probability. However, distinguishing between the two was too much of an ask of readers, most of whom skip the preface anyway. So in this edition, I avoid the temptation to use 'may' and replace it with a direct statement of what I mean. "It is of high probability that..." or "There are options for...". Directly saying what is meant, who would have thought of it? The RFC series has since narrowed the word further. RFC 8174 amended RFC 2119 so that the key words carry their defined meanings only when written in capitals, which leaves a lower case 'may' in an RFC with no normative force at all.<RT·endnote>Scott Bradner, <em>Key words for use in RFCs to Indicate Requirement Levels</em>, RFC 2119, March 1997. Barry Leiba, <em>Ambiguity of Uppercase vs Lowercase in RFC 2119 Key Words</em>, RFC 8174, May 2017.</RT·endnote></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>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>
- <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 id="Section·grounding_number-types">
+ <RT·name>Number types</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 equations, and sets the rules for modulus arithmetic. For example, encryption algorithms belong to Number Theory.</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>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>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>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>
+ <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 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>
+
+ <RT·section id="Section·grounding_logic">
+ <RT·name>Logic</RT·name>
+
+ <p>A <RT·term>proposition</RT·term> is a statement that takes no arguments and carries a truth value. It is not predicated upon anything, so settling it requires no variable 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.</p>
+
+ <p>The <RT·term>propositional calculus</RT·term>, also called propositional logic, begins with sentences of symbols. Some of the symbols carry a fixed meaning, and these are the connectives: <RT·math>∧</RT·math> (and), <RT·math>∨</RT·math> (or), <RT·math>¬</RT·math> (not), <RT·math>→</RT·math> (implies), and <RT·math>↔</RT·math> (if and only if), together with parentheses for grouping. The remaining symbols are left open, and these are the variables, written <RT·math>P</RT·math>, <RT·math>Q</RT·math>, <RT·math>R</RT·math>, each standing in the place where a proposition is later supplied. Formation rules settle which sentences of such symbols are well formed: a variable alone is well formed, a well formed sentence preceded by <RT·math>¬</RT·math> is well formed, and two of them joined by a binary connective and enclosed in parentheses are well formed. So <RT·math>(P ∧ ¬Q)</RT·math> is a sentence of the calculus and <RT·math>P ¬ ∧ Q</RT·math> is not. Nothing said so far concerns truth. A well formed sentence is an arrangement of symbols, and the calculus is the collection of such arrangements together with the rules that govern them. This is the logic of logic design, where the sentence is a gate network drawn before any signal has been applied to it.</p>
+
+ <p>An <RT·term>interpretation</RT·term> supplies what the open symbols lack. It gives each variable of a sentence a proposition, and since the connectives are defined as functions of truth values alone, an interpretation carries no more information than the truth value each such proposition holds. Let <RT·math>P</RT·math> be given "the clock line is high" and <RT·math>Q</RT·math> "the enable line is high"; the sentence <RT·math>(P ∧ ¬Q)</RT·math> then holds or fails according to those two truth values and according to nothing else. A sentence of <RT·math>n</RT·math> variables therefore admits <RT·math>2^n</RT·math> distinct interpretations, and this is what a truth table enumerates. A sentence that holds under every interpretation has the property of <RT·term>validity</RT·term>, and in the propositional calculus such a sentence is also called a <RT·term>tautology</RT·term>. A sentence that holds under at least one has the property of <RT·term>satisfiability</RT·term>. So <RT·math>(P ∧ P) ↔ P</RT·math> is valid, and it is valid without any proposition having been supplied for <RT·math>P</RT·math>, because the claim quantifies over the interpretations rather than resting within one. <RT·math>(P ∧ Q)</RT·math> is satisfiable and is not valid, and <RT·math>(P ∧ ¬P)</RT·math> is neither. The two properties are duals of each other: a sentence is valid exactly when its negation is unsatisfiable
+ <RT·endnote>This duality is why a decision procedure for the one is a decision procedure for the other. Hilbert and Ackermann state it in the passage of the 1928 book surveyed in section <RT·Counter·read snapshot="Section·search-for_Turing-Machine"></RT·Counter·read>, and they pose the Entscheidungsproblem in both forms.</RT·endnote>.
+ Because <RT·math>2^n</RT·math> is finite, tabulating every interpretation settles both questions and the tabulation terminates. This is why the <RT·term>Entscheidungsproblem</RT·term>, the problem of deciding validity by a mechanical procedure, was solved for the propositional calculus before it had a name. Section <RT·Counter·read snapshot="Section·search-for_Turing-Machine"></RT·Counter·read> gives its history.</p>
+
+ <p>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. A predicate is to a proposition what a function is to a constant. <RT·math>Prime(x)</RT·math> is a predicate of one argument, and giving it an argument yields a proposition: <RT·math>Prime(7)</RT·math> is true and <RT·math>Prime(8)</RT·math> is false. <RT·math>LessThan(x, y)</RT·math> is a predicate of two arguments, which is how a relation is written. The arguments are drawn from a domain set, and that domain is whatever mathematics cares to name: the Peano Numbers, the points of a plane, the strings over an alphabet. The arguments are not themselves logic values. Only the result of the predicate is a logic value.</p>
- <p>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.</p>
+ <p>The <RT·term>first-order predicate calculus</RT·term> also begins with sentences of symbols. Where the propositional calculus had two classes of symbol, those carrying a fixed meaning and those left open for an interpretation to supply, there are now three, because the open class divides in two. The fixed class gains the quantifiers, <RT·math>∀</RT·math> (for all) and <RT·math>∃</RT·math> (there exists), alongside the connectives and parentheses already in it. Of the open symbols, the <RT·term>individual variables</RT·term>, written <RT·math>x</RT·math>, <RT·math>y</RT·math>, <RT·math>z</RT·math>, stand where a member of a domain set is later supplied. The <RT·term>predicate letters</RT·term>, written <RT·math>F</RT·math>, <RT·math>G</RT·math>, <RT·math>R</RT·math>, each carry a fixed number of argument places and stand where a predicate of that many arguments is later supplied. The propositional variable is gone, having no work left to do: a predicate letter given its arguments occupies the place where a proposition once stood. The formation rules carry over, with two additions. A predicate letter applied to the right number of individual variables is a well formed sentence, and a quantifier followed by an individual variable and a well formed sentence is well formed. So <RT·math>∀x \, F(x)</RT·math> and <RT·math>∀x ∃y \, R(x, y)</RT·math> are sentences of the calculus.</p>
- <p>The first type of <RT·term>Turing Machine</RT·term> 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.</p>
+ <p>A quantifier <RT·term>claims</RT·term> the variable that follows it, and it claims every occurrence of that variable in the sentence to which it applies. In <RT·math>∀x \, F(x)</RT·math> the quantifier has claimed <RT·math>x</RT·math>. A claimed variable is spoken for, and nothing supplies it a value, because the quantifier is what runs it over the domain, passing the sentence over every member of the domain in the universal case and over at least one member in the existential case. A variable that no quantifier has claimed is left for an interpretation to supply. So there are two fates for a variable in a sentence, claimed by a quantifier or supplied by an interpretation, and no variable meets both.</p>
- <p>The second type is the <RT·term>Universal Turing Machine</RT·term>, 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.</p>
+ <p>An interpretation of a first-order sentence therefore supplies three things. It supplies a domain set. It supplies a predicate over that domain for each predicate letter, of the matching number of arguments, since in this calculus no quantifier can claim a predicate letter and every one of them awaits an interpretation. And it supplies a member of the domain for each individual variable that no quantifier has claimed, passing over the ones 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>LessThan</RT·math> for <RT·math>R</RT·math>: the sentence <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. Both of its individual variables were claimed by quantifiers, so the only things the interpretation had to supply were the domain and the predicate. 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 <RT·math>2^n</RT·math> assignments of truth values. Here it selects a domain of any size whatever, and then a predicate over that domain for each letter, 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 <RT·Counter·read snapshot="Section·search-for_Turing-Machine"></RT·Counter·read>.</p>
- <p>The <RT·term>RT Machine</RT·term> 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.</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. A domain of <RT·math>n</RT·math> members therefore carries <RT·math>2^n</RT·math> properties. 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.</p>
+
+ <p>In the first-order calculus a quantifier claims individual variables and nothing else. Every predicate letter awaits an interpretation, so a person supplies a particular predicate for <RT·math>F</RT·math> and asks what follows, and no sentence of that calculus ranges over the predicates themselves. The <RT·term>second-order predicate calculus</RT·term> lifts that restriction by letting a quantifier claim a predicate letter as well. The two fates are the same as before, and they now apply to a second kind of symbol. In <RT·math>∀F \, \Phi</RT·math> the quantifier has claimed <RT·math>F</RT·math>, so no interpretation supplies a predicate for it, and the quantifier runs it over the properties of the domain in the same way that <RT·math>∀x</RT·math> runs an individual variable over the domain itself. An interpretation of a second-order sentence supplies a domain, together with a predicate for each predicate letter that no quantifier has claimed.</p>
+
+ <p>The gain is that a statement about all properties becomes a single statement. Mathematical induction is the example that matters here. In the first-order calculus, induction is written as an infinite family of axioms, one for each sentence 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, <RT·math>∀F \, \big( (F(0) ∧ ∀x \, (F(x) → F(S(x)))) → ∀x \, F(x) \big)</RT·math>, where <RT·math>S(x)</RT·math> is the successor of <RT·math>x</RT·math>. The outermost quantifier has claimed the predicate letter, so the axiom states that any property holding of zero and carried from each Peano Number to its successor holds of every Peano Number.</p>
+
+ <p>The cost is paid at the quantifier. The second-order axioms for arithmetic, induction among them, pin down the Peano Numbers so tightly that every question of arithmetic is settled by them. A proof procedure is a mechanical enumeration of derivations, so a complete proof procedure for the second-order calculus would make the truths of arithmetic mechanically enumerable. Gödel's result forbids exactly that, as section <RT·Counter·read snapshot="Section·search-for_Turing-Machine"></RT·Counter·read> sets out. So under the standard reading there is no effective set of rules deriving every second-order validity, and provability and truth part company. A weaker reading is available, under which the predicate quantifier ranges only over a collection of properties named in advance, and this restores a complete proof procedure at the cost of the expressive power that was the point of the exercise.</p>
+
+ <p>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 the quantifiers range over: individuals at the first order, and properties of individuals 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. 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_machines">
+ <RT·name>Machines</RT·name>
+
+ <p>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.</p>
+
+ <p>The first type of <RT·term>Turing Machine</RT·term> 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.</p>
+
+ <p>The second type is the <RT·term>Universal Turing Machine</RT·term>, 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.</p>
+
+ <p>The <RT·term>RT Machine</RT·term> 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.</p>
+ </RT·section>
</RT·section>
projects / TM-2026 / commitdiff