Incompleteness
Read as: the tuple containing two, d sub one, d sub two, the Goedel number of capital A and capital B, zero, and k
Means: the tuple containing two, d sub one, d sub two, the Goedel number of capital A and capital B, zero, and k
Read as: delta sub three
Means: delta sub three
Read as: Component zero of d equals one, and there exists an a less than d such that both of the following hold. Discharge of a, component one of d, and Discharge Label of d holds. End Formula of d equals the code obtained by concatenating, in order, the code of an opening parenthesis, a, the code of the conditional symbol, End Formula of component one of d, and the code of a closing parenthesis
Means: Component zero of d equals one, and there exists an a less than d such that both of the following hold. Discharge of a, component one of d, and Discharge Label of d holds. End Formula of d equals the code obtained by concatenating, in order, the code of an opening parenthesis, a, the code of the conditional symbol, End Formula of component one of d, and the code of a closing parenthesis
Read as: the Open Assumption predicate
Means: the Open Assumption predicate
Read as: n equals zero
Means: n equals zero
Read as: the variable v subscript three
Means: the variable v subscript three
Read as: s
Means: s
Read as: k equals the length of the sequence coded by x
Means: k equals the length of the sequence coded by x
Read as: the symbol code of v subscript five equals the code of the sequence one, five, which equals two squared times three to the sixth power
Means: the symbol code of v subscript five equals the code of the sequence one, five, which equals two squared times three to the sixth power
Read as: Component zero of d equals one, and Discharge Label of d equals zero, and there exist a, x, and t, each less than d, such that all of the following hold. t is a closed term code. x is a variable code. The substitution function at a, t, and x equals End Formula of component one of d. End Formula of d equals the code obtained by concatenating the code of the existential quantifier symbol, x, and a, in that order
Means: Component zero of d equals one, and Discharge Label of d equals zero, and there exist a, x, and t, each less than d, such that all of the following hold. t is a closed term code. x is a variable code. The substitution function at a, t, and x equals End Formula of component one of d. End Formula of d equals the code obtained by concatenating the code of the existential quantifier symbol, x, and a, in that order
Read as: Is Axiom of n
Means: Is Axiom of n
Read as: the symbol code of s equals the code of the sequence four, n, i
Means: the symbol code of s equals the code of the sequence four, n, i
Read as: for every i less than the length of the sequence of subtree codes for d, Correct holds of entry i of that sequence
Means: for every i less than the length of the sequence of subtree codes for d, Correct holds of entry i of that sequence
Read as: the Goedel number of the one symbol variable term v subscript i
Means: the Goedel number of the one symbol variable term v subscript i
Read as: the term code relation Term applied to x
Means: the term code relation Term applied to x
Read as: u
Means: u
Read as: n equals two
Means: n equals two
Read as: A with t substituted for every free occurrence of x
Means: A with t substituted for every free occurrence of x
Read as: the element at position k minus one in the sequence coded by y equals x
Means: the element at position k minus one in the sequence coded by y equals x
Read as: two closing parenthesis symbols
Means: two closing parenthesis symbols
Read as: two raised to the power k subscript zero plus one, times three raised to the power k subscript one plus one, and so on, ending with p subscript n minus one raised to the power k subscript n minus one plus one
Means: two raised to the power k subscript zero plus one, times three raised to the power k subscript one plus one, and so on, ending with p subscript n minus one raised to the power k subscript n minus one plus one
Read as: p
Means: p
Read as: Follows By right universal quantifier of p
Means: Follows By right universal quantifier of p
Read as: the coded concatenation of three strings: the string consisting of the predicate symbol P with index j and arity n followed by left parenthesis; the comma separated argument string with code flatten of z; and the one symbol string right parenthesis
Means: the coded concatenation of three strings: the string consisting of the predicate symbol P with index j and arity n followed by left parenthesis; the comma separated argument string with code flatten of z; and the one symbol string right parenthesis
Read as: End Sequent of x
Means: End Sequent of x
Read as: universal quantifier introduction
Means: universal quantifier introduction
Read as: the symbols falsity, not, or, and, if then, for all, there exists, equality, left parenthesis, right parenthesis, and comma
Means: the symbols falsity, not, or, and, if then, for all, there exists, equality, left parenthesis, right parenthesis, and comma
Read as: x equals
Means: x equals
Read as: j
Means: j
Read as: The tuple has three entries in proof line order. First, the Goedel number of the formula if capital B then either capital B or capital A. Second, the Goedel number of the formula whose antecedent is if capital B then either capital B or capital A, and whose consequent is if capital A then, if capital B then either capital B or capital A. Third, the Goedel number of the formula if capital A then, if capital B then either capital B or capital A.
Means: The tuple has three entries in proof line order. First, the Goedel number of the formula if capital B then either capital B or capital A. Second, the Goedel number of the formula whose antecedent is if capital B then either capital B or capital A, and whose consequent is if capital A then, if capital B then either capital B or capital A. Third, the Goedel number of the formula if capital A then, if capital B then either capital B or capital A.
Read as: d
Means: d
Read as: Assum of x, d, and n
Means: Assum of x, d, and n
Read as: nine
Means: nine
Read as: n
Means: n
Read as: s equals the Goedel number of the sequent with Gamma on the left and Delta on the right
Means: s equals the Goedel number of the sequent with Gamma on the left and Delta on the right
Read as: Subsequence of s and s prime
Means: Subsequence of s and s prime
Read as: the predicate symbol code relation Pred applied to x and n
Means: the predicate symbol code relation Pred applied to x and n
Read as: the formula code relation F r m applied to x
Means: the formula code relation F r m applied to x
Read as: v subscript zero equals the object language constant zero
Means: v subscript zero equals the object language constant zero
Read as: pi sub one
Means: pi sub one
Read as: R sub Gamma of y
Means: R sub Gamma of y
Read as: if capital A then capital B
Means: if capital A then capital B
Read as: the component at index one of the tuple coded by s equals the Goedel number of Delta
Means: the component at index one of the tuple coded by s equals the Goedel number of Delta
Read as: the formula obtained by substituting c for every free occurrence of x in capital A of x
Means: the formula obtained by substituting c for every free occurrence of x in capital A of x
Read as: Term holds of the element at position i in the sequence coded by z
Means: Term holds of the element at position i in the sequence coded by z
Read as: delta sub zero equals delta
Means: delta sub zero equals delta
Read as: the sequence of subtree codes for d
Means: the sequence of subtree codes for d
Read as: the function symbol f with index i and arity n
Means: the function symbol f with index i and arity n
Read as: for every i less than the length of s, there exists a j less than the length of s prime such that component i of s equals component j of s prime
Means: for every i less than the length of s, there exists a j less than the length of s prime such that component i of s equals component j of s prime
Read as: z subscript l
Means: z subscript l
Read as: First product. Two raised to the power the symbol code of equality plus one, times three raised to the power the symbol code of left parenthesis plus one, times five raised to the power the symbol code of v subscript zero plus one, times seven raised to the power the symbol code of comma plus one, times eleven raised to the power the symbol code of c subscript zero plus one, times thirteen raised to the power the symbol code of right parenthesis plus one. This equals the following second product. Two raised to the power the quantity two to the first power times three to the eighth power, plus one; times three raised to the power the quantity two to the first power times three to the ninth power, plus one; times five raised to the power the quantity two squared times three to the first power, plus one; times seven raised to the power the quantity two to the first power times three to the eleventh power, plus one; times eleven raised to the power the quantity two cubed times three to the first power, plus one; times thirteen raised to the power the quantity two to the first power times three to the tenth power, plus one. This equals the following third product. Two raised to the power thirteen thousand one hundred twenty three, times three raised to the power thirty nine thousand three hundred sixty seven, times five to the thirteenth power, times seven raised to the power three hundred fifty four thousand two hundred ninety five, times eleven to the twenty fifth power, times thirteen raised to the power one hundred eighteen thousand ninety nine.
Means: First product. Two raised to the power the symbol code of equality plus one, times three raised to the power the symbol code of left parenthesis plus one, times five raised to the power the symbol code of v subscript zero plus one, times seven raised to the power the symbol code of comma plus one, times eleven raised to the power the symbol code of c subscript zero plus one, times thirteen raised to the power the symbol code of right parenthesis plus one. This equals the following second product. Two raised to the power the quantity two to the first power times three to the eighth power, plus one; times three raised to the power the quantity two to the first power times three to the ninth power, plus one; times five raised to the power the quantity two squared times three to the first power, plus one; times seven raised to the power the quantity two to the first power times three to the eleventh power, plus one; times eleven raised to the power the quantity two cubed times three to the first power, plus one; times thirteen raised to the power the quantity two to the first power times three to the tenth power, plus one. This equals the following third product. Two raised to the power thirteen thousand one hundred twenty three, times three raised to the power thirty nine thousand three hundred sixty seven, times five to the thirteenth power, times seven raised to the power three hundred fifty four thousand two hundred ninety five, times eleven to the twenty fifth power, times thirteen raised to the power one hundred eighteen thousand ninety nine.
Read as: the length of the tuple coded by s is two, and for every i less than the sum of the lengths of the sequences coded by its components at indices zero and one, Sent holds of the entry at index i in the concatenation of those two sequences
Means: the length of the tuple coded by s is two, and for every i less than the sum of the lengths of the sequences coded by its components at indices zero and one, Sent holds of the entry at index i in the concatenation of those two sequences
Read as: x
Means: x
Read as: Follows By existential quantifier introduction of d
Means: Follows By existential quantifier introduction of d
Read as: if the conditional, if capital B then either capital B or capital A, holds, then the following conditional holds: if capital A then, if capital B then either capital B or capital A
Means: if the conditional, if capital B then either capital B or capital A, holds, then the following conditional holds: if capital A then, if capital B then either capital B or capital A
Read as: the code of the sequence one, zero, equals two raised to the power one plus one, times three raised to the power zero plus one
Means: the code of the sequence one, zero, equals two raised to the power one plus one, times three raised to the power zero plus one
Read as: c
Means: c
Read as: the symbol code of s equals the code of the sequence three, n, i
Means: the symbol code of s equals the code of the sequence three, n, i
Read as: y equals the code of the sequence of Goedel numbers of s subscript zero through s subscript k minus one
Means: y equals the code of the sequence of Goedel numbers of s subscript zero through s subscript k minus one
Read as: Proof from Gamma of x and y
Means: Proof from Gamma of x and y
Read as: capital B belongs to Gamma
Means: capital B belongs to Gamma
Read as: End Formula of d is a sentence code, and at least one of the following cases holds. Last Rule of d equals one and Follows By conjunction introduction of d holds; or one of the intervening correctly numbered rule cases; or Last Rule of d equals sixteen and Follows By equality elimination of d holds; or there exist n and x, both less than d, such that d is the tuple containing zero, x, and n
Means: End Formula of d is a sentence code, and at least one of the following cases holds. Last Rule of d equals one and Follows By conjunction introduction of d holds; or one of the intervening correctly numbered rule cases; or Last Rule of d equals sixteen and Follows By equality elimination of d holds; or there exist n and x, both less than d, such that d is the tuple containing zero, x, and n
Read as: capital B sub n belongs to Gamma
Means: capital B sub n belongs to Gamma
Read as: Sequent of s
Means: Sequent of s
Read as: the function symbol f with index i and arity n
Means: the function symbol f with index i and arity n
Read as: an opening parenthesis symbol
Means: an opening parenthesis symbol
Read as: num of n equals the Goedel number of the object language numeral for n
Means: num of n equals the Goedel number of the object language numeral for n
Read as: the sequent with an empty left side and, on the right, the implication whose antecedent is the conjunction of capital A and capital B and whose consequent is capital A
Means: the sequent with an empty left side and, on the right, the implication whose antecedent is the conjunction of capital A and capital B and whose consequent is capital A
Read as: equality
Means: equality
Read as: Open Assumption of z and d
Means: Open Assumption of z and d
Read as: the sequent with Gamma on the left and Delta followed by the conjunction of capital A and capital B on the right
Means: the sequent with Gamma on the left and Delta followed by the conjunction of capital A and capital B on the right
Read as: the element at position i in the sequence coded by y equals the coded concatenation of three strings: the string consisting of the function symbol f with index j and arity n followed by left parenthesis; the comma separated argument string with code flatten of z; and the one symbol string right parenthesis
Means: the element at position i in the sequence coded by y equals the coded concatenation of three strings: the string consisting of the function symbol f with index j and arity n followed by left parenthesis; the comma separated argument string with code flatten of z; and the one symbol string right parenthesis
Read as: Is Axiom for the schema, if capital A of x holds for every x then capital A of t, evaluated at n
Means: Is Axiom for the schema, if capital A of x holds for every x then capital A of t, evaluated at n
Read as: End Formula of d sub two equals the Goedel number of capital B
Means: End Formula of d sub two equals the Goedel number of capital B
Read as: the four entry tuple consisting, in order, of one, p sub one, the Goedel number of the sequent with an empty left side and the implication from the conjunction of capital A and capital B to capital A on the right, and fourteen
Means: the four entry tuple consisting, in order, of one, p sub one, the Goedel number of the sequent with an empty left side and the implication from the conjunction of capital A and capital B to capital A on the right, and fourteen
Read as: End Formula of d sub one equals the Goedel number of capital A
Means: End Formula of d sub one equals the Goedel number of capital A
Read as: the symbol code of s equals the code of the sequence two, i
Means: the symbol code of s equals the code of the sequence two, i
Read as: Discharge Label of d equals the component of d whose index is component zero of d plus two
Means: Discharge Label of d equals the component of d whose index is component zero of d plus two
Read as: lower case b
Means: lower case b
Read as: Const holds of the element at position i in the sequence coded by y
Means: Const holds of the element at position i in the sequence coded by y
Read as: delta sub zero
Means: delta sub zero
Read as: Follows By cut of p
Means: Follows By cut of p
Read as: there exist g, d, lower case a, x, and t, each less than p, such that all the following hold. End Sequent of p equals the ordered pair of g and d concatenated with the singleton tuple containing the concatenation of the Goedel code of the existential quantifier, x, and lower case a. End Sequent of the component at index one of p equals the ordered pair of g and d concatenated with the singleton tuple containing Subst of lower case a, t, and x. The component at index zero of p is one, and Last Rule of p is eighteen. Here lower case a, x, and t are numerical codes, and Subst operates on those codes
Means: there exist g, d, lower case a, x, and t, each less than p, such that all the following hold. End Sequent of p equals the ordered pair of g and d concatenated with the singleton tuple containing the concatenation of the Goedel code of the existential quantifier, x, and lower case a. End Sequent of the component at index one of p equals the ordered pair of g and d concatenated with the singleton tuple containing Subst of lower case a, t, and x. The component at index zero of p is one, and Last Rule of p is eighteen. Here lower case a, x, and t are numerical codes, and Subst operates on those codes
Read as: the code of the singleton sequence whose only element is the code of the sequence one, i
Means: the code of the singleton sequence whose only element is the code of the sequence one, i
Read as: Follows By conditional introduction of d
Means: Follows By conditional introduction of d
Read as: Quantifier Rule one of d and i holds by definition if and only if there exists a j less than i, and there exist b, x, and a less than component i of d, and c less than component j of d, such that all of the following hold. x is a variable code and c is a constant code. Component i of d is the concatenation, in order, of the code of an opening parenthesis, b, the code of the conditional symbol, the code of the universal quantifier symbol, x, a, and the code of a closing parenthesis. Component j of d is the concatenation, in order, of the code of an opening parenthesis, b, the code of the conditional symbol, the substitution function at a, c, and x, and the code of a closing parenthesis. b and the result of that substitution are sentence codes. Every symbol entry in b differs from component zero of c. Source anomaly note: this displayed test omits freshness of c in the quantified matrix
Means: Quantifier Rule one of d and i holds by definition if and only if there exists a j less than i, and there exist b, x, and a less than component i of d, and c less than component j of d, such that all of the following hold. x is a variable code and c is a constant code. Component i of d is the concatenation, in order, of the code of an opening parenthesis, b, the code of the conditional symbol, the code of the universal quantifier symbol, x, a, and the code of a closing parenthesis. Component j of d is the concatenation, in order, of the code of an opening parenthesis, b, the code of the conditional symbol, the substitution function at a, c, and x, and the code of a closing parenthesis. b and the result of that substitution are sentence codes. Every symbol entry in b differs from component zero of c. Source anomaly note: this displayed test omits freshness of c in the quantified matrix
Read as: the Goedel number of the one symbol constant term c subscript i
Means: the Goedel number of the one symbol constant term c subscript i
Read as: the code of the sequence zero, seven, equals two raised to the power zero plus one, times three raised to the power seven plus one
Means: the code of the sequence zero, seven, equals two raised to the power zero plus one, times three raised to the power seven plus one
Read as: j is less than x
Means: j is less than x
Read as: the Goedel number of the sequent with Gamma on the left and Delta on the right equals the ordered pair whose first entry is the Goedel number of Gamma and whose second entry is the Goedel number of Delta
Means: the Goedel number of the sequent with Gamma on the left and Delta on the right equals the ordered pair whose first entry is the Goedel number of Gamma and whose second entry is the Goedel number of Delta
Read as: if capital B then capital A of c
Means: if capital B then capital A of c
Read as: the Goedel number of the prefix equality formula with arguments v subscript zero and c subscript zero
Means: the Goedel number of the prefix equality formula with arguments v subscript zero and c subscript zero
Read as: the free occurrence relation Free Occ applied to x, z, and i
Means: the free occurrence relation Free Occ applied to x, z, and i
Read as: i is less than k
Means: i is less than k
Read as: ten
Means: ten
Read as: the predicate symbol P with index i and arity n
Means: the predicate symbol P with index i and arity n
Read as: Follows By rule R of p
Means: Follows By rule R of p
Read as: the sequent with Gamma on the left and Delta followed by capital B on the right
Means: the sequent with Gamma on the left and Delta followed by capital B on the right
Read as: the sequent with Gamma on the left and Delta followed by capital B on the right
Means: the sequent with Gamma on the left and Delta followed by capital B on the right
Read as: the component at index zero of End Sequent of x
Means: the component at index zero of End Sequent of x
Read as: right universal quantifier
Means: right universal quantifier
Read as: Follows By conditional elimination of d
Means: Follows By conditional elimination of d
Read as: for every y less than d, if Assum of y, d, and n holds, then y equals x
Means: for every y less than d, if Assum of y, d, and n holds, then y equals x
Read as: the variable v subscript two
Means: the variable v subscript two
Read as: the variable v subscript five
Means: the variable v subscript five
Read as: if capital B then the conditional, if capital C then capital B
Means: if capital B then the conditional, if capital C then capital B
Read as: left conjunction
Means: left conjunction
Read as: As printed, there exists an s less than the code of the sequence of subtree codes for d such that Subsequence of s and that sequence holds, component zero of s equals d, and there exists an n less than d with the following properties. The component of s at its length truncated minus one equals the tuple containing zero, z, and n. For every i less than the length of s truncated minus one, component i plus one of s is an immediate subderivation of component i of s, and Discharge Label of component i of s differs from n. The correction ledger records defects in the strict path bound and the treatment of label zero
Means: As printed, there exists an s less than the code of the sequence of subtree codes for d such that Subsequence of s and that sequence holds, component zero of s equals d, and there exists an n less than d with the following properties. The component of s at its length truncated minus one equals the tuple containing zero, z, and n. For every i less than the length of s truncated minus one, component i plus one of s is an immediate subderivation of component i of s, and Discharge Label of component i of s differs from n. The correction ledger records defects in the strict path bound and the treatment of label zero
Read as: s subscript k minus one equals s
Means: s subscript k minus one equals s
Read as: the predicate symbol P with index i and arity n
Means: the predicate symbol P with index i and arity n
Read as: y is a member of Gamma
Means: y is a member of Gamma
Read as: Gamma
Means: Gamma
Read as: s subscript zero through s subscript n minus one
Means: s subscript zero through s subscript n minus one
Read as: Last Rule of p equals the component of the tuple coded by p at index two plus the component at index zero of that tuple
Means: Last Rule of p equals the component of the tuple coded by p at index two plus the component at index zero of that tuple
Read as: z
Means: z
Read as: the sequent with Gamma on the left and Delta followed by the conjunction of capital A and capital B on the right
Means: the sequent with Gamma on the left and Delta followed by the conjunction of capital A and capital B on the right
Read as: Assum of x, d, and n holds by definition if and only if there exists an i less than d such that entry i of the sequence of subtree codes for d equals the tuple containing zero, x, and n
Means: Assum of x, d, and n holds by definition if and only if there exists an i less than d such that entry i of the sequence of subtree codes for d equals the tuple containing zero, x, and n
Read as: the constant symbol c subscript i
Means: the constant symbol c subscript i
Read as: the final component of the sequence coded by x, at index the length of x minus one
Means: the final component of the sequence coded by x, at index the length of x minus one
Read as: zero
Means: zero
Read as: Is Axiom for the schema, if capital A then, if capital B then both capital A and capital B, evaluated at n
Means: Is Axiom for the schema, if capital A then, if capital B then both capital A and capital B, evaluated at n
Read as: p subscript i
Means: p subscript i
Read as: the right side of the end sequent coded by x has length one, and its entry at index zero equals y
Means: the right side of the end sequent coded by x has length one, and its entry at index zero equals y
Read as: Var holds of the element at position i in the sequence coded by y
Means: Var holds of the element at position i in the sequence coded by y
Read as: h Conditional of s, y, and zero equals y. h Conditional of s, y, and n plus one equals the concatenation, in order, of the code of an opening parenthesis, component n of s, the code of the conditional symbol, h Conditional of s, y, and n, and the code of a closing parenthesis. Conditional of s and y equals h Conditional of s, y, and the length of s. Thus the antecedents are prepended in reverse sequence order. So we can define Proof relative to Gamma of x and y by requiring an s less than Sequence Bound of x and x such that the last component of x equals Conditional of s and y, every component of s belongs to the code set for Gamma, and Deriv of x holds. Here x codes a proof without assumptions of that nested conditional, not a proof ending directly with the formula coded by y
Means: h Conditional of s, y, and zero equals y. h Conditional of s, y, and n plus one equals the concatenation, in order, of the code of an opening parenthesis, component n of s, the code of the conditional symbol, h Conditional of s, y, and n, and the code of a closing parenthesis. Conditional of s and y equals h Conditional of s, y, and the length of s. Thus the antecedents are prepended in reverse sequence order. So we can define Proof relative to Gamma of x and y by requiring an s less than Sequence Bound of x and x such that the last component of x equals Conditional of s and y, every component of s belongs to the code set for Gamma, and Deriv of x holds. Here x codes a proof without assumptions of that nested conditional, not a proof ending directly with the formula coded by y
Read as: m
Means: m
Read as: L K
Means: L K
Read as: either the four entry tuple consisting, in order, of one, the Goedel number of pi sub one, the Goedel number of the conclusion sequent with Gamma on the left and Delta on the right, and k; or the five entry tuple consisting, in order, of two, the Goedel number of pi sub one, the Goedel number of pi sub two, the Goedel number of that conclusion sequent, and k
Means: either the four entry tuple consisting, in order, of one, the Goedel number of pi sub one, the Goedel number of the conclusion sequent with Gamma on the left and Delta on the right, and k; or the five entry tuple consisting, in order, of two, the Goedel number of pi sub one, the Goedel number of pi sub two, the Goedel number of that conclusion sequent, and k
Read as: the variable v subscript i
Means: the variable v subscript i
Read as: the element at position zero in the sequence coded by x
Means: the element at position zero in the sequence coded by x
Read as: one
Means: one
Read as: t equals t
Means: t equals t
Read as: Follows By conjunction introduction of d
Means: Follows By conjunction introduction of d
Read as: there exist g, d, lower case a, and lower case b, each less than p, such that all the following hold. End Sequent of p equals the ordered pair of g and the concatenation of d with the singleton tuple containing the concatenation of the Goedel code of an opening parenthesis, lower case a, the Goedel code of conjunction, lower case b, and the Goedel code of a closing parenthesis. End Sequent of the component at index one of p equals the ordered pair of g and d concatenated with the singleton tuple containing lower case a. End Sequent of the component at index two of p equals the ordered pair of g and d concatenated with the singleton tuple containing lower case b. The component at index zero of p is two, and Last Rule of p is ten
Means: there exist g, d, lower case a, and lower case b, each less than p, such that all the following hold. End Sequent of p equals the ordered pair of g and the concatenation of d with the singleton tuple containing the concatenation of the Goedel code of an opening parenthesis, lower case a, the Goedel code of conjunction, lower case b, and the Goedel code of a closing parenthesis. End Sequent of the component at index one of p equals the ordered pair of g and d concatenated with the singleton tuple containing lower case a. End Sequent of the component at index two of p equals the ordered pair of g and d concatenated with the singleton tuple containing lower case b. The component at index zero of p is two, and Last Rule of p is ten
Read as: Follows By equality elimination of d
Means: Follows By equality elimination of d
Read as: the tuple containing, in order, the Goedel numbers of capital A sub one through capital A sub n
Means: the tuple containing, in order, the Goedel numbers of capital A sub one through capital A sub n
Read as: Deriv of p
Means: Deriv of p
Read as: the tuple with entries zero, x, and n
Means: the tuple with entries zero, x, and n
Read as: if capital B then the formula obtained by substituting c for every free occurrence of x in capital A
Means: if capital B then the formula obtained by substituting c for every free occurrence of x in capital A
Read as: the helper substitution function h Subst
Means: the helper substitution function h Subst
Read as: right existential quantifier
Means: right existential quantifier
Read as: the code of the sequence z subscript one through z subscript n
Means: the code of the sequence z subscript one through z subscript n
Read as: Symbol code table. Each code is the code of a two element sequence. Falsity has code zero, zero. Not has code zero, one. Or has code zero, two. And has code zero, three. If then has code zero, four. For all has code zero, five. There exists has code zero, six. Equality has code zero, seven. Left parenthesis has code zero, eight. Right parenthesis has code zero, nine. Comma has code zero, ten. End of symbol code table.
Means: Symbol code table. Each code is the code of a two element sequence. Falsity has code zero, zero. Not has code zero, one. Or has code zero, two. And has code zero, three. If then has code zero, four. For all has code zero, five. There exists has code zero, six. Equality has code zero, seven. Left parenthesis has code zero, eight. Right parenthesis has code zero, nine. Comma has code zero, ten. End of symbol code table.
Read as: the ordered pair whose first entry is zero and whose second entry is the Goedel number of the sequent with Gamma on the left and Delta on the right
Means: the ordered pair whose first entry is zero and whose second entry is the Goedel number of the sequent with Gamma on the left and Delta on the right
Read as: the equality symbol
Means: the equality symbol
Read as: the symbol code of s equals the code of the sequence one, i
Means: the symbol code of s equals the code of the sequence one, i
Read as: Modus Ponens of d and i holds by definition if and only if there exist j and k, both less than i, such that component k of d equals the concatenation, in order, of the code of an opening parenthesis, component j of d, the code of the conditional symbol, component i of d, and the code of a closing parenthesis
Means: Modus Ponens of d and i holds by definition if and only if there exist j and k, both less than i, such that component k of d equals the concatenation, in order, of the code of an opening parenthesis, component j of d, the code of the conditional symbol, component i of d, and the code of a closing parenthesis
Read as: component i of the sequence coded by s
Means: component i of the sequence coded by s
Read as: the symbol code of s
Means: the symbol code of s
Read as: delta sub i plus one
Means: delta sub i plus one
Read as: Discharge of x, d, and n
Means: Discharge of x, d, and n
Read as: Last Rule of d equals the component of d whose index is component zero of d plus three
Means: Last Rule of d equals the component of d whose index is component zero of d plus three
Read as: the code of the sequence n subscript zero through n subscript k
Means: the code of the sequence n subscript zero through n subscript k
Read as: Initial Sequent of s
Means: Initial Sequent of s
Read as: Correct of p
Means: Correct of p
Read as: capital A of x
Means: capital A of x
Read as: A
Means: A
Read as: k
Means: k
Read as: the assumption capital A, marked with discharge label n
Means: the assumption capital A, marked with discharge label n
Read as: the sequent with the conjunction of capital A and capital B on the left and capital A on the right
Means: the sequent with the conjunction of capital A and capital B on the left and capital A on the right
Read as: Proof from Gamma of x and y holds, by definition, if and only if all the following hold. Deriv of x holds. For every i less than the length of the left side of the end sequent coded by x, R sub Gamma holds of the entry at index i on that left side. The right side of the end sequent coded by x has length one, and its entry at index zero equals y
Means: Proof from Gamma of x and y holds, by definition, if and only if all the following hold. Deriv of x holds. For every i less than the length of the left side of the end sequent coded by x, R sub Gamma holds of the entry at index i on that left side. The right side of the end sequent coded by x has length one, and its entry at index zero equals y
Read as: For zero premises, the tuple contains zero, the Goedel number of capital A, n, and k. For one premise, it contains one, the Goedel number of delta sub one, the Goedel number of capital A, n, and k. For two premises, it contains two, the Goedel numbers of delta sub one and delta sub two, the Goedel number of capital A, n, and k. For three premises, it contains three, the Goedel numbers of delta sub one, delta sub two, and delta sub three, the Goedel number of capital A, n, and k. The entry order is the order just stated in each case.
Means: For zero premises, the tuple contains zero, the Goedel number of capital A, n, and k. For one premise, it contains one, the Goedel number of delta sub one, the Goedel number of capital A, n, and k. For two premises, it contains two, the Goedel numbers of delta sub one and delta sub two, the Goedel number of capital A, n, and k. For three premises, it contains three, the Goedel numbers of delta sub one, delta sub two, and delta sub three, the Goedel number of capital A, n, and k. The entry order is the order just stated in each case.
Read as: the Goedel number of delta
Means: the Goedel number of delta
Read as: right conjunction
Means: right conjunction
Read as: the closed term code relation C l Term
Means: the closed term code relation C l Term
Read as: the following nested four entry tuple. Its first entry is one. Its second entry is a four entry tuple whose entries, in order, are one; the ordered pair of zero and the Goedel number of the sequent with capital A on both sides; the Goedel number of the sequent with the conjunction of capital A and capital B on the left and capital A on the right; and nine. Its third entry is the Goedel number of the sequent with an empty left side and the implication from the conjunction of capital A and capital B to capital A on the right. Its fourth entry is fourteen
Means: the following nested four entry tuple. Its first entry is one. Its second entry is a four entry tuple whose entries, in order, are one; the ordered pair of zero and the Goedel number of the sequent with capital A on both sides; the Goedel number of the sequent with the conjunction of capital A and capital B on the left and capital A on the right; and nine. Its third entry is the Goedel number of the sequent with an empty left side and the implication from the conjunction of capital A and capital B to capital A on the right. Its fourth entry is fourteen
Read as: the length of the sequence coded by x
Means: the length of the sequence coded by x
Read as: x equals the Goedel number of the one symbol formula falsity
Means: x equals the Goedel number of the one symbol formula falsity
Read as: R
Means: R
Read as: the empty set
Means: the empty set
Read as: less than or equal to p subscript k minus one raised to the power k times the quantity x plus one
Means: less than or equal to p subscript k minus one raised to the power k times the quantity x plus one
Read as: the final component of the sequence coded by d, at index the length of d minus one
Means: the final component of the sequence coded by d, at index the length of d minus one
Read as: the code of the sequence of symbol codes of s subscript zero through s subscript n minus one
Means: the code of the sequence of symbol codes of s subscript zero through s subscript n minus one
Read as: the symbol code of the variable v subscript zero
Means: the symbol code of the variable v subscript zero
Read as: z equals the code of the sequence z subscript one through z subscript n
Means: z equals the code of the sequence z subscript one through z subscript n
Read as: equality introduction
Means: equality introduction
Read as: the sequent with Gamma on the left and Delta followed by the result of substituting the term t for the free occurrences of x in capital A on the right
Means: the sequent with Gamma on the left and Delta followed by the result of substituting the term t for the free occurrences of x in capital A on the right
Read as: Deriv of p
Means: Deriv of p
Read as: delta sub k
Means: delta sub k
Read as: z subscript one and z subscript two, both less than x
Means: z subscript one and z subscript two, both less than x
Read as: the variable v subscript j
Means: the variable v subscript j
Read as: Component zero of d equals two, and Discharge Label of d equals zero, and Last Rule of d equals one, and End Formula of d equals the code obtained by concatenating, in order, the code of an opening parenthesis, End Formula of component one of d, the code of the conjunction symbol, End Formula of component two of d, and the code of a closing parenthesis
Means: Component zero of d equals two, and Discharge Label of d equals zero, and Last Rule of d equals one, and End Formula of d equals the code obtained by concatenating, in order, the code of an opening parenthesis, End Formula of component one of d, the code of the conjunction symbol, End Formula of component two of d, and the code of a closing parenthesis
Read as: p subscript zero equals two
Means: p subscript zero equals two
Read as: the component at index zero of the tuple coded by s equals the Goedel number of Gamma
Means: the component at index zero of the tuple coded by s equals the Goedel number of Gamma
Read as: k subscript zero
Means: k subscript zero
Read as: capital C
Means: capital C
Read as: Term holds of z subscript two
Means: Term holds of z subscript two
Read as: delta sub one
Means: delta sub one
Read as: k equals one
Means: k equals one
Read as: the sequent with Gamma on the left and Delta followed by capital A on the right
Means: the sequent with Gamma on the left and Delta followed by capital A on the right
Read as: the function symbol f with index j and arity n
Means: the function symbol f with index j and arity n
Read as: delta sub i
Means: delta sub i
Read as: y
Means: y
Read as: Gamma sub zero is a subset of Gamma
Means: Gamma sub zero is a subset of Gamma
Read as: the formula there exists an x such that capital A
Means: the formula there exists an x such that capital A
Read as: pi sub two
Means: pi sub two
Read as: F r m holds of x, and for every i less than the length of the sequence coded by x and every z less than x: if there exists j less than z such that z equals the Goedel number of the variable term v subscript j, then Free Occ does not hold of x, z, and i
Means: F r m holds of x, and for every i less than the length of the sequence coded by x and every z less than x: if there exists j less than z such that z equals the Goedel number of the variable term v subscript j, then Free Occ does not hold of x, z, and i
Read as: the code of the six element sequence consisting, in order, of the symbol codes of equality, left parenthesis, v subscript zero, comma, c subscript zero, and right parenthesis
Means: the code of the six element sequence consisting, in order, of the symbol codes of equality, left parenthesis, v subscript zero, comma, c subscript zero, and right parenthesis
Read as: the equality symbol applied to the variable v subscript zero and the constant c subscript zero
Means: the equality symbol applied to the variable v subscript zero and the constant c subscript zero
Read as: component zero of d equals zero
Means: component zero of d equals zero
Read as: i is less than n
Means: i is less than n
Read as: Subst applied to the Goedel numbers of A, t, and u equals the Goedel number of A with t substituted for every free occurrence of u
Means: Subst applied to the Goedel numbers of A, t, and u equals the Goedel number of A with t substituted for every free occurrence of u
Read as: the atomic formula code relation Atom applied to x
Means: the atomic formula code relation Atom applied to x
Read as: the Goedel number of the single string consisting of t subscript one through t subscript n separated by commas
Means: the Goedel number of the single string consisting of t subscript one through t subscript n separated by commas
Read as: h Subst applied to x, y, z, and the length of the sequence coded by x
Means: h Subst applied to x, y, z, and the length of the sequence coded by x
Read as: End Formula of d equals the component of d whose index is component zero of d plus one
Means: End Formula of d equals the component of d whose index is component zero of d plus one
Read as: Follows By rule R of d
Means: Follows By rule R of d
Read as: capital A is derivable from the set containing capital B sub one through capital B sub n
Means: capital A is derivable from the set containing capital B sub one through capital B sub n
Read as: p sub zero equals the ordered pair whose first entry is zero and whose second entry is the Goedel number of the sequent with capital A on both sides
Means: p sub zero equals the ordered pair whose first entry is zero and whose second entry is the Goedel number of the sequent with capital A on both sides
Read as: l
Means: l
Read as: the sequent with Gamma on the left and Delta followed by the formula there exists x such that capital A on the right
Means: the sequent with Gamma on the left and Delta followed by the formula there exists x such that capital A on the right
Read as: right conjunction
Means: right conjunction
Read as: z is less than x
Means: z is less than x
Read as: the Deriv predicate
Means: the Deriv predicate
Read as: A with t substituted for every free occurrence of u
Means: A with t substituted for every free occurrence of u
Read as: the assumption capital A and capital B, marked with discharge label one
Means: the assumption capital A and capital B, marked with discharge label one
Read as: the element at position i prime in the sequence coded by y
Means: the element at position i prime in the sequence coded by y
Read as: the code of the sequence of Goedel numbers of t subscript one through t subscript n
Means: the code of the sequence of Goedel numbers of t subscript one through t subscript n
Read as: n subscript zero
Means: n subscript zero
Read as: s subscript k minus one
Means: s subscript k minus one
Read as: the function symbol code relation F n applied to x and n
Means: the function symbol code relation F n applied to x and n
Read as: the Goedel number of Gamma equals the tuple of the Goedel numbers of capital A sub one through capital A sub n
Means: the Goedel number of Gamma equals the tuple of the Goedel numbers of capital A sub one through capital A sub n
Read as: the tuple containing one, d sub one, the Goedel number of the formula if both capital A and capital B then capital A, one, and five
Means: the tuple containing one, d sub one, the Goedel number of the formula if both capital A and capital B then capital A, one, and five
Read as: for every i less than the length of Subtree Sequence of p, Correct holds of the entry at index i in Subtree Sequence of p
Means: for every i less than the length of Subtree Sequence of p, Correct holds of the entry at index i in Subtree Sequence of p
Read as: Correct of d
Means: Correct of d
Read as: s subscript zero
Means: s subscript zero
Read as: the sequent with an empty left side and the equation t equals t on the right
Means: the sequent with an empty left side and the equation t equals t on the right
Read as: if both capital A and capital B hold, then capital A
Means: if both capital A and capital B hold, then capital A
Read as: Follows By right conjunction of p
Means: Follows By right conjunction of p
Read as: the sequent with capital A on the left and capital A on the right
Means: the sequent with capital A on the left and capital A on the right
Read as: the closed term code relation C l Term applied to x
Means: the closed term code relation C l Term applied to x
Read as: if capital B then either capital B or capital A
Means: if capital B then either capital B or capital A
Read as: the code of the sequence k subscript zero through k subscript n minus one
Means: the code of the sequence k subscript zero through k subscript n minus one
Read as: t subscript l
Means: t subscript l
Read as: t subscript one
Means: t subscript one
Read as: if capital B then, for every x, capital A of x
Means: if capital B then, for every x, capital A of x
Read as: num of n
Means: num of n
Read as: capital A and capital B
Means: capital A and capital B
Read as: Num of zero equals the Goedel number of the one symbol term zero. Num of n plus one equals the coded concatenation of the string consisting of the successor symbol followed by left parenthesis, the numeral string with Goedel number num of n, and the one symbol string right parenthesis.
Means: Num of zero equals the Goedel number of the one symbol term zero. Num of n plus one equals the coded concatenation of the string consisting of the successor symbol followed by left parenthesis, the numeral string with Goedel number num of n, and the one symbol string right parenthesis.
Read as: if capital A then the following conditional holds: if capital B then either capital B or capital A
Means: if capital A then the following conditional holds: if capital B then either capital B or capital A
Read as: the Goedel number of pi
Means: the Goedel number of pi
Read as: the code of the singleton sequence containing the symbol code of v subscript five equals two raised to the power the symbol code of v subscript five plus one. This equals two raised to the power the quantity two squared times three to the sixth power, plus one
Means: the code of the singleton sequence containing the symbol code of v subscript five equals two raised to the power the symbol code of v subscript five plus one. This equals two raised to the power the quantity two squared times three to the sixth power, plus one
Read as: t subscript n
Means: t subscript n
Read as: conjunction introduction
Means: conjunction introduction
Read as: the length of the sequence coded by y
Means: the length of the sequence coded by y
Read as: less than x
Means: less than x
Read as: the sequent with Gamma on the left and Delta followed by capital A on the right
Means: the sequent with Gamma on the left and Delta followed by capital A on the right
Read as: Gamma equals the finite sequence capital A sub one through capital A sub n
Means: Gamma equals the finite sequence capital A sub one through capital A sub n
Read as: d sub zero equals the tuple containing zero, the Goedel number of the formula capital A and capital B, and one
Means: d sub zero equals the tuple containing zero, the Goedel number of the formula capital A and capital B, and one
Read as: s subscript i
Means: s subscript i
Read as: lower case a
Means: lower case a
Read as: the tuple with entries zero, the Goedel number of capital A, and n
Means: the tuple with entries zero, the Goedel number of capital A, and n
Read as: k subscript n minus one
Means: k subscript n minus one
Read as: capital A is derivable from Gamma
Means: capital A is derivable from Gamma
Read as: g
Means: g
Read as: the variable term code relation Var applied to x
Means: the variable term code relation Var applied to x
Read as: flatten of z
Means: flatten of z
Read as: if capital A then capital B
Means: if capital A then capital B
Read as: the sequence s subscript zero through s subscript k minus one
Means: the sequence s subscript zero through s subscript k minus one
Read as: n subscript k
Means: n subscript k
Read as: the conditional symbol
Means: the conditional symbol
Read as: capital B
Means: capital B
Read as: conjunction elimination
Means: conjunction elimination
Read as: Term holds of z subscript one
Means: Term holds of z subscript one
Read as: i prime is less than i
Means: i prime is less than i
Read as: delta
Means: delta
Read as: Base case: h Subst of x, y, z, and zero equals the code of the empty sequence. Recursion step: h Subst of x, y, z, and i plus one has two cases. If Free Occ holds of x, z, and i, concatenate the string coded by h Subst of x, y, z, and i with the replacement term string coded by y. Otherwise append the single symbol code at position i in the sequence coded by x to the sequence coded by h Subst of x, y, z, and i. Each case returns the code of the resulting sequence.
Means: Base case: h Subst of x, y, z, and zero equals the code of the empty sequence. Recursion step: h Subst of x, y, z, and i plus one has two cases. If Free Occ holds of x, z, and i, concatenate the string coded by h Subst of x, y, z, and i with the replacement term string coded by y. Otherwise append the single symbol code at position i in the sequence coded by x to the sequence coded by h Subst of x, y, z, and i. Each case returns the code of the resulting sequence.
Read as: Follows By equality of p
Means: Follows By equality of p
Read as: two
Means: two
Read as: Deriv of d holds by definition if and only if, for every i less than the length of d, either component i of d is an axiom code, or Modus Ponens of d and i holds, or Quantifier Rule of d and i holds
Means: Deriv of d holds by definition if and only if, for every i less than the length of d, either component i of d is an axiom code, or Modus Ponens of d and i holds, or Quantifier Rule of d and i holds
Read as: delta sub two
Means: delta sub two
Read as: Follows By left conditional of p
Means: Follows By left conditional of p
Read as: Follows By right existential quantifier of p
Means: Follows By right existential quantifier of p
Read as: k is less than i
Means: k is less than i
Read as: Follows By universal quantifier introduction of d
Means: Follows By universal quantifier introduction of d
Read as: the component at index one of End Sequent of x
Means: the component at index one of End Sequent of x
Read as: capital A sub n
Means: capital A sub n
Read as: i
Means: i
Read as: the sequent with Gamma on the left and Delta on the right
Means: the sequent with Gamma on the left and Delta on the right
Read as: Var of x holds by definition if and only if there exists i less than x such that x equals the code of the singleton sequence whose only element is the code of the sequence one, i. Const of x holds by definition if and only if there exists i less than x such that x equals the code of the singleton sequence whose only element is the code of the sequence two, i.
Means: Var of x holds by definition if and only if there exists i less than x such that x equals the code of the singleton sequence whose only element is the code of the sequence one, i. Const of x holds by definition if and only if there exists i less than x such that x equals the code of the singleton sequence whose only element is the code of the sequence two, i.
Read as: the constant term code relation Const applied to x
Means: the constant term code relation Const applied to x
Read as: Quantifier Rule two of d and i
Means: Quantifier Rule two of d and i
Read as: capital A sub one
Means: capital A sub one
Read as: the coded concatenation, in order, of the string consisting of equality followed by left parenthesis, the term string coded by z subscript one, the one symbol string comma, the term string coded by z subscript two, and the one symbol string right parenthesis
Means: the coded concatenation, in order, of the string consisting of equality followed by left parenthesis, the term string coded by z subscript one, the one symbol string comma, the term string coded by z subscript two, and the one symbol string right parenthesis
Read as: Deriv of x
Means: Deriv of x
Read as: the sequent with the conjunction of capital A and capital B on the left and capital A on the right
Means: the sequent with the conjunction of capital A and capital B on the left and capital A on the right
Read as: t
Means: t
Read as: Sequent holds of End Sequent of p, and at least one of the following alternatives holds. Last Rule of p is one and Follows By left weakening of p holds; or one of the intervening alternatives indexed by the rule code table holds; or Last Rule of p is twenty and Follows By equality of p holds; or the component at index zero of p is zero and Initial Sequent holds of End Sequent of p
Means: Sequent holds of End Sequent of p, and at least one of the following alternatives holds. Last Rule of p is one and Follows By left weakening of p holds; or one of the intervening alternatives indexed by the rule code table holds; or Last Rule of p is twenty and Follows By equality of p holds; or the component at index zero of p is zero and Initial Sequent holds of End Sequent of p
Read as: the sequent with capital A on the left and capital A on the right
Means: the sequent with capital A on the left and capital A on the right
Read as: the free for relation Free For applied to x, y, and z
Means: the free for relation Free For applied to x, y, and z
Read as: Proof relative to Gamma of x and y holds by definition if and only if Deriv of x holds, End Formula of x equals y, and, for every z less than x, if Open Assumption of z and x holds then R sub Gamma of z holds
Means: Proof relative to Gamma of x and y holds by definition if and only if Deriv of x holds, End Formula of x equals y, and, for every z less than x, if Open Assumption of z and x holds then R sub Gamma of z holds
Read as: the constant symbol c subscript j
Means: the constant symbol c subscript j
Read as: the substitution coding function Subst applied to x, y, and z
Means: the substitution coding function Subst applied to x, y, and z
Read as: j is less than i
Means: j is less than i
Read as: there exists a j less than component zero of d prime such that d equals component j plus one of d prime
Means: there exists a j less than component zero of d prime such that d equals component j plus one of d prime
Read as: Is Axiom for the schema if capital B then, if capital C then capital B, evaluated at n, holds by definition if and only if there exist b and c, both less than n, such that b and c are sentence codes and n equals the concatenation, in order, of the code of an opening parenthesis, b, the code of the conditional symbol, the code of an opening parenthesis, c, the code of the conditional symbol, b, and the code of two closing parentheses
Means: Is Axiom for the schema if capital B then, if capital C then capital B, evaluated at n, holds by definition if and only if there exist b and c, both less than n, such that b and c are sentence codes and n equals the concatenation, in order, of the code of an opening parenthesis, b, the code of the conditional symbol, the code of an opening parenthesis, c, the code of the conditional symbol, b, and the code of two closing parentheses
Read as: the sentence code relation Sent applied to x
Means: the sentence code relation Sent applied to x
Read as: the language L
Means: the language L
Read as: p sub one equals the four entry tuple consisting, in order, of one, p sub zero, the Goedel number of the sequent with the conjunction of capital A and capital B on the left and capital A on the right, and nine
Means: p sub one equals the four entry tuple consisting, in order, of one, p sub zero, the Goedel number of the sequent with the conjunction of capital A and capital B on the left and capital A on the right, and nine
Read as: Component zero of d equals zero, and Discharge Label of d equals zero, and there exists a t less than d such that t is a closed term code and End Formula of d equals the concatenation, in order, of the code of the equality symbol followed by an opening parenthesis, t, the code of a comma, t, and the code of a closing parenthesis
Means: Component zero of d equals zero, and Discharge Label of d equals zero, and there exists a t less than d such that t is a closed term code and End Formula of d equals the concatenation, in order, of the code of the equality symbol followed by an opening parenthesis, t, the code of a comma, t, and the code of a closing parenthesis
Read as: less than or equal to x
Means: less than or equal to x
Read as: Delta
Means: Delta
Read as: pi
Means: pi
Read as: Subderivation of d and d prime
Means: Subderivation of d and d prime
Read as: the symbol code of the equality symbol
Means: the symbol code of the equality symbol
Read as: End Sequent of p equals the component of the tuple coded by p at index one plus the component at index zero of that tuple
Means: End Sequent of p equals the component of the tuple coded by p at index one plus the component at index zero of that tuple
Read as: with no assumptions, the nested conditional is derivable: if capital B sub one, then if capital B sub two, and so on through if capital B sub n, then capital A
Means: with no assumptions, the nested conditional is derivable: if capital B sub one, then if capital B sub two, and so on through if capital B sub n, then capital A
Read as: either there is an x less than s such that Sent of x holds and s equals the ordered pair of the singleton tuple containing x and that same singleton tuple; or there is a t less than s such that Term of t holds and s equals the ordered pair whose first entry is zero and whose second entry is the singleton tuple containing the concatenation, in this order, of the Goedel code of the equality symbol followed by an opening parenthesis, t, the Goedel code of a comma, t again, and the Goedel code of a closing parenthesis
Means: either there is an x less than s such that Sent of x holds and s equals the ordered pair of the singleton tuple containing x and that same singleton tuple; or there is a t less than s such that Term of t holds and s equals the ordered pair whose first entry is zero and whose second entry is the singleton tuple containing the concatenation, in this order, of the Goedel code of the equality symbol followed by an opening parenthesis, t, the Goedel code of a comma, t again, and the Goedel code of a closing parenthesis
Read as: the sequent with Gamma sub zero on the left and capital A on the right
Means: the sequent with Gamma sub zero on the left and capital A on the right
Read as: d sub one equals the tuple containing one, d sub zero, the Goedel number of capital A, zero, and two
Means: d sub one equals the tuple containing one, d sub zero, the Goedel number of capital A, zero, and two
Read as: the Goedel number of the one symbol term v subscript five
Means: the Goedel number of the one symbol term v subscript five
Read as: Follows By disjunction elimination of d
Means: Follows By disjunction elimination of d
Read as: The outer tuple has five entries. First, one. Second, the following inner tuple: one; the assumption tuple containing zero, the Goedel number of capital A and capital B, and one; the Goedel number of capital A; zero; two. Third, the Goedel number of the formula if both capital A and capital B then capital A. Fourth, one. Fifth, five.
Means: The outer tuple has five entries. First, one. Second, the following inner tuple: one; the assumption tuple containing zero, the Goedel number of capital A and capital B, and one; the Goedel number of capital A; zero; two. Third, the Goedel number of the formula if both capital A and capital B then capital A. Fourth, one. Fifth, five.
Read as: capital B sub one
Means: capital B sub one
Every logical symbol receives the code of a pair beginning with zero. Variables receive codes beginning with one, constants codes beginning with two, function symbols codes beginning with three, and predicate symbols codes beginning with four. The function and predicate codes also record arity and index. The complete logical symbol table is read entry by entry in the associated formula.
The first relation recognizes the code of a function symbol with specified arity. The second recognizes the code of a predicate symbol with specified arity, including the equality symbol in arity two. These are symbol codes, not Goedel numbers of whole terms or formulas.
For a finite sequence of symbols, form the finite sequence of their individual symbol codes in the same order, then take the number coding that sequence. The result is the Goedel number of the string.
The example codes equality, left parenthesis, variable v subscript zero, comma, constant c subscript zero, and right parenthesis, in that order. It then uses the first six primes with exponents one greater than those six symbol codes. The final display presents the symbolic product, the substituted exponents, and the evaluated exponents as equal numbers. This is a source worked example, not a solution added by the edition.
The first row uses symbol codes as exponents plus one. The second row substitutes the powers of primes defining each symbol code. The third row evaluates all six exponents. The rows are connected by equality, not by a proof inference. Full factor by factor speech is attached to the formula occurrence.
Two equivalences define Var and Const. Each existential quantifier is bounded by x. The nested sequence coding is essential: x codes a singleton sequence containing the symbol code of a variable or a constant, rather than merely being that symbol code.
Term recognizes Goedel numbers of terms and C l Term recognizes Goedel numbers of closed terms. The source proof checks a finite formation sequence, requiring each entry to be a variable, a constant, or a function application to earlier terms. It requires the last entry to code the target term. It then bounds the formation sequence code by a primitive recursive expression. Omitting the variable case gives the closed term construction.
The reader is asked to prove that flatten is primitive recursive. Its input codes a sequence of term Goedel numbers; its output is the Goedel number of the single comma separated term string. The source provides no solution here, and none is added.
The function num maps the natural number n to the Goedel number of its object language numeral. The distinction between a number and the syntactic numeral denoting it is preserved.
The base value is the Goedel number of the zero term. The successor step concatenates the successor symbol and opening parenthesis, the previously constructed numeral string, and the closing parenthesis. All concatenations operate on codes and return the code of the resulting string.
Atom recognizes the Goedel numbers of atomic formulas. The source proof considers predicate applications, equality applications, and the selected falsity case. The argument length requirement and the argument list bound in the first clause have documented source caveats; the edition does not present those defective details as independently proved.
F r m recognizes Goedel numbers of formulas. The source sketches a formation sequence argument and leaves the detailed proof as the next exercise. Its assertion that every formation entry and the whole sequence code are less than the final formula code has a documented counterexample and remains visibly attributed to the source.
The reader is asked for a detailed proof that the formula code relation is primitive recursive, following the earlier term coding proof. The proposition and earlier proof references are retained. The exercise is unsolved in the source and in this edition.
Free Occ of x, z, and i holds exactly when the symbol at position i in the formula with Goedel number x is a free occurrence of the variable with Goedel number z. The second argument is a variable term Goedel number, not the variable symbol code. The proof is marked Exercise in the source and is not filled in.
The exercise asks for the proof of the preceding free occurrence proposition. It permits use of the fact that a substring of a formula that is itself a formula is a subformula. No solution is supplied.
Sent recognizes Goedel numbers of formulas with no free variable occurrences. A transparent reader correction adds the formula recognition conjunct omitted by the source display. The original formula and correction explanation remain available.
After requiring that x code a formula, quantify over every position less than the length of the coded sequence and every variable term code less than x. If the candidate z is a variable term code, its occurrence at the selected position must not be free. The added formula condition is explicitly recorded as a reader correction to the source.
The function Subst receives the Goedel numbers of a formula A, a replacement term t, and a variable u, in that order. It returns the Goedel number of A with every free occurrence of u replaced by t. The proposition concerns syntactic substitution, not evaluation of the terms or formulas.
The helper starts with the empty sequence code and processes one source position per step. At a free occurrence of the selected variable it concatenates the entire replacement term string. Otherwise it appends exactly one source symbol code. The terminal call processes the length of the original formula, so inserted symbols are not scanned again. The source does not perform variable renaming here.
Free For of x, y, and z holds exactly when the term with Goedel number y is free for the variable with Goedel number z in the formula with Goedel number x. This is the syntactic condition preventing capture of variables from the replacement term. The proof is marked Exercise and remains unsolved.
The reader is asked to prove the preceding Free For proposition. Its reference is retained, and no proof is added to the source exercise.
A finite sequence of sentences is coded by the tuple of its sentence codes. A sequent is coded by the ordered pair of its left sequence code and its right sequence code. A derivation consisting only of an initial sequent is coded by a pair beginning with zero. A one premise inference is coded by a four entry tuple beginning with one, followed by the immediate subderivation code, the conclusion sequent code, and the rule code. A two premise inference is coded by a five entry tuple beginning with two, followed by both immediate subderivation codes in premise order, the conclusion sequent code, and the rule code. The associated table assigns twenty rule codes. The code of a derivation and the code of its end sequent are distinct objects.
The first tuple has four entries: one, the code of pi sub one, the code of the conclusion sequent, and k. The second tuple has five entries: two, the code of pi sub one, the code of pi sub two, the code of the conclusion sequent, and k. The leading entry is the number of immediate premises and determines the index of the conclusion sequent and the final rule code.
The table pairs each inference rule with its numerical code. Codes one through six are left and right weakening, contraction, and exchange in that order. Codes seven through twelve are left and right negation, conjunction, and disjunction in that order. Codes thirteen through eighteen are left and right conditional, universal quantifier, and existential quantifier in that order. Cut has code nineteen and equality has code twenty. Each rule and code is available as an explicit row in the linearized table.
Begin with the initial sequent having capital A on both sides. Left conjunction gives the sequent with the conjunction of capital A and capital B on the left and capital A on the right. Right conditional then gives the empty antecedent sequent whose succedent is the implication from that conjunction to capital A. The initial derivation code is p sub zero. The next derivation code p sub one stores one premise and rule code nine. The final code stores one premise, p sub one, the final sequent code, and rule code fourteen. The fully expanded nested tuple preserves this same topology. Two unmatched parentheses in the source are explicitly ledgered reader repairs.
Three sequent nodes form one branch. The top initial sequent has capital A on both sides. Applying left conjunction yields the middle sequent with the conjunction of capital A and capital B on the left and capital A on the right. Applying right conditional to that middle node yields the bottom sequent with an empty left side and the implication from the conjunction to capital A on the right. Each inference has one premise.
The proposition states that Correct of p, the predicate checking the last inference in the derivation coded by p, is primitive recursive. The proof encodes initial sequents and checks individual inference rules using finite tuple projections and bounded searches. It explicitly develops right conjunction and right existential quantifier and then takes the disjunction over the rule codes together with the initial sequent case.
Two alternatives are joined by or. The first searches below the sequent code for a sentence code and requires identical singleton left and right sides. The second searches below the sequent code for a term code and requires an empty left side and a singleton right side containing the encoded equality of that term with itself. The equality expression is assembled from the equality symbol, parentheses, the two copies of the term code, and the comma. The bounded variables in the two alternatives have separate scopes.
The omitted subderivation pi sub one ends in a sequent with Gamma on the left and Delta followed by capital A on the right. The omitted subderivation pi sub two ends in a sequent with the same Gamma on the left and the same Delta followed by capital B on the right. Right conjunction uses those two ordered premises to conclude the sequent with Gamma on the left and Delta followed by the conjunction of capital A and capital B on the right. The blank top boxes are layout placeholders for omitted derivations, not additional axioms or empty sequents.
A single bounded existential scope chooses g, d, lower case a, and lower case b, each less than p. They represent the left context code, the shared right context code, and the two sentence codes. The conclusion extends the right context by the singleton containing the encoded conjunction. The first and second immediate subderivation end sequents extend that same context by the singleton containing the respective conjunct code. The tuple begins with two and the final rule code is ten. Lower case a and lower case b are numerical codes; capital A and capital B are the formulas whose codes they represent.
A single bounded existential scope chooses g, d, lower case a, x, and t, each less than p. The conclusion right side extends d by a singleton whose member is built from the existential quantifier code, variable code x, and formula code lower case a. The premise right side extends the same d by the singleton containing Subst of lower case a, t, and x. Here Subst is the numerical function on codes, whereas the preceding prose describes substitution of a term into a formula. The tuple begins with one and the rule code is eighteen. The source is a sketch; this reading does not silently add a new syntactic domain test or substitution side condition to its displayed formula.
First the code extracted as the end sequent must satisfy Sequent. Under that conjunction, the bracketed alternatives select a rule code and its corresponding Follows By predicate, ranging from left weakening at one to equality at twenty. A final alternative handles a zero premise derivation whose end sequent satisfies Initial Sequent. The last alternative is itself a conjunction. The source ellipsis stands for the intervening rule cases, not an extra condition or an unbounded search.
Define the Follows By predicates for cut, left conditional, equality, and right universal quantifier by the method of the preceding proposition. For right universal quantifier, also show primitive recursively that the eigenvariable does not occur in the end sequent. This remains an unsolved exercise. No definition, proof, or proposed solution is supplied here.
The proposition states that Deriv of p, recognizing the code of a correct derivation, is primitive recursive. Its proof checks Correct at every entry of the finite sequence of subtree codes. The entry index is bounded by the length of Subtree Sequence of p. The isolated d in the predicate name and the missing closing parenthesis in its argument are explicitly ledgered reader repairs.
Fix a primitive recursive set Gamma of sentences. Proof from Gamma of x and y relates a derivation code x to a sentence code y when the derivation ends with a finite left side drawn from Gamma and the sole right side sentence has code y. The proof combines Deriv of x, a bounded membership check on every left side sentence code, and a singleton right side check. Gamma is the fixed premise set, Gamma sub zero is the finite antecedent, x codes the derivation, and y codes its conclusion sentence.
Proof from Gamma of x and y is defined by a conjunction of three requirements. First x codes a correct derivation. Second every entry of its finite left end sequent side satisfies R sub Gamma. Third its right side has length one and the sole entry is y. The bounded universal quantifier applies only to the membership test on the left side; the right side requirements are conjoined outside that quantifier.
An assumption is coded by a tuple of its zero arity, formula code, and label. An inference is coded by its arity, the immediate subderivation codes in order, its conclusion code, discharge label, and rule number. The separate cases distinguish an assumption from a zero premise inference.
Four rows give the tuple forms for zero, one, two, and three premises. In every case the number of child codes matches the initial arity; the final three entries are conclusion code, discharge label, and rule code.
The table assigns sixteen rule codes. It pairs introduction and elimination for conjunction, disjunction, conditional, and negation; then intuitionistic and classical falsity rules; then introduction and elimination for universal quantification, existential quantification, and equality. The reading gives every rule and its corresponding code.
Assume capital A and capital B under label one, infer capital A by conjunction elimination, and discharge the assumption by conditional introduction to infer if capital A and capital B then capital A. The nested tuple codes record both inferences and the original assumption.
A single branch has three nodes. The leaf is capital A and capital B under discharge label one. Conjunction elimination yields capital A without discharging it. Conditional introduction yields if capital A and capital B then capital A and discharges the original label one assumption.
The proposition asserts that two relations are primitive recursive: a formula occurs as an assumption with a specified label, and all assumptions with a specified label have that same formula. Its proof uses coded subtrees and bounded quantification.
Correct of a derivation code tests the final inference. The proof supplies conjunction introduction, equality introduction, conditional introduction, and existential introduction examples, then combines the numbered rule cases with the assumption case. It is distinct from correctness of every inference.
The left unexpanded subderivation delta sub one concludes capital A. The right unexpanded subderivation delta sub two concludes capital B. A binary conjunction introduction combines their conclusions into capital A and capital B. No assumptions are discharged by this last step.
The code has two children, no discharge label, and rule code one. Its end formula code concatenates the first child conclusion, the conjunction symbol, and the second child conclusion, with parentheses.
The code has zero premises and no discharge. A bounded closed term code is repeated on both sides of the coded equality. The separate Correct definition selects the appropriate last rule code.
The code has one child. A bounded antecedent code satisfies the discharge predicate for that child and the last inference label. The conclusion code is the conditional from that antecedent to the child conclusion.
The code has one child and no discharge. Bounded witnesses give a formula code, variable code, and closed term code. Substitution produces the child conclusion, and existential quantification of the formula produces the parent conclusion.
A sentence test is conjoined with the disjunction of the numbered rule cases and the assumption case. The source omitted the grouping around that entire disjunction; the explicit correction supplies the scope required by the following prose.
The exercise asks for conditional elimination, equality elimination, disjunction elimination, and universal introduction tests. For universal introduction it also asks for a primitive recursive eigenvariable condition, using Open Assumption if desired. No definitions or solutions are supplied here.
A derivation is correct when every coded subtree ends in a correct inference. The proof universally checks Correct over the sequence of subtree codes.
Open Assumption relates a formula code and a derivation code when at least one occurrence of the formula remains undischarged. The proof distinguishes occurrences of the same formula along separate paths. Source anomalies in its displayed bound and treatment of label zero are preserved with notes.
The source searches for a sequence starting at the root derivation code, ending at a labelled assumption code, and following immediate child links without the matching discharge label. Its strict path bound and label zero handling have explicit anomaly notes; no new path algorithm is substituted.
For a primitive recursive set of sentences Gamma, the proposition asserts that a code is a derivation of the indicated sentence from undischarged assumptions in Gamma by a primitive recursive relation.
The displayed predicate requires a correct derivation code x, end formula code y, and membership in Gamma for every open assumption code below x.
The code of an axiomatic derivation is the number coding the sequence of the codes of its formulas, in the order in which the formulas occur as proof lines. The sequence and the number coding that sequence are distinct objects.
The example displays three proof formulas, followed by the tuple of their Goedel numbers in exactly the same order. The third formula is obtained by modus ponens from the first two; the original derivation prints formulas only, without line justifications.
Line one is if capital B then capital B or capital A. Line two is the conditional from line one to if capital A then line one. Line three is if capital A then line one. The proof dependencies are from lines one and two to line three by modus ponens; this explanatory dependency is not a printed source annotation.
The displayed tuple has three entries: the Goedel number of each formula in the preceding example, in line order. Tuple entries are numbers coding formulas, not the formulas themselves.
The proposition lists axiom recognition, justification of a line by modus ponens, justification of a line by a quantifier rule, and correctness of the entire axiomatic derivation. The proof gives explicit arithmetic tests and leaves the other quantifier rule version as an exercise.
Bounded sentence codes for capital B and capital C are combined by coded concatenation with the codes of the conditional symbols and parentheses to recognize the code of an instance of if capital B then, if capital C then capital B. Every operand of this arithmetic concatenation is a code, not a bare symbol or formula.
Two indices earlier than the current line are bounded witnesses. The numerical component for one earlier line must equal the code of the conditional whose antecedent is the formula on the other earlier line and whose consequent is the formula on the current line.
The test compares a preceding substituted conditional with the current universally quantified conditional. A source-determined missing earlier-line quantifier is explicitly supplied. The missing freshness test for the quantified matrix is instead preserved as a source anomaly, not silently added.
Three tasks ask for recognition of the conjunction axiom schema, recognition of universal instantiation, and the second quantifier rule test. The tasks remain unsolved.
The proposition concerns proofs relative to a primitive recursive sentence set. Its proof then explicitly changes the certificate convention: x codes an assumption free derivation of a nested conditional with antecedents from Gamma and the target sentence as consequent.
The recursive helper starts with the target sentence code and prepends antecedents from a coded sequence. Its recursive call typo is explicitly corrected to hCond. The final predicate checks an assumption free derivation ending with the nested conditional and that all antecedents belong to Gamma. This is the modified certificate convention stated in the preceding prose.
the proposition that the formula code predicate is primitive recursive
the proposition that the term code predicate is primitive recursive
the proposition that the free for relation is primitive recursive
the proposition on primitive recursive inference correctness
the proposition on primitive recursive inference correctness
the proposition on primitive recursive inference correctness