<RT·section id="Section·exordium">
<RT·name>Exordium</RT·name>
- <p>My colleagues in computer arithmetic work tirelessly to confirm Schopenhauer's thesis, so I am left with only the easy problems no one else wants.</p>
-
- <p>This book would not exist without the encouragement of my wife. While cousins brought their husbands to family events, she sat by herself as I remained home in the company of computation theory. She is a beautiful, charming woman. I count myself fortunate not to be wearing horns.</p>
+ <p>My colleagues in computer arithmetic work tirelessly to confirm Schopenhauer's thesis, so I am left to chose among only unfunded inconsequential problems that no one else wants.</p>
<p>So perhaps we can discuss this one. Turing began with a Naturalist model, a clerk at a desk, yet the machine he described cannot be built. What follows completes the foundation he began. The subject of Computational Naturalism lies at the intersection of number theory, numerical analysis, computation theory, and computer architecture.</p>
- <p>The RT Iterator Library was developed at Reasoning Technology Inc. It is a first step toward a computer language for increased security and behavioral introspection.</p>
+ <p>This book would not exist without the encouragement of my wife. While cousins brought their husbands to family events, she sat by herself as I remained home in the company of computation theory. She is a beautiful, charming woman. I count myself fortunate not to be wearing horns.</p>
</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>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_notation">
<RT·name>Notation</RT·name>
<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>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>
+ <!--------------------------------------------------------------------------------->
<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>A <RT·term>symbol</RT·term> 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 <RT·term>representation</RT·term> 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 <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 <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 <em>true</em> and <em>false</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>The <RT·term>connective</RT·term>s are symbols, and instances of their representations are these: <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). Alongside them stand the parentheses, <RT·math>(</RT·math> and <RT·math>)</RT·math>, 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 <RT·math>∧</RT·math> gives true exactly when both of the truth values given to it are true, <RT·math>¬</RT·math> gives the truth value it was not given, and so on for the rest.</p>
+
+ <p>Beside the connectives stand the <RT·term>proposition symbol</RT·term>s. Common examples of their representations include <RT·math>p</RT·math>, <RT·math>q</RT·math>, and <RT·math>r</RT·math>. 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.<RT·endnote>Many texts call these <em>propositional variables</em>. 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 <RT·Counter·read snapshot="Section·grounding_notation"></RT·Counter·read>, 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.</RT·endnote></p>
+
+ <p>Symbol instances are strung together according to the <RT·term>formation rules</RT·term>, and what the rules build is called a <RT·term>formula</RT·term>. The rules are three, and the third is what closes the definition. The Greek letters <RT·math>Φ</RT·math> and <RT·math>Ψ</RT·math> are used below to represent whole formulas. They belong to this discussion rather than to the calculus being discussed.</p>
+
+ <RT·Counter·step counter="RT·List·counter" id="List·propositional_formation-rules">
+ <RT·Counter·snapshot counter="RT·List·counter" snapshot="List·propositional_formation-rules"></RT·Counter·snapshot>
+ <ol>
+ <li>A proposition symbol standing alone is a formula. Such a formula is called <RT·term>atomic</RT·term>, meaning the formation rules cannot break it down further.</li>
+ <li>If <RT·math>Φ</RT·math> and <RT·math>Ψ</RT·math> are formulas, then <RT·math>¬Φ</RT·math> is a formula, and so is <RT·math>(Φ ∘ Ψ)</RT·math> for each binary connective <RT·math>∘</RT·math>.</li>
+ <li>Nothing is a formula except by finitely many applications of rules 1 and 2.</li>
+ </ol>
+ List <RT·Counter·read snapshot="List·propositional_formation-rules"></RT·Counter·read>. <RT·name>Formation rules of the propositional calculus</RT·name>
+ </RT·Counter·step>
+
+ <p>For example, <RT·math>(p ∧ ¬q)</RT·math> is a formula. Rule 1 supplies the base of the construction and rule 2 supplies the negation, <RT·math>¬q</RT·math>, then rule 2 applied again supplies the connective, <RT·math>p ∧ ¬q</RT·math>. 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.</p>
+
+ <p>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 <em>well formed formula</em>, and that for a <em>malformed formula</em>. Take for example the string <RT·math>p ¬ ∧ q</RT·math>. 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 <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 terms are used interchangeably, so the adjective <em>well formed</em> 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. <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.</RT·endnote><RT·endnote>A C++ committee borrowed the terminology for a <em>well formed program</em> 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.</RT·endnote></p>
+
+ <p>An <RT·term>interpretation</RT·term> 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 <RT·math>p</RT·math> be given "the clock line is high" and <RT·math>q</RT·math> "the enable line is high"; whether <RT·math>(p ∧ ¬q)</RT·math> 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.</p>
+
+ <p>A <RT·term>propositional calculus</RT·term> therefore consists of math objects that occur on an abstraction stack, which collects what has been said so far.</p>
+
+ <RT·Counter·step counter="RT·List·counter" id="List·propositional_stack">
+ <RT·Counter·snapshot counter="RT·List·counter" snapshot="List·propositional_stack"></RT·Counter·snapshot>
+ <ol reversed start="2">
+ <li>interpretation
+ <ul>
+ <li>supplies a proposition, and so a truth value, for each proposition symbol</li>
+ </ul>
+ </li>
+ <li>formula
+ <ul>
+ <li>built from the level 0 symbols by the formation rules</li>
+ </ul>
+ </li>
+ <li>symbol
+ <ul>
+ <li>fixed: connective, parenthesis</li>
+ <li>awaiting an interpretation: proposition symbol</li>
+ </ul>
+ </li>
+ </ol>
+ List <RT·Counter·read snapshot="List·propositional_stack"></RT·Counter·read>. <RT·name>The propositional logic abstraction stack</RT·name>
+ </RT·Counter·step>
+
+ <p>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 <em>primitive</em>. Hardware designers might think of them as being <em>native</em>, 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.</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>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>LessThan(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. Only the result of the predicate is a truth value.</p>
+
+ <p>The <RT·term>first-order predicate calculus</RT·term> also begins with expressions of 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 awaiting group, whose members each mark a place for something an interpretation later supplies, now holds three kinds of symbol: 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. The third group is new. A <RT·term>variable</RT·term> is a symbol that a quantifier is able to claim, and 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>.<RT·endnote>Many texts call the <RT·math>p</RT·math>, <RT·math>q</RT·math>, <RT·math>r</RT·math> of the propositional calculus <em>propositional variables</em>. 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.</RT·endnote> 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.</p>
+
+ <RT·Counter·step counter="RT·List·counter" id="List·first-order_formation-rules">
+ <RT·Counter·snapshot counter="RT·List·counter" snapshot="List·first-order_formation-rules"></RT·Counter·snapshot>
+ <ol>
+ <li>A predicate symbol of <RT·math>n</RT·math> places applied to <RT·math>n</RT·math> terms is a formula, and it is atomic.</li>
+ <li>If <RT·math>Φ</RT·math> and <RT·math>Ψ</RT·math> are formulas, then <RT·math>¬Φ</RT·math> is a formula, and so is <RT·math>(Φ ∘ Ψ)</RT·math> for each binary connective <RT·math>∘</RT·math>.</li>
+ <li>If <RT·math>Φ</RT·math> is a formula and <RT·math>x</RT·math> is a domain variable, then <RT·math>∀x \, Φ</RT·math> and <RT·math>∃x \, Φ</RT·math> are formulas.</li>
+ <li>No expression is a formula except by finitely many applications of rules 1 through 3.</li>
+ </ol>
+ List <RT·Counter·read snapshot="List·first-order_formation-rules"></RT·Counter·read>. <RT·name>Formation rules of the first-order predicate calculus</RT·name>
+ </RT·Counter·step>
+
+ <p>So <RT·math>∀x \, F(x)</RT·math> and <RT·math>∀x ∃y \, R(x ,y)</RT·math> are formulas of the calculus.</p>
+
+ <p>A quantifier <RT·term>claims</RT·term> 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 <RT·term>scope</RT·term>. Where a variable appears within the scope of a quantifier claiming it, that appearance is <RT·term>bound</RT·term>; where it appears within no such scope, that appearance is <RT·term>free</RT·term>.<RT·endnote>The words <em>bound</em> and <em>free</em> are the standard ones, and are given here so that a reader can find the literature. The word <em>claims</em> is used alongside them in this book because it names the agency, which is what the reader needs to see.</RT·endnote> 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.</p>
+
+ <p>The fates belong to appearances and not to variables, and a reader who forgets that will be caught by two ordinary formulas. In <RT·math>∀x \, (F(x) ∧ ∃x \, G(x))</RT·math> the inner quantifier claims the appearance inside <RT·math>G</RT·math>, 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 <RT·math>(F(x) ∧ ∀x \, G(x))</RT·math> 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 <RT·term>hygiene</RT·term> 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.</p>
+
+ <p>Here at last is the word set aside earlier. A <RT·term>sentence</RT·term> is a formula in which no variable appears free. So <RT·math>∀x ∃y \, R(x ,y)</RT·math> is a sentence, and <RT·math>∃y \, R(x ,y)</RT·math> 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.</p>
+
+ <p>An interpretation of a first-order formula supplies 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 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
+ <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. 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.</p>
+
+ <p>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 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 <RT·Counter·read snapshot="Section·search-for_Turing-Machine"></RT·Counter·read>. 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.</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>
+
+ <RT·Counter·step counter="RT·List·counter" id="List·first-order-predicate-logic_stack">
+ <RT·Counter·snapshot counter="RT·List·counter" snapshot="List·first-order-predicate-logic_stack"></RT·Counter·snapshot>
+ <ol reversed start="2">
+ <li>interpretation
+ <ul>
+ <li>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</li>
+ </ul>
+ </li>
+ <li>formula
+ <ul>
+ <li>a quantifier in it claims a domain variable</li>
+ <li>a formula with no free appearance is a sentence</li>
+ </ul>
+ </li>
+ <li>symbol
+ <ul>
+ <li>fixed: connective, parenthesis, quantifier</li>
+ <li>awaiting an interpretation: predicate symbol, name, function symbol</li>
+ <li>claimable by a quantifier: domain variable</li>
+ </ul>
+ </li>
+ </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>
- <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>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. That correspondence counts two predicates holding of the same members as the same property, which is a decision and not a discovery.<RT·endnote>The decision is 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. Nothing in the calculus below is able to tell them apart, and nothing in it needs to.</RT·endnote> 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>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>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 <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 variable, the <RT·term>predicate variable</RT·term>, 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 <RT·math>∀F \, Φ</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 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.</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>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:</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><RT·math>∀F \, \big( (F(0) ∧ ∀x \, (F(x) → F(s(x)))) → ∀x \, F(x) \big)</RT·math></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>where <RT·math>0</RT·math> is a name marking the place of zero and <RT·math>s</RT·math> 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.</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>One cell of the abstraction stack changes, and it is the cell at level 1.</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>
+ <RT·Counter·step counter="RT·List·counter" id="List·second-order-predicate-logic_stack">
+ <RT·Counter·snapshot counter="RT·List·counter" snapshot="List·second-order-predicate-logic_stack"></RT·Counter·snapshot>
+ <ol reversed start="2">
+ <li>interpretation
+ <ul>
+ <li>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</li>
+ </ul>
+ </li>
+ <li>formula
+ <ul>
+ <li>a quantifier in it claims a domain variable or a predicate variable</li>
+ <li>a formula with no free appearance of either kind is a sentence</li>
+ </ul>
+ </li>
+ <li>symbol
+ <ul>
+ <li>fixed: connective, parenthesis, quantifier</li>
+ <li>awaiting an interpretation: predicate symbol, name, function symbol</li>
+ <li>claimable by a quantifier: domain variable, predicate variable</li>
+ </ul>
+ </li>
+ </ol>
+ List <RT·Counter·read snapshot="List·second-order-predicate-logic_stack"></RT·Counter·read>. <RT·name>The second order predicate logic stack</RT·name>
+ </RT·Counter·step>
- <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 paid for. Read <RT·math>∀F</RT·math> as running over every property of the domain, which is the reading intended above and is called the <RT·term>standard semantics</RT·term>, 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 <RT·math>⊨</RT·math> outruns <RT·math>⊢</RT·math> permanently.<RT·endnote>The alternative is to let an interpretation nominate a smaller collection of properties for the quantifier to run over, which is the <em>Henkin semantics</em>. 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", <em>Journal of Symbolic Logic</em> 15, no. 2 (1950): 81−91.</RT·endnote> 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.</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 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. 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>
- <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 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.</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·section>
- <RT·name>The software layer</RT·name>
+ <RT·name>Symbol</RT·name>
+
+ <RT·section>
+ <RT·name>Natural Symbol</RT·name>
+
+ <p>The design for the RT Machine was given in chapter <RT·Counter·read snapshot="Section·RT_machine-design"></RT·Counter·read>. On that machine there was a column of patch panel holes said to be symbols for gating next state transitions. The presence of a symbol could be ascertained by its effect on the machine by observing the indicator lights, or more directly if the observer is allowed and facilitated to probe the machine with a voltage meter. Alternatively, the symbols could be enumerated in the abstract, as the maker of the control panel did, when he wrote symbol names next to each of the symbol holes. These are all natural actions. When there are merely two such symbols the machine is said to be a "binary" machine.
+ </p>
+ </RT·section>
<RT·section>
- <RT·name>Symbol in mathematics</RT·name>
+ <RT·name>Conventionally defined symbol</RT·name>
<p>
- A <RT·term>symbol</RT·term> is a distinct mathematical object capable of being instantiated. Within a given context, any instance of a specific symbol evaluates as equal to any other instance of that identical symbol, and evaluates as not equal to any instance of a different symbol.
+ A <RT·term>symbol</RT·term> is a distinct mathematical object capable of being instantiated. Within a given context, any instance of a specific symbol evaluates as equal to any other instance of that identical symbol, and evaluates as not equal to any instance of a different symbol. (Here we speak at the metamathematical level, where the objects being compared are the symbol instances themselves, rather than anything that might be <RT·term>bound</RT·term> to the symbol. <RT·term>binding</RT·term> is discussed in section <RT·Counter·read snapshot="Section·binding"></RT·Counter·read>.)
</p>
<p>
<p>
It follows from this definition that the distinct equivalence classes can be used as a proxy for the instantiable objects themselves. That is, a person can name either the instantiable object or the equivalence class, and then through this correspondence, find the other.
</p>
-
</RT·section>
<RT·section id="Section·symbol_in-computing">
- <RT·name>Symbol in computing</RT·name>
+ <RT·name>Naturally derived Math Symbol</RT·name>
<p>
- In the context of realized machines, the symbol itself can be defined as a factory that produces symbol instances. A new symbol instance of the given symbol is then made, say, by calling the factory's <RT·code>make</RT·code> function. All of the symbol instances made by the factory constitute the members of the corresponding equivalence class.
+ Because the RT Machine runs programs, it is possible to extend the notion of the Natural Symbol to that of the symbol of mathematics. Accordingly, the symbol of mathematics is defined as a program that produces symbol instances. A new symbol instance of the given symbol is then made, say, by calling a symbol factory's <RT·code>make</RT·code> function. All of the symbol instances made by the factory constitute the members of corresponding 'made by' equivalence class.
</p>
<p>
</RT·Counter·step>
</RT·section>
+ </RT·section>
+
+ <!--------------------------------------------------------------------------------->
+ <RT·section id="Section·binding">
+ <RT·name>Binding</RT·name>
<RT·section>
<RT·name>Property</RT·name>
</RT·section>
- <RT·section>
- <RT·name>Tape</RT·name>
+ </RT·section>
- <p>
- A tape is a set containing exactly one leftmost cell and an infinite number of medial cells. For each cell in the set, called cell A, if cell A has a right neighbor that is cell B, then cell B's left neighbor is cell A. Similarly, if cell A has a left neighbor of cell B, then cell B's right neighbor is cell A. Furthermore, any cell in the set must be reachable by traversing right neighbors starting from the leftmost cell, in a finite number of steps.
- </p>
+ <!--------------------------------------------------------------------------------->
+ <RT·section>
+ <RT·name>Mathematical Tape</RT·name>
- <p>
- To say that a tape is infinite, and to simultaneously require that any cell can be reached in a finite number of steps, means that after reaching said cell, there will always be further cells to the right. Consequently, though <em>any</em> cell can be reached in finite hops starting at the leftmost cell, a finite traversal of the tape can not visit <em>all</em> of the cells. This seeming contradiction is at the very heart of the definition of the countable infinity in mathematics.
- </p>
+ <p>The RT Machine is a natural object. We observe its mechanisms, name its parts, and then find symbol representation for them so as to facilitate introspection. In short, we build a model.</p>
- In conventional computation theory, once a tape is defined, the cell neighbor properties values are fixed. Cells don't move, new cells cannot be added, and cells existing on the tape cannot be removed. This fits the definition of a <RT·term>space</RT·term>, so we can say that a Turing Machine tape has a constant, fixed, linear <RT·term>topology</RT·term>. This permanence of cells matches the reality of hardware memories. On the other hand, it does not track well with general memory containers such as linked lists where <RT·term>destructive</RT·term> operations are often permitted.
- </p>
+ <p>
+ A tape is a set containing exactly one leftmost cell and an infinite number of medial cells. For each cell in the set, called cell A, if cell A has a right neighbor that is cell B, then cell B's left neighbor is cell A. Similarly, if cell A has a left neighbor of cell B, then cell B's right neighbor is cell A. Furthermore, any cell in the set must be reachable by traversing right neighbors starting from the leftmost cell, in a finite number of steps.
+ </p>
- Nor can a cell data property be removed; however, unlike for cell neighbor property values, the cell data property value can be changed while the Turing Machine is running. In fact some people would say this is the whole point of running a Turing Machine.
- </p>
+ <p>
+ To say that a tape is infinite, and to simultaneously require that any cell can be reached in a finite number of steps, means that after reaching said cell, there will always be further cells to the right. Consequently, though <em>any</em> cell can be reached in finite hops starting at the leftmost cell, a finite traversal of the tape can not visit <em>all</em> of the cells. This seeming contradiction is at the very heart of the definition of the countable infinity in mathematics.
+ </p>
- An empty tape is filled with empty symbols. However, as we noted above, a Turing Machine cannot visit all the cells on a tape, so a Turing Machine cannot erase a tape in advance for another Turing Machine to use. Say a Turing Machine tried to erase a tape by writing the empty symbol, then stepping right, then repeating. At some point it must halt. When it halts some number of cells will have been written with the empty symbols, but there will be further cells to the right of the cell the machine halted at, which have not yet been erased. So for example, if a machine wrote 10 cells with the empty symbol, then it might be the case that the prior user of the tape had written data to 11 of the cells. Without historical knowledge the eraser machine can not know where to stop. So here we see another meaning of infinity, it speaks to the situation of not having historical knowledge. And thus, we are left to decree into existence an empty tape, or as the mathematicians say, empty tapes are available <em>by definition</em>.
- </p>
+ <p>
+ In conventional computation theory, once a tape is defined, the cell neighbor properties values are fixed. Cells don't move, new cells cannot be added, and cells existing on the tape cannot be removed. This fits the definition of a <RT·term>space</RT·term>, so we can say that a Turing Machine tape has a constant, fixed, linear <RT·term>topology</RT·term>. This permanence of cells matches the reality of hardware memories. On the other hand, it does not track well with general memory containers such as linked lists where <RT·term>destructive</RT·term> operations are often permitted.
+ </p>
- <p>
- Mathematically, a Turing Machine tape is a specialized path graph. The neighbor properties are the edges. In this special form, properties are attached to the edges. A Turing Machine has a clock based state controller. Taking a step is an atomic operation. The machine is either in state <RT·math>q_i</RT·math> or in state <RT·math>q_{i+1}</RT·math>, there is no mathematical meaning given to the concept of <em>during a step</em>, which is why no properties are added to the edges of the tape path graph. This is not to say that some analysis of a Turing Machine program won't take pairs of nodes from the path graph and give them meaning, thus effectively giving properties to the arcs. However, this would not be part of the machine definition, such a program must go through the additional effort of making node pairs, because the machine itself does not provide the program with a feature for attaching properties directly to the neighbor property itself.</p>
+ <p>
+ Nor can a cell data property be removed; however, unlike for cell neighbor property values, the cell data property value can be changed while the Turing Machine is running. In fact some people would say this is the whole point of running a Turing Machine.
+ </p>
- <p>An example of a non-Turing tape like model is the Emacs vertical line cursor model, where a cursor is said to be between characters. An ASCII file offers no such feature as 'in between' characters. Like a Turing Machine tape, a medial character in an ASCII file has a left neighbor and a right neighbor character. Any attempt to represent an in between cursor within the file itself would require inserting more characters into the file under the same model of every medial character having a left and a right character. Consequently, though emacs presents a model where cursor is located in between two characters, this model is only due to the interpretation of the functions' actual effects presented to users in the documentation. For example, instead of saying a cursor is located upon a character, and that inserting a character inserts the character to the right of the given character, the manual gives the description that the new character is inserted at the cursor location, where said cursor is in between the given character and its right neighbor. Thus the documentation presents the user with one model, which by necessity of using standard library calls to work with files, is built upon another model.</p>
+ <p>
+ An empty tape is filled with empty symbols. However, as we noted above, a Turing Machine cannot visit all the cells on a tape, so a Turing Machine cannot erase a tape in advance for another Turing Machine to use. Say a Turing Machine tried to erase a tape by writing the empty symbol, then stepping right, then repeating. At some point it must halt. When it halts some number of cells will have been written with the empty symbols, but there will be further cells to the right of the cell the machine halted at, which have not yet been erased. So for example, if a machine wrote 10 cells with the empty symbol, then it might be the case that the prior user of the tape had written data to 11 of the cells. Without historical knowledge the eraser machine can not know where to stop. So here we see another meaning of infinity, it speaks to the situation of not having historical knowledge. And thus, we are left to decree into existence an empty tape, or as the mathematicians say, empty tapes are available <em>by definition</em>.
+ </p>
+ <p>
+ Mathematically, a Turing Machine tape is a specialized path graph. The neighbor properties are the edges. In this special form, properties are attached to the edges. A Turing Machine has a clock based state controller. Taking a step is an atomic operation. The machine is either in state <RT·math>q_i</RT·math> or in state <RT·math>q_{i+1}</RT·math>, there is no mathematical meaning given to the concept of <em>during a step</em>, which is why no properties are added to the edges of the tape path graph. This is not to say that some analysis of a Turing Machine program won't take pairs of nodes from the path graph and give them meaning, thus effectively giving properties to the arcs. However, this would not be part of the machine definition, such a program must go through the additional effort of making node pairs, because the machine itself does not provide the program with a feature for attaching properties directly to the neighbor property itself.</p>
+ <p>An example of a non-Turing tape like model is the Emacs vertical line cursor model, where a cursor is said to be between characters. An ASCII file offers no such feature as 'in between' characters. Like a Turing Machine tape, a medial character in an ASCII file has a left neighbor and a right neighbor character. Any attempt to represent an in between cursor within the file itself would require inserting more characters into the file under the same model of every medial character having a left and a right character. Consequently, though emacs presents a model where cursor is located in between two characters, this model is only due to the interpretation of the functions' actual effects presented to users in the documentation. For example, instead of saying a cursor is located upon a character, and that inserting a character inserts the character to the right of the given character, the manual gives the description that the new character is inserted at the cursor location, where said cursor is in between the given character and its right neighbor. Thus the documentation presents the user with one model, which by necessity of using standard library calls to work with files, is built upon another model.</p>
- </RT·section>
</RT·section>
<!--------------------------------------------------------------------------------->
<!-- LocalWords: Hopcroft Ullman endnote unformatted dereference
LocalWords: computable cardinality uniquifier namespace
<!-- LocalWords: Entscheidungsproblem metamathematics
+<!-- LocalWords: metamathematical
+ -->
-->
-->
projects / TM-2026 / commitdiff