Automated Reasoning in Higher Order Logic
This page was created and is maintained by Chad E Brown.
Chapter 1: Propositional Calculus.
Chapter 3: Provability and Refutability.
Chapter 4: Further Topics in First-Order Logic.
Chapter 6: Formalized Number Theory.
Chapter 7: Incompleteness and Undecidability.
Chapter 1: Propositional Calculus. The set of propositional wff's (for system P) is generated from propositional variables by negation and disjunction (and the principle of induction on the construction of a wff is introduced)--the other operators are introduced as abbreviations. Substitution is introduced as a function from formulas (meaning arbitrary sequences in the language--not wff's) to formulas. Next, system P is given by three axiom schemas and modus ponens [in terms of negation and disjunction] as an inference rule [Hilbert Style!]. The notion of proof (from hypotheses) follows. Basic theorems and derived rules are proven.
Truth table semantics are given (as functions from propositional variables to the set {T,F}), along with the definitions of tautology [=valid in this context], contradiction, and satisfaction.
Soundness (that is, every theorem is a tautology) is proven by induction on the length of proofs (that is, by checking that the axioms are tautologies and that modus ponens preserves the property of being a tautology.
Absolute consistency (there is an unprovable wff) and consistency with respect to negation (there is no wff such that it and its negation are provable) are defined for general logical systems and a condition is given under which the two become equivalent (the provability of "A implies . not A implies B" in a system with modus ponens). P is proven consistent (in both senses--as they are equivalent for P).
Completeness (that is, every tautology is a theorem) is proven by induction on the number of propositional variables in the tautology using the Deduction Theorem and Lemma 1202 (p1^phi,...,pn^phi |- A^phi where B^phi is B if Vphi(B)=T and is -B if Vphi[B]=F). Lemma 1202 follows by induction on A. So, the set of theorems equals the set of tautologies.
Independence is discussed and the axiom schemata and rule of inference of P are all proven independent (using nonstandard truth tables with three truth values for the axiom schemata). So, removing an axiom or rule results in a genuinely smaller set of theorems.
Substitutivity of Equivalence is proven by induction on the number of propositional connectives of the wff before substitution of subformulas. The fact that any truth function can be represented by a wff in disjunctive normal form is proven. Together these imply that every wff can be put into disjunctive normal form.
A complete set of propositional connectives is sufficient to define all the truth functions. Complete sets of propositional connectives are given.
Negation normal form is defined, and the two-dimensional representation is introduced (conjuncts=vertical paths and disjuncts=horizontal paths). The set of conjuncts (vertical paths) is inductively defined. If a wff is in negation normal form, then a truth assignment satisfies it iff it satisfies some conjunct (vertical path). It follows that a wff in negation normal form is a contradiction iff every vertical path contains complementary literals.
The fact that satisfiability and consistency of finite sets of wff's is coextensive is a trivial consequence of soundness and completeness (using the Deduction Theorem). We can extend this to infinite sets using compactness (note that usually we prove compactness from completeness!). Compactness is proven directly by inductively extending a truth assignment on the propositional variables p1, p2, . . . so that they preserve an "extendability" property. Does this require Konig's Lemma?
Finally, ground resolution is defined and proven complete in the sense that a set of clauses is contradictory iff there is a resolution refutation. (This is called the "Ground Resolution Theorem". The proof in one direction reduces to the case of a finite set of clauses S by compactness. We argue by induction on e(C) = #(S1)+...+#(Sn)-n where #(S) is the number of literals in a clause. Note when e(C) <= 0 we either have an empty clause in the set or all unit clauses. When e(C) > 0 we must either have the empty clause in C or a clause with at least two literals.) Note that the resolution rule is a "special case" [in some sense] of the cut rule. Modus ponens is a special case of the resolution rule.
Chapter 2: First-Order Logic. System F of first-order logic is introduced in the usual way (with disjunction, negation, and universal quantification as primitive)--except he allows propositional, function and relation variables over which we cannot quantify. The rules of inference are Modus Ponens and Generalization [again, Hilbert style]. The axiom schemata include three propositional axioms which (with MP) generate all the tautologies (so system F includes system P--this also gives "Rule P") and a schema internalizing universal instantiation and a schema allowing disjunction to commute with the universal quantifier when one disjunct does not contain free occurrences of the bound variable. This, of course, leads to a definition of the set of theorems of the system F (as well as provability from hypotheses).
F is proven absolutely consistent and consistent with respect to negation. This follows from consistency of system P (by erasing quantifiers and replacing all atomic wffs with a fixed propositional variable). Then derived rules of inference are proven.
The system F is modified to include existential quantifiers as primitive and called system E. A wff G in E is in prenex normal form iff no vacuous quantifier occurs and no quantifier occurs in the scope of a propositional connective. The scope of the initial string of quantifiers of a wff in prenex normal form is called the matrix of the wff. The initial string of quantifiers is called the prefix. In fact, if a wff D is rectified (that is, D has no vacuous quantifiers and there is no overloading of variable names), then we can define "the" prenex normal form by simply "pulling out" the quantifiers (in one step) changing the quantifier if it is a negative occurrence. (We pull them out in the same order as they occur [left to right] in D.) Every wff has a prenex normal form, and "the" prenex normal form of a rectified wff is a prenex normal form for the wff. This is proven by induction on the sum (over all quantifiers) of the number of occurrences of propositional connectives in whose scope the given quantifier lies. The induction step appears to correspond to Herbrand's method of "pulling out" quantifiers.
As for semantics of F, an interpretation is a domain and a mapping from the constants of F to individuals/truth values/functions/relations as appropriate. An assignment into an interpretation maps variables to individuals/truth values/functions/relations as appropriate. We use this to define the value of terms and wffs with respect to an assignment in an interpretation, so that terms map to individuals and wffs map to truth values. This leads to definitions of satisfaction, validity, contradictory [unsatisfiability], and models. Soundness is proven.
Next, independence of the rules of inference and axiom schemata of F are proven. First, we have a lemma that any theorem must contain a disjunction [consider the singleton domain]. Modus Ponens is independent since we cannot prove "p or not p" without it. The propositional axioms are independent by the methods used for system P (by deleting quantifiers and replacing atomic wffs with propositional variables). Generalization is independent since "forall x . p implies p" [slight modification from the book] is not provable without generalization (as can be seen by modifying the "value" function to send any formula with an initial universal quantifier to false). Axiom 4 is independent since all the other axioms and rules of inference are sound if universal quantifiers are replaced with existential quantifiers. Axiom 5 is shown independent by replacing "forall x B" by a contradiction whenever B contains no disjunctions--then we consider the property of wffs A which holds if A is provable and A' [via the replacements] is valid. The general idea in each case is to consider a property of wffs which all the axioms have and all the rules preserve--except the one whose independence is to be established.
The notions of extension and conservative extensions of first-order theories are defined and basic theorems are proven. Then an abstract consistency class (of sets of sentences) is defined. Such a class must be closed under subsets and satisfy properties relating to logical connectives and quantifiers. It amounts to saying each set of sentences is consistent and can be extended to a set in the class which has (any "unused" constants as) a witness. Examples: The class of consistent sets of sentences. Any abstract consistency class can be extended to an abstract consistency class of finite character--i.e., S is in the class iff every finite subset of S is in the class (stronger than just closure under subsets). Smullyan's Unifying Principle states that if Gamma is an abstract consistency class and S in Gamma is a "sufficiently pure" set of sentences (i.e., there is a set of constants unused in S the same cardinality as the language) has a frugal model. This is proven by extending S by transfinite induction to be maximally consistent and contain witnesses (remaining in Gamma at each step). It follows that every consistent set of sentences has a frugal model. From this, we can deduce:
1. Every consistent set of sentences has a frugal model.
2. The Generalized Completeness Theorem: If S is a set of sentences and A is valid in all frugal models of S, then S|-A.
3. Godel's Completeness Theorem: Every valid wff of F is a theorem.
4. Lowenheim's Theorem: If A is valid in every countable interpretation, then A is valid.
5. A set of sentences is consistent iff it has a model.
6. The Lowenheim-Skolem Theorem: Every set of sentences which has a model has a countable model.
7. The Compactness Theorem: A set S of sentences has a model iff every finite subset of S has a model.
An appendix shows how to prove completeness (by extending consistent sets of sentences to be maximally consistent with witnesses) without relying on abstract consistency and Smullyan's Unifying Principle.
Finally, we can add equality to first-order logic by including the equality constant, Axiom 6 (reflexivity), and Axiom Schema 7 (Substitutivity). Equality-interpretations & equality-models are defined as before (except equality must be interpreted as identity). Soundness follows of course. Elementary equivalence is defined and it is proven that every model for Axioms 6 and 7 is elementarily equivalent (over first-order logic without equality) to an equality-model. Completeness and Lowenheim-Skolem-Tarski (i.e., we have equality-models of every cardinality at least the cardinality of the language) follows. Finally, technically we can prove any theorem of first-order logic with equality in first-order logic (i.e., without Axioms 6 & Axiom Schema 7) by converting the theorem to an implication with the theorem as conclusion and reflexivity and substitution instances of formula and relation constants occurring in the theorem as hypotheses).
Chapter 3: Provability and Refutability. The purpose of this chapter is to introduce and compare different proof procedures for first-order logic. First, natural deduction (System N) is described. Rules: Hyp, Expanding/Rearranging Hyps, Deduction, Rule P, Negation, Indirect, Cases, alpha-beta, UG, EG, UI, Rule C. System N proves the same theorems as System F--so we have soundness and completeness for System N--though these facts are left as exercises. He notes that to prove an existential formula in System N, we cannot always prove the formula for a specific term (or even a finite disjunction with different terms). The example he gives is "exists x forall y . Px implies Py" where a semantic argument shows that no terms can "name" the x (use a domain with two individuals where every term is interpreted as one and the 'x' is the other). Contrast this result with Herbrand's Theorem.
Gentzen's (Hauptsatz) Theorem (and the subformula property) is discussed by introducing a System G which is similar to Gentzen's LJ/LK Sequent Calculi. Andrew's System G operates with disjunctions (not with sequents)--deriving theorems from "not A or A" (with A atomic) using "introduction" style rules (double negation, conjunction, universal generalization, and existential generalization) and alpha-beta. System G is cut-free. Using Smullyan's Unifying Principle, System G is equivalent to System F. (Here the abstract consistency class consists of sets {C1,...,Cn} such that G does not prove "-C1 or . . . or -C2".) Since the "cut-rule" is sound for System F (by Rule P), we have that it is sound for System G (so we could form the System G+ as G with cut and obtain the same set of theorems). Note that this (semantic) proof does not give a construction of a cut-free proof from a proof with cuts, as Gentzen's proof did.
Semantic Tableau is discussed (attributed to Beth, Hintikka, and Schutte). These arrange sentences into a downard dyadic tree (these can be formalized using a binary relation satisfying "tree" properties--which lead to definitions of "below," "terminal node/leaf," and "branch"). A semantic tableau (for a set of sentences as hypotheses) is a tree of sentences constructed by induction from Hyp, Double-negation, Conjunction Elimination [left/right], Universal Instantiation, Existential Instantiation (with restriction on constant), Disjunction Elimination (giving two branches). A branch is closed if it contains a sentence and its negation. A tableau is closed if all branches are closed. Smullyan's Unifying Principle is used to show that a set of sentences S of F has no model iff S has a closed semantic tableau (well, one direction is obvious--the other direction we use Smullyan's Unifying Principle on the class of sets of sentences which have no closed tableau). The last paragraph (p. 122) discusses how semantic tableau's can be used to search for proofs in a very systematic way. Only Universal Instantiation may need to be applied more than once (with different choices). The choices can be restricted by looking at other function and constant symbols in the tableau. Without function symbols in the language, the number of choices is finite! However, Existential Introduction may keep expanding that finite set.
Next, Skolemization is discussed--that is, converting a sentence B of (a countable formulation of) F into a universal sentence star-B of F-star (an expansion of F with countably many new individual and function constants of each arity). This is accomplished by inductively defining a mapping from sentences of F (enumerated) to sentences of F-star removing existential quantifiers (i.e., negative universal quantifiers) inductively from left to right and replacing the existential bound variable with a new (not yet used) function constant depending on the free variables in the scope of the quantifier. (Two other alternatives include making the dependent variables be the ones universally quantified in the current scope [Skolem/Herbrand], and the ones which are universally quantified in the scope after anti-prenexing/mini-scoping [Herbrand]. Andrews' method results in the fewest variables as arguments in the Skolem terms.) For any sentence B of F, F-star proves star-B implies B (use the negative version of substitution of implication). Given any set of sentences G of F, let G-star be the set of Skolemized forms of B (set of sentences of F-star). Then G-star has a model iff G has a model (and F-star union G-star is a conservative extension of F union G). (The hard direction is proven by starting with an enumerable [hence well-ordered] model of G and choosing interpretations for the existential individual and function constants by using the "least" operator.) Thus, a sentence B of F is satisfiable iff star-B is satisfiable. Also, if A is any wff (in F), then A is valid iff star-not-universal-closure(A) is unsatisfiable.
This naturally leads to the notion of refuting wff's instead of proving sentences. A resolution style refutation system R is introduced for this purpose. Here we derive wff's (including an "empty disjunction" wff which may stand for "false" or nothing if used with a disjunction) starting from a given set S of wff's by the rules: Disjunction (for rearranging disjunctions), simplification [factoring], substitution, cut, negation elimination, conjunction elimination, and universal instantiation (by simply removing the quantifier). An R-refutation of S is an R-derivation of the "empty disjunction" from S. Given any set S of universal sentences, S is R-refutable iff S is unsatisfiable. This is proven by Smullyan's Unifying Principle with the abstract class being the set of finite sets of universal sentences which are not R-refutable. It follows that for any wff A (in F), we can form star-not-universal-closure(A) (in F-star) and then form the conjunctive normal form N1 and . . . and Nk (so, each Ni is a disjunction of literals [clause]). Then, A is valid iff {N1,...,Nk} has no model iff the empty disjunction can be derived from {N1,...,Nk} using only Disjunction, Simplification, Substitution, and Cut. Of course, this is essentially resolution (without using unification to combine substitution and cut) and dates back to J. A. Robinson.
Next, Herbrand's Theorem is discussed. Again, the emphasis is on refuting universal sentences--in fact, here we work with negation normal forms. A compound instance (c-instance) of such a formula is defined much as the deep formula of an expansion tree. A simple instance is one in which we do not get a conjunction [of more than one conjunct] at (universal) quantifier nodes. Every c-instance is equivalent to a conjunction of simple instances. For any two c-instances there is a third c-instance which implies the conjunction of the other two. Given a universal nnf D, either some c-instance is a t-f contradiction or there is some truth assignment (to all the atomic wff's involved) which simultaneously satisfies all c-instances. This follows by Compactness for the propositional system P. The Herbrand universe H(D) of a sentence D is the set of terms constructed from the individual and function constants in D (with an extra individual constant thrown in if none is in D already). Herbrand's Theorem states that given a wff A we can construct D as a negation normal form of star-not-universal-closure(A) and A is valid iff D has a compound Herbrand instance (c-instance using only terms from H(D)) which is a truth-functional contradiction. It follows that A is valid iff some conjunction of simple Herbrand instances of D is a t-f contradiction. Also, if B is a sentence and D is a nnf of star-B, then B is satisfiable iff the set of simple Herbrand instances of D is t-f satisfiable. Herbrand's Theorem is, of course, essentially the basis for expansion trees as used in TPS.
Actually, Herbrand proved his result (in his thesis) completely syntactically using a cut-free first-order system FH with quantifier-free tautologies as axioms and rules for introducing and manipulating quantifiers (but no modus ponens rule) and a Hilbert-style system (with modus ponens) similar to F. He showed that for any wff A, "FH proves A" implies "F proves A" implies "A has the Herbrand Property" implies "FH proves A." Here, A has the Herbrand Property iff some Herbrand expansion (negation of the compound Herbrand instances which Andrews considers) is tautologous.
Also, there was a mistake in Herbrand's proof pointed out by Andrews, Drebin and Aanderaa in 1963 and corrected by Dreben and Denton in 1966.
Finally, first-order unification is discussed--including the definition of substitutions being more general than others if they factor through other substitutions. Robinson's unification algorithm is given (using disagreement pairs to extend the substitution) and it is proven that it either halts on failure if there are no unifiers or halts with a most general unifier if unifiers do exist.
Chapter 4: Further Topics in First-Order Logic. We can map wff's of F to "dual" wff's by interchanging dual pairs of [abbreviations for] logical connectives and quantifiers. The dual pairs are (forall,exists), (and,or), (equivalence,xor), (nand,nor), and two for implies [in each direction]. If we perform this on the unabbreviated form of A we get the "principal dual" Ad. Any two duals of a wff are provably equivalent, and the double principal dual (or any double dual) is provably equivalent to the original formula. Given any interpretation and assignment satisfying A, we can define a new [dual] model by reinterpreting predicate constants as the complement of their original interpretations. This new model satisfies the negation of the dual of A. So, (by completeness) if A is provable, then the negation of its dual is provable. Also, if "A implies B" is provable, then "Bd implies Ad" is provable. And if "A equiv B" is provable, then "Ad equiv Bd" is provable.
An interpolation sentence for "H implies K" is a sentence J so that "H implies J" and "J implies K" are both valid, all individual constants in J appear in both H and K, and all propositional or predicate constants occurring positively [negatively] in J occurs positively [negatively] in both H and K. The Craig-Lyndon Interpolation Theorem implies that every valid sentence "H implies K" has an interpolation sentence. This is proven using Smullyan's Unifying Principle on the class of all sets of sentences which can be partitioned into two sets which have no interpolation sentence (where here we have a generalized notion of interpolation sentence). Then we note that since {H,-K} has no model, it must not be in the class, and so the pair ({H},{-K}) has an interpolation sentence.
Beth's Definability Theorem (H defines P implicitly iff P is explicitly definable from H) follows from the interpolation theorem. We interpolate "H and Pc1...cn implies [H' implies P'c1...cn]" where the c1,...,cn are otherwise unused individual constants and H' is H with P replaced by P'. By replacing the ci's in the interpolation sentence by new xi variables, we obtain an explicit definition of P from H (which furthermore satisfies constraints on what individual constants and predicate constants can occur in the definition).
Chapter 5: Type Theory. Omega-order logic is introduced by starting with system F (without function constants or variables) and allowing quantification over relational variables (second order), then allowing relations over relations (third order), quantifying over these (fourth order), and so on. This leads to the relational system F-omega (which Leivant calls [relational] finite order logic and attributes to Schutte 1960). F-omega is axiomatized in a Hilbert-style (as system F was) with Modus Ponens and Generalization as rules and three propositional axioms [where two correspond to simplification and weakening], two universal quantifier axioms, and finally the comprehension axioms and axioms of extensionality.
However, Andrews uses Q0 instead of F-omega. Q0 takes equality (and description) as primitive and defines logic in terms of equality. While equality can be defined in terms of logic (using Leibniz), Henkin-style general models of such systems may not satisfy extensionality (see Andrews 1972) and Leibniz equality may not be interpreted as the identity relation. If we force ourselves to only consider models in which equality is interpreted as identity (it is enough to assume the identity relations are in the appropriate domains), this determines the interpretation of logical constants and quantifiers--so, we may as well take equality as primitive.
So, Q0 is generated by equality (at each type), description (at the type of individuals), variables, lambda abstraction, and application. We have an obvious principle of induction on the construction of a wff. The logical constants, operators, and quantifiers are defined. Axioms 1-5 are given (1: T & F exhaust type o, 2: internal law of identity, 3: extensionality, 4: lambda conversion, 5: description). The sole rule of inference is Rule R, the rule of replacement. The notion of proof follows, and with a few technical details (using Rule R'--replacement with a variable restriction) we have proofs from hypotheses. The basic theorems and metatheorems are proven: Equality rules, eta-conversion, alpha-beta, lambda-conversion [beta], propositional laws, Universal Instantiation, Rule T, Universal Generalization, Substitution, Cases, Modus Ponens, Rule P, "Rule Q", Deduction, Existential Generalization, Comprehension (which is a theorem here since we can name the terms using lambda-abstraction), and Rule C.
Next, Axiom 2 is extended to apply to functions instead of just predicates, which allows us to further "internalize" replacement. The Sigma1 "exists-unique" operator is defined as equality to a unit set. This operator is characterized in four ways. Description is defined at other types and proven (by induction on types) to satisfy the property of being left-inverse to equality at all types. Description is related to unique existence. The "Conditional" operator is defined and proven to have the appropriate property. Also, he notes how to define the axiom of choice (at a type alpha) by saying there exists a choice function from nonempty sets to elements of such sets.
Henkin-style general models are defined as semantics for Q0. First, a frame is simply a collection of domains where Do={T,F}, Di is the domain of individuals, and each D_{alpha beta} is a subset of the collection of functions from D_beta to D_alpha. An interpretation is a frame and a function mapping constants of Q0 to the appropriate domains, taking each Q to the appropriate identity relation (as a Curried characteristic function, of course), and taking the description operator to some map from sets of individuals to individuals that takes singletons to their unique element. An assignment maps variables to elements of domains. A general model is an interpretation for which any assignment can be extended to a "value" function on all wff's of Q0 (the main issue being the existence of functions in the appropriate domains). Standard models have all functions in their function domains. The definitions of "satisfies" [with respect to a model and assignment], "satisfiability" [in a model], "validity" [in a fixed model, in the general sense, in the standard sense], and "models for a set of wffs" follow.
Soundness is proven, and Consistency (if a set of wffs has a model, it is consistent) follows. Every finite model is standard (because we can define any function in terms of a finite number of elements of the domain--accessible through an assignment function) [attributed to Henkin 1963]. Isomorphisms are defined in the usual way (except we can leave off injectivity, since it follows from the other conditions). The value function commutes with isomorphisms, from which it follows that the same wffs are valid in isomorphic models.
Henkin's Completeness Theorem is shown by extending a consistent set of sentences to be a consistent, complete, extensionally complete (meaning there are terms which act as witness whenever two function terms are not equal) in an expansion Q0+ of Q0 (where the cardinality of the language does not increase--the expansion contains card(L(Q0))-many new constants of each type). (The Extension Lemma allows us to extend a set of sentences in this way.) Henkin's Theorem follows: We have a "frugal" (the cardinality of each domain is less than or equal to the cardinality of the language) general model for any consistent set of sentences (by taking a "term" model with equivalence classes of terms). Henkin's Completeness Theorem follows, and states that provability is equivalent to validity, provability from a set G is equivalent to validity in all general models of G, and provability from a set G is equivalent to validity in all frugal general models of G. Note that this was not proven using Smullyan's Unifying Principle. However, Smullyan's Unifying Principle modified for [a version of] type theory is used in Andrew's 1971 ("Resolution in Type Theory").
(Weak) Compactness and the usual applications follow from Completeness. Every [infinite] frugal model for which card(Di) >= card(L(Q0)) is nonstandard (by Cantor's Theorem). Every set of sentences (of Q0--with no extra constants) which has an infinite model has a nonstandard model. So, there's a problem with using the language to distinguish between standard and nonstandard models. Assuming the background set theory satisfies AC, it follows that AC is valid in every standard model. However, AC is not valid in all general models.
Chapter 6: Formalized Number Theory. In Q0, we can define equipollence of sets and cardinality ["number classes"]. A cardinal number is a class of equipollent sets of a given type. In order to ensure all finite cardinals exist and are distinct, we assume an axiom of infinity. This gives Q0-inf, which is Q0 with Axiom 6: "there exists an irreflexive, partial ordering (of the individuals) with no maximal element" [attributed to Bernays and Schonfinkel 1928]. Two other axioms of infinity are introduced (InfI: "there is a set with a proper subset of the same cardinality" [essentially, the pigeon-hole principle fails], InfII: "there exists a 'zero' and 'successor' satisfying Peano's Axioms without Induction"). InfI and InfII are equivalent, and both imply Axiom 6.
In Q0-inf, we define 0 to be the class of the empty set of individuals. Then Successor is defined to take a class of sets N and return the class of sets from which we can remove an element and obtain a set in N. The set of naturals is defined as the intersection of all sets containing 0 and closed under successor. Finite is defined to be "member of a natural number." Also, relativized quantifiers are introduced (as abbreviations). These are necessary because the set of natural numbers is not the entire domain of type sigma = o(oi).
Peano's Postulates are proven. In particular, induction follows easily from the definition of the naturals--indicating the power of higher order logic. Axiom 6 is only needed to show that the successor function is injective.
Representability (of naturals, functions on naturals, and relations on naturals) is defined (as the existence of a closed formula such that Q0-inf proves it satisfies the appropriate equations on numerals to represent the function or relation). The numeral S^n0 represents the number n. Q_{o sigma sigma} represents equality relation on naturals.
We can define an ordering on the naturals as the intersection of relations which contain the first argument and are closed under successor. (Note: The set of naturals is the same as [<= 0]). Properties of the ordering are proven until it is proven that the ordering represents the usual ordering on the natural numbers. This allows us to reduce bounded quantifiers to checking a finite number of cases.
In fact, the ordering is a well-ordering on the natural numbers, which allows us to define a minimization operator mu (as "the" [description] smallest natural satisfying a predicate). mu is proven to have the obvious properties [if p is nonempty, then mu p is a natural, satisfies p, and is less than anything else satisfying p]. If we start with a representable regular numerical relation and define a numerical function by minimization, the mu operator can be used to represent the function. (Representability is closed under minimization of regular relations.) (Note: We can also minimize functions using the relation "function = 1.")
The representable functions/relations are shown to be closed under primitive recursion by defining a recursion operator R. Rgh defines a function satisfying f(0) = g & f(Sn) = h(n,f(n)). R actually defines the graph of such a function by intersecting the appropriate relations and then uses description to extract values of the function. (Note that we may treat any other arguments as parameters.) Thus, every (general) recursive function is representable in Q0-inf. Church's Thesis (that every effectively computable function is general recursive) is discussed [Church 1936].
Finally, the class PR of primitive recursive functions (PRF) and relations (PRR) is explored. Constant functions are p.r. PRF is closed under explicit definitions [generalization of composition] and under generalizations of primitive recursion [allowing the recursion argument to be in different positions]. These results allow us to conclude that the usual numerical functions and relations (addition, multiplication, exponentiation, bounded products, factorial, predecessor, modified subtraction, signum, less-than, and equality) are p.r. Relations defined from p.r. relations using propositional connectives are p.r. PRR is closed under bounded quantification (where the bound function is p.r.), and the corresponding result for bounded minimization and maximization holds. PRF is closed under definition by PRR-determined cases. Divides, Prime, and the "nth odd prime" function are all p.r. We can use these to code sequences of naturals into a natural by defining the p.r. function Gl (for "Glied"--"term" in German [Godel 1931]) so that n Gl x is the exponent of Pr(n) in the prime factorization of x. Also, we define the "extent" [length] function so that E(x) is the largest n such that Pr(n) divides x. Finally, the concatenation function on such sequences is p.r. and we can recover exponents to powers of arbitrary primes using the p.r. function Lg.
Chapter 7: Incompleteness and Undecidability. A Godel numbering is applied to the language of Q0-inf (types using primes 3 & 5, the remaining odd primes used for the symbols of the language). Recognizing variables, wff's, axioms (of Q0-inf), and proofs (in Q0-inf) can be done p.r. functions (hence, each can be represented). (In order to avoid changing the Godel numbering, we only consider "pure" extensions of logistic systems [same wff's and rules of inference]--this restriction is not essential.) Also, we can represent the function which maps each natural to the Godel number of the corresponding numeral. At this point we can prove that every representable function is recursive by building numerical n+2-ary relations which allow us to use the mu-operator to search for the proof p and number z such that p proves [f x1 ... xn]=z (where the Godel number of f and the naturals x1,...,xn are specified by the first n+1 arguments). Then we can plug the Godel number for the formula representing the function into the first argument of the relation. Since the function must be total (by definition of representability), the relation is regular, and we can apply the mu-operator to the last argument, and extract the value of the function from the value-proof pair. (Incidentally, this implies recursive functions can be defined by one application of a mu-operator to a p.r. relation--and also that all recursive functions can be represented in the above manner [Kleene's "Normal Form Theorem"].)
Next, consistency, omega-consistency, completeness, omega-completeness, and essential incompleteness are defined. Omega-consistency implies consistency. It is easy to diagonalize closed formulas of type (osigma) in Q0-inf (see X7105 which is reminiscent of a fixed point theorem). Forming the sentence "I am not provable" gives Godel's Incompleteness Theorem (so that every omega-consistent, recursively axiomatized pure extension of Q0-inf is incomplete [and consistency implies omega-incompleteness]). The argument can be internalized. This gives Godel's Second Incompleteness Theorem, that if A is any consistent recursively axiomatized pure extension of Q0-inf, then A cannot prove Consis-A (where Consis-A is the sentence not-Theorem_"F"_).
With a few more "internalization" results, Lob's Theorem is proven: That D is provable iff 'Theorem _"D"_ implies D' is provable (using the sentence "If I am provable, then D."). From this it follows that given any sentence D such that 'D = Theorem_"D"_' is provable, D is provable. Godel's Second Incompleteness Theorem also follows from this, since Consis is equivalent to 'F=Theorem_"F"_'.
Godel's Theorem was strengthened (by replacing omega-consistency with consistency) by Rosser (giving the Godel-Rosser Theorem [Rosser 1936]) by forming the sentence "If I am provable, then my negation has a shorter proof." So, no consistent complete extension of Q0-inf is recursively axiomatizable, and given any model of Q0-inf, the set of sentences true in the model is neither recursive nor even recursively axiomatizable.
Next, the sentence Inf-III is introduced (which is Peano with second order induction and a definition for description on non-unit sets). Inf-III has a unique standard model N up to isomorphism. Since, Inf-III implies Axiom 6, it follows that Q0-inf is consistent. Also, Q0-inf is essentially incomplete (by Godel-Rosser and consistency of Q0-inf). Inf-III can be used to show that the set of wffs valid in the standard sense is not recursively axiomatizable (hence, not recursive). If we could axiomatize them, say by B, then we can extend B by Inf-III to obtain A. N is a model of A, and the only standard model. So, truth of C in N reduces to provability of "Inf-III implies C" in B. So, we have recursively axiomatized truth in N--contradiction.
Any consistent pure extension of Q0-inf is undecidable (the set of [Godel numbers of] theorems is not recursive--use the statement that says "I am not a theorem"--where theoremhood is presumed to be representable). In fact, any extension B of Q0 which is consistent with Axiom 6 is undecidable (by reducing the decision problem of B union {Axiom 6} [undecidable by above] to the one for B). So, Q0 is undecidable. Since any extension of Q0 which is recursively axiomatizable and complete is decidable, we have another proof of Godel-Rosser.
Definability of relations in a general model, and the special case of definability of numerical relations in a general model are introduced. Of course, representability implies definability. Tarski's Theorem is proven (that truth in a model M is not definable in M) using the sentence "I am not true" (under the assumption that truth is definable). The same style of argument shows that for any consistent pure extension A of Q0-inf there is no wff B of type (osigma) such that A proves C=B_"C"_ for every wff C.
Truth is elusive!