*To*: coq-club at inria.fr, cl-isabelle-users at lists.cam.ac.uk, hol-info at lists.sourceforge.net*Subject*: [isabelle] Corrections of and amendments to prior publications on Goedel's First Incompleteness Theorem; Russell O'Connor's definitions for its proof in Peter B. Andrews' logic Q0; Comparison of the proofs by O'Connor and Paulson*From*: Ken Kubota <mail at kenkubota.de>*Date*: Thu, 7 Jul 2016 18:49:01 +0200*Cc*: "Prof. Lawrence C. Paulson" <lp15 at cam.ac.uk>, "Prof. Peter B. Andrews" <andrews at cmu.edu>, Russell O'Connor <roconnor at theorem.ca>

Dear Members of the Research Community, After a very fruitful debate with Russell O'Connor (who provided the proof of Goedel's First Incompleteness Theorem in Coq) I would like to correct and update some of my earlier publications. Also, with the kind permission of Russell O'Connor, his definitions for carrying out Goedel's First Incompleteness Theorem in Peter B. Andrews' logic Q0, an improved variant of Church's type theory, including a sample proof for a case of theorem V, are attached at the end of this e-mail. Andrews' logic Q0 is specified in [Andrews, 2002, pp. 210-215; Andrews, 1986, pp. 161-165]. A short description is available online at [Andrews, 2014]: http://plato.stanford.edu/archives/spr2014/entries/type-theory-church/#ForBasEqu Finally, a comparison of the proofs of Goedel's First Incompleteness Theorem by Russell O'Connor (in Coq) and Lawrence C. Paulson (in Isabelle) is undertaken in order to foster the understanding of the proof. The type system implemented by O'Connor is particularly well suited for demonstrating the three different language levels in the proof. Kind regards, Ken Kubota I. Corrections 1. The critique of a presentation of Goedel's First Incompleteness Theorem in my 2013 article [Kubota, 2013] applies to that particular presentation only, but not to the original publication of Goedel's First Incompleteness Theorem [GÃdel, 1931]. Since the work with the criticized presentation is a standard work on higher-order logic, and the author of that work is usually extremely precise and accurate, I did not expect the criticized presentation to substantially differ from Goedel's original proof. 2. The hypothesis in my 2015 article [Kubota, 2015] that there is a significant difference in the results between axiomatic (Hilbert-style) deductive systems (called "object logics" in the article) and natural deduction systems (called "meta-logics" in the article) cannot be upheld. In summary, although some presentations of Goedel's First Incompleteness Theorem fail, this doesn't seem to apply to Goedel's original proof, nor does it apply to the formalized (mechanized) proofs provided by Russell O'Connor (in Coq) and others. The result of the formal proof can be interpreted in the sense that there is a formula (having the form of a sentence) that is neither provable nor refutable, but calling this "incompleteness" depends on a specific philosophical view, the semantic approach (model theory). If one doesn't share the semantic view, Goedel's theorem, although it seems formally correct, doesn't have the philosophical relevance often associated with it. II. Summary of the Proof 1. Mathematical (formal) part a) Goedel begins with the introduction of a number of definitions supposed to represent the form of a mathematical proof using mathematical (arithmetic) means, up to the last definition "Bew" (for "beweisbare Formel", i.e., "provable formula"). b) In theorem V, Goedel shows that each relation R (with the property of being primitive recursive) is definable within the logistic system by syntactical means (i.e., provability) only, in other words, for each R, there is an r (with the free variables u_1, ..., u_n), such that R(x_1, ..., x_n) -> Bew( Sb(r, u_1, Z(x_1), ..., u_n, Z(x_n)) ) where Z is the numeral function, which returns the number in the language of the embedded language when supplying a (natural) number of the logistic system in which the proof is undertaken. The proof is of a rather technical nature and quite lengthy, and, unfortunately, in his presentation Goedel only sketched the idea. For an example, see the attached presentation by Russell O'Connor. c) Newer presentations refer to a fixed-point theorem called the diagonal lemma (or diagonalization lemma), which is rather implicit in Goedel's original proof. It can be used to construe a formula with the form of a sentence (a boolean-valued well-formed formula with no free variables) g of the embedded language, such that (simplified) ~Bew(g) and ~Bew(not g). For an excellent introduction to the diagonal lemma, see [Raatikainen, 2015], available online at http://plato.stanford.edu/archives/spr2015/entries/goedel-incompleteness/sup2.html In order to use the least amount of prerequisites, one may consider Goedel's proof of the (simplified) formula ~Bew(g) /\ ~Bew(not g) as a purely formal proof, where the definition of "Bew" is simply an abbreviation of a more complex number-theoretic well-formed formula. However, for establishing the philosophical meaning associated with Goedel's First Incompleteness Theorem, namely incompleteness, two philosophical assumptions are necessary. 2. Philosophical part I: Correctness of definitions The first philosophical assumption is the correspondence of the definitions up to "Bew" with the form of mathematical proofs. Although it is obvious that the definitions do establish a proper representation of mathematical proofs, this fact goes beyond the formal part. For example, a proof verification system (or proof assistant) may prove ~Bew(g) /\ ~Bew(not g) as a formal theorem, showing that, given the definitions, this theorem can be obtained. But the software does not verify whether the definitions actually match the form of mathematical proofs; this task is left to the reader. Goedel himself emphasizes that the definability of (primitive) recursive relations in the system P is expressed by theorem V "_without_ reference to any interpretation of the formulas of P" [GÃdel, 1931, p. 606, emphasis in the original]. Goedel speaks of yielding "an isomorphic image of the system PM in the domain of arithmetic, and all metamathematical arguments can just as well be carried out in this isomorphic image." [GÃdel, 1931, p. 597, fn. 9] The isomorphism itself, however, can only be seen from top, from the meta-perspective, i.e., from outside of the logistic system in which the proof is undertaken. A direct reference of the formal system to its own propositions is not possible. Accordingly, O'Connor distinguishes between a Goedel quote function and a Goedel numbering (or encoding) function, saying that propositions are "opaque". The Goedel numbering (or encoding) function "G isn't a function from propositions to natural numbers. It is supposed to be a function from *syntactic* formulas to natural numbers and the type of syntactic formulas is completely different from the type of propositions. Computations over syntactic formulas can inspect the intension[al] structure of the formula, but propositions are opaque and no such computation is possible." [Russell O'Connor, e-mail to Ken Kubota, February 8, 2016] The same consideration was made by the author when mentioning the "non-definability of the Goedel encoding function" previously at https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-January/msg00029.html By verifying the definitions (which is not a purely mathematical / formal task) one then can reasonably state that "Bew" can be interpreted as "provable", and that there is a formula with the form of a sentence (a proposition with no free variables) that is neither provable nor refutable. 3. Philosophical part II: The semantic approach Assuming 1. the correctness of the formal proof, and 2. the correctness of the definitions, the result obtained so far is that a well-formed formula exists, or more specifically, a formula of the form of an arithmetic proposition exists, which can neither be proven nor refuted. Following the semantic approach, according to which meaning is obtained by an interpretation in some kind of meta-theory, either "g" or "not g" must be true, hence there must be a true but unprovable theorem. This discrepancy between syntax (provability) and semantics (truth, meaning) is what is commonly called "incompleteness". The implicit assumption made here and not discussed in the original publication of Goedel's First Incompleteness Theorem in [GÃdel, 1931] is the use of the semantic approach (also called model-theoretic approach). In his completeness essay published a year earlier, Goedel already makes use of the model-theoretic approach in which semantic evaluation is performed by substitution at a meta-level, without explicitly pointing out the use of a specific philosophical assumption: "A formula of this kind is said to be valid (tautological) if a true proposition results from every substitution of specific propositions and functions for X, Y, Z, ... and F(x), G(x,y), ..., respectively [...]." [GÃdel, 1930, p. 584, fn. 3] In order to speak of "incompleteness", an expectation of "completeness" is necessary, which is generally defined as the provability of all true propositions. Hence, incompleteness is only possible if semantics (meaning) differs from syntax, as is the case with model theory (the semantic approach). But the semantic approach itself is a specific philosophical view and not inherent in mathematics. If one, like the author, does not share the semantic approach, but a purely syntactic approach, such that meaning in mathematics is obtained by syntactical inference only (and the few rules of inference have their legitimation in philosophy, outside of formal logic and mathematics), then by definition there is no distinction between syntax and semantics. In summary, if one assumes the philosophical assumption of the semantic approach, then there is mathematical (arithmetic) incompleteness. But if one doesn't, Goedel's First Incompleteness Theorem only shows that there is a formula with the form of a well-formed (arithmetic) proposition which is neither provable nor refutable, but may also be considered meaningless. Not every well-formed formula (proposition) necessarily has to have a meaning, if one doesn't follow the semantic approach. "Mathematics is liquid" is grammatically correct, but nonsense. In philosophy, it is a well-established fact that sentences may have the (outward) form of a meaningful proposition without being meaningful. Hence, without the philosophical assumption of the semantic view or a similar approach, Goedel's First Incompleteness Theorem loses its philosophical significance. III. The Proofs by Russell O'Connor (in Coq) and Lawrence C. Paulson (in Isabelle) A particularly elegant formulation of Goedel's First Incompleteness Theorem was presented by Russell O'Connor using the proof assistant Coq, as he takes advantage of "type safety by coding using an inductive type" [Russell O'Connor, e-mail to Ken Kubota, February 13, 2016], such that all three language levels use a different type. A short description is given in [O'Connor, 2006] available online at http://arxiv.org/pdf/cs/0505034v2.pdf The formal proof is available at http://www.lix.polytechnique.fr/coq/pylons/contribs/view/Goedel/trunk O'Connor uses different types for the three different levels of language: L1: type "prop" L2: type "Formula" (which may contain expressions of type "Term") L3: type "nat" The first language level (L1) is the language in which the proof is undertaken, expressed by propositions (type "prop"). The second language level (L2) is the embedded logic to be represented, expressed by syntactic formulae (type "Formula"). The third language level (L3) are the Goedel numbers obtained by encoding syntactic formulae (L2) using the Goedel numbering (or encoding) function, expressed by natural numbers (type "nat"). For example, the elimination of the implication can be expressed by "Lemma impE : forall (T : System) (f g : Formula), SysPrf T (impH g f) -> SysPrf T g -> SysPrf T f." http://www.lix.polytechnique.fr/coq/pylons/contribs/files/Goedel/trunk/Goedel.LNN.html with the predicate "SysPrf" corresponding to Goedel's "Bew", expressing the provability of a L2 formula p in a theory T by "SysPrf T p". The L1 expression is: "forall (T : System) (f g : Formula), SysPrf T (impH g f) -> SysPrf T g -> SysPrf T f". A L2 expression is: "impH g f" (which would be written as "g -> f" at the L1 level). The Goedel numbering (or encoding) function accepts an argument of L2, and returns a number of L3: "Fixpoint codeFormula (f : Formula) : nat := match f with | fol.equal t1 t2 => cPair 0 (cPair (codeTerm t1) (codeTerm t2)) | fol.impH f1 f2 => cPair 1 (cPair (codeFormula f1) (codeFormula f2)) | fol.notH f1 => cPair 2 (codeFormula f1) | fol.forallH n f1 => cPair 3 (cPair n (codeFormula f1)) | fol.atomic R ts => cPair (4+(codeR R)) (codeTerms _ ts) end." http://www.lix.polytechnique.fr/coq/pylons/contribs/files/Goedel/trunk/Goedel.code.html The numeral function accepts a number of L3 and returns the corresponding term that can be part of a L2 formula: "Fixpoint natToTerm (n : nat) : Term := match n with | O => Zero | S m => Succ (natToTerm m) end." http://www.lix.polytechnique.fr/coq/pylons/contribs/files/Goedel/trunk/Goedel.LNN.html For example, the number 3 is mapped to Succ(Succ(Succ(Zero))). The final result is: "Theorem Goedel'sIncompleteness1st : wConsistent T -> exists f : Formula, ~ SysPrf T f /\ ~ SysPrf T (notH f) /\ (forall v : nat, ~ In v (freeVarFormula LNN f))." http://www.lix.polytechnique.fr/coq/pylons/contribs/files/Goedel/trunk/Goedel.goedel1.html So if the theory is (omega-)consistent, then a proposition exists (that does not contain any free variables) which is neither provable nor refutable. Another formulation of Goedel's First Incompleteness Theorem was presented by Lawrence C. Paulson using the Isabelle proof assistant software. Descriptions are given in [Paulson, 2014] and [Paulson, 2015], linked at http://www.cl.cam.ac.uk/~lp15/papers/Formath/ and available online at http://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-logic-mine.pdf http://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-ar.pdf The formal proof is available at https://www.isa-afp.org/browser_info/current/AFP/Incompleteness/ The proof by Paulson is carried out in his proof assistant software Isabelle, which is implemented as a logical framework (a meta-logic), such that a fourth language level (the meta-logic) is involved. On the basis of this meta-logic (Isabelle/Pure), different object logics can be implemented such as set theory (Isabelle/ZF) or type theory (Isabelle/HOL). Hence, the four language levels of Paulson's proof are: L0: type "prop" of Isabelle/Pure (the logical framework / meta-logic) L1: type "bool" of Isabelle/HOL (the object logic) L2: type "fm" (for formula) of HF set theory (which may contain expressions of type "tm") L3: type "tm" (for term) of HF set theory However, since the purpose of the logical framework or meta-logic (L0) is only the implementation of several object logics such as the type theory / higher-order logic HOL (L1), the meta-logic has no significance, and for the purpose of verifying Goedel's proof and comparing its different formulations, one may abstract from (i.e., ignore) it. The proof could be carried out within a direct implementation of HOL (without a logical framework / meta-logic) also. Particularly misleading to those not familiar with the Isabelle software can be the turnstile symbol (â) as defined by Paulson in the context of Goedel's proof only: "inductive hfthm :: "fm set => fm => bool" (infixl "â" 55)" https://www.isa-afp.org/browser_info/current/AFP/Incompleteness/SyntaxN.html The turnstile is introduced as an infix operator in a L1 expression, accepting a set of L2 formulae as first (left) operand, and a L2 formula as second (right) operand, denoting the predicate hfthm (for theorem of HF set theory) defined inductively directly afterwards. Usually in literature (e.g., [Andrews, 2002]), the right operand is an expression of the main language (L1), such that the turnstile is an operator of the metamathematical level (which one would have to place at L0, although it would functionally differ from a logical framework). Paulson's Goedel numbering (or encoding) function does not return numbers, but type "tm" (for term) of L3, which are more likely to be confused with L2: "class quot = fixes quot :: "'a => tm" ("â_â") instantiation tm :: quot begin definition quot_tm :: "tm => tm" where "quot_tm t = quot_dbtm (trans_tm [] t)" instance .. end [...] instantiation fm :: quot begin definition quot_fm :: "fm => tm" where "quot_fm A = quot_dbfm (trans_fm [] A)" instance .. end" https://www.isa-afp.org/browser_info/current/AFP/Incompleteness/Coding.html Paulson: "It is essential to remember that [in Paulson's formulation of the proof] GÃdel encodings are terms (having type tm), not sets or numbers." http://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-ar.pdf (p. 16) The final result is: "text{*GÃdel's first incompleteness theorem: If consistent, our theory is incomplete.*} theorem Goedel_I: assumes "Â {} â Fls" obtains Î where "{} â Î IFF Neg (PfP âÎâ)" "Â {} â Î" "Â {} â Neg Î" "eval_fm e Î" "ground_fm Î" " https://www.isa-afp.org/browser_info/current/AFP/Incompleteness/Goedel_I.html Paulson's definition of the turnstile symbol (â) corresponds to O'Connor's predicate "SysPrf", which allows to express provability of L2 sentences within L1. Paulson's definition of the predicate "PfP" corresponds to O'Connor's predicate "codeSysPf", which allows to express provability of L3 sentences within L2. The statement "{} â Î IFF Neg (PfP âÎâ)" is an instance of the diagonal lemma using the construction "not provable" ("Neg (PfP [...])") as the lemma's property, which corresponds to that in O'Connor's definition of G: "Definition G := let (a,_) := FixPointLNN (notH codeSysPf) 0 in a." http://www.lix.polytechnique.fr/coq/pylons/contribs/files/Goedel/trunk/Goedel.goedel1.html The statements "Â {} â Î" and "Â {} â Neg Î" express that neither the proposition nor its negation are provable. The turnstile (â) denotes a predicate defined on the basis of the language of the logic in which the proof is undertaken. In contrast to O'Connor, Paulson also performs a semantic evaluation: The statement "eval_fm e Î" says that the proposition evaluates to true. The statement "ground_fm Î" ensures, like in O'Connor's proof, that the proposition does not contain any free variables. Despite Paulson's claim that "the availability of this formal proof (which can be surveyed by anybody who has a suitable computer and a copy of the Isabelle software) can help to demystify the incompleteness theorems" http://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-logic-mine.pdf (p. 1) his presentation has a number of disadvantages. In order to fully understand Paulson's proof, including the language levels and the type system involved, Paulson's articles are insufficient. Especially the description of the type system of both meta-logic and object logic is fragmented into a number of occurrences across various documentation files of the software, making it extremely tedious to obtain all the information necessary to fully understand the formalized (mechanized) proof for anyone who is not very familiar with the proof assistant software used, even with advanced knowledge in formalizing (mechanizing) proofs. Not only would one expect a short introduction into the language levels, including the type system involved, but the articles concentrate on technical implementation details rather than the basic idea of the proof. The type "tm" occurs at two different language levels (L2 and L3), resulting in a higher ambiguity. The notation would require introduction, as a predicate is written as a symbol. Intermediary results, such as an instance of the diagonal lemma, and the additional semantic evaluation make the final result less readable in comparison to O'Connor's, who focuses on the non-provability and non-refutability of the proposition like Goedel in his original proof in theorem VI [cf. GÃdel, 1931, p. 607 ff.]. Moreover, the formulation of the diagonal lemma is given as a special instance only, but not in the general form. Due to the "elimination of the pseudo-function K_i" http://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-ar.pdf (p. 23) his formulation of the diagonal lemma (and its application in Goedel's First Incompleteness Theorem) lacks the explicit use of the numeral function, yielding the following formulation: "lemma diagonal: obtains Î where "{} â Î IFF Î(i::=âÎâ)" "supp Î = supp Î - {atom i}" " https://www.isa-afp.org/browser_info/current/AFP/Incompleteness/Goedel_I.html Only the encoding function (â...â) is explicit in Paulson's formulation, whereas in O'Connor's formulation not only the Goedel encoding function (codeFormula), but also the numeral function (natToTermLNT) is present: "Lemma FixPointLNT : forall (A : Formula) (v : nat), {B : Formula | SysPrf PA (iffH B (substituteFormula LNT A v (natToTermLNT (codeFormula B)))) /\ [...]" http://www.lix.polytechnique.fr/coq/pylons/contribs/files/Goedel/trunk/Goedel.fixPoint.html Without crediting Wikipedia with scientific credibility, we shall take advantage of the symbolic notation used for the Goedel encoding function (#) and the numeral function (Â): "Then T proves [...] p <-> F(Â#(p)), which is the desired result." [The Greek character 'psi' was replaced by 'p'.] https://en.wikipedia.org/w/index.php?title=Diagonal_lemma&oldid=702789841#Proof In both cases quoted above, first the Goedel numbering or encoding function (#/codeFormula), then the numeral function (Â/natToTermLNT) is applied. IV. Possible Objections to the Formalized (Mechanized) Proofs Due to their nature, formalized (mechanized), i.e., computer verified proofs are unlikely to contain mistakes. But two conceptual issues require discussion, as they are tacitly assumed. 1. The semantic approach (model theory) Some proof assistants use methods of inference that rely on the semantic approach, specifically on the notion of satisfiability. These methods include resolution, which regularly makes use of unification and skolemization. If one does not share the semantic approach, but wants to rely on syntactical inference only, some skepticism may arise against theorems obtained by using these methods. However, since no unexpected results are known by the use of the current proof assistants, most likely an equivalent method exists by which the results can be obtained using syntactical means only. 2. The introduction of types with the Backus-Naur form (BNF) Most of the current proof assistants allow the introduction of mathematical types by use of the Backus-Naur form (BNF), which in computer science is the method of specifying an element of a formal language corresponding to inductive definitions in mathematics. For example, O'Connor defines the type of syntactic formulae "Formula" as follows: "Inductive Formula : Set := | equal : Term -> Term -> Formula | atomic : forall r : Relations L, Terms (arity L (inl _ r)) -> Formula | impH : Formula -> Formula -> Formula | notH : Formula -> Formula | forallH : nat -> Formula -> Formula." http://www.lix.polytechnique.fr/coq/pylons/contribs/files/Goedel/trunk/Goedel.fol.html In an e-mail to the author, Paulson, who designed the Isabelle proof assistant software, basically argued that newer type systems should be more expressive than Church's simple type theory which uses combinations of iota (i) and omicron (o) only. Although this is, of course, correct, the explanation is not sufficient for justifying this specific mode, namely BNF, of type introduction. The legitimacy of mathematical types depends on logical properties. For example, types must not be empty, since otherwise the logistic system is rendered inconsistent. Thus, the use of the Backus-Naur form, which historically was introduced to specify grammars, is not appropriate for replacing mathematical reasoning. Types were invented by Bertrand Russell in order to avoid the paradoxes and therefore have logical properties (e.g., being non-empty) which should be subject to proof, but not be a matter of arbitrary declaration. Nevertheless, other means may be used to express the same, such that the use of the Backus-Naur form is not essential to the proofs obtained by it. V. Some Remarks on the Semantic Approach In his article "The Semantic or Model-Theoretic View of Theories and Scientific Realism" available online at http://www3.nd.edu/~achakra1/downloads/semantic_view.pdf Anjan Chakravartty emphasizes that according to the syntactic view, a theory "is identified with a particular linguistic formulation" [Chakravartty, 2001, p. 325]. In contrast, the semantic view aims at "independence on behalf of theories from language" [Chakravartty, 2001, p. 326]. Obviously, Paulson and his Isabelle software follow the semantic approach. In his essays describing the proof [Paulson, 2014; Paulson, 2015], the semantic approach remains a tacit assumption given as granted, as the notion of incompleteness depends on it. On the basis of Isabelle's logical framework Isabelle/Pure, variants of both axiomatic set theory and type theory, i.e., a formulation of Zermelo-Fraenkel set theory (Isabelle/ZF) and a polymorphic version of Church's simple type theory (Isabelle/HOL), are implemented without opting or showing preference for one. In some sense, O'Connor is more careful, as he doesn't refer to the general notion of incompleteness, but only to "arithmetic incompleteness" or "essential incompleteness of [...] the language of arithmetic" [O'Connor, 2006, p. 15]. The problem reduces to a very specific phenomenon: "Goedel's theorem is more than the exist[ ]ance of a wff of type 'o' that is neither provable nor refutable. That goal is easy ((iota x : Nat . F) = 0) : o This wff above is neither provable nor refutable in Q0 (or both provable and refutable in the unlikely case Q0 is inconsistent.) The point of the incompleteness theorem is that there is an *arith[ ]metic* formula that is neither provable nor refutable, specifically a Pi1 arithmetic formula." [Russell O'Connor, e-mail to Ken Kubota, February 19, 2016] "The emphasis on syntactical inference exists already hidden in the Åuvre of Andrews. After stating that the semantic approach is only 'appealing' (but not definitely necessary), he then suggests to 'focus on trying to understand what there is about the syntactic structures of theorems that makes them valid.' '[S]imply checking each line of a truth table is not really very enlightening' [Andrews, 1989, pp. 257 f.]." [Kubota, 2013, p. 15] VI. Acknowledgements I would like to thank Russell O'Connor for providing the attached definitions and the sample proof as well as for granting permission for publication, for our interesting discussion, and for granting permission for the quotes used in this article to be published. References Andrews, Peter B. (1986), An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Orlando: Academic Press. Andrews, Peter B. (2002), An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Second edition. Dordrecht / Boston / London: Kluwer Academic Publishers. ISBN 1-4020-0763-9. DOI: 10.1007/978-94-015-9934-4. Andrews, Peter B. (2014), "Church's Type Theory". In: Stanford Encyclopedia of Philosophy (Spring 2014 Edition). Ed. by Edward N. Zalta. Available online at http://plato.stanford.edu/archives/spr2014/entries/type-theory-church/ (July 2, 2016). Chakravartty, Anjan (2001), "The Semantic or Model-Theoretic View of Theories and Scientific Realism". In: Synthese 127, pp. 325-345. DOI: 10.1023/A:1010359521312. Available online at http://www3.nd.edu/~achakra1/downloads/semantic_view.pdf (June 30, 2016). GÃdel, Kurt (1930), "The completeness of the axioms of the functional calculus of logic". In: Heijenoort, Jean van, ed. (1967), From Frege to GÃdel: A Source Book in Mathematical Logic, 1879-1931. Cambridge, Massachusetts: Harvard University Press, pp. 582-591. GÃdel, Kurt (1931), "On formally undecidable propositions of Principia mathematica and related systems I". In: Heijenoort, Jean van, ed. (1967), From Frege to GÃdel: A Source Book in Mathematical Logic, 1879-1931. Cambridge, Massachusetts: Harvard University Press, pp. 596-616. Kubota, Ken (2013), On Some Doubts Concerning the Formal Correctness of GÃdel's Incompleteness Theorem. Berlin: Owl of Minerva Press. ISBN 978-3-943334-04-3. DOI: 10.4444/100.101. See: http://dx.doi.org/10.4444/100.101 Kubota, Ken (2015), GÃdel Revisited. Some More Doubts Concerning the Formal Correctness of GÃdel's Incompleteness Theorem. Berlin: Owl of Minerva Press. ISBN 978-3-943334-06-7. DOI: 10.4444/100.102. See: http://dx.doi.org/10.4444/100.102 O'Connor, Russell (2006), "Essential Incompleteness of Arithmetic Verified by Coq" (2nd version). Available online at http://arxiv.org/pdf/cs/0505034v2.pdf (June 29, 2016). DOI: 10.1007/11541868_16. Paulson, Lawrence C. (2014), "A Machine-Assisted Proof of GÃdel's Incompleteness Theorems for the Theory of Hereditarily Finite Sets". In: Review of Symbolic Logic 7, pp. 484-498. DOI: 10.1017/S1755020314000112. Available online at http://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-logic-mine.pdf (June 30, 2016). Paulson, Lawrence C. (2015), "A Mechanised Proof of GÃdel's Incompleteness Theorems using Nominal Isabelle". In: Journal of Automated Reasoning 55, pp. 1-37. DOI: 10.1007/s10817-015-9322-8. Available online at http://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-ar.pdf (June 30, 2016). Raatikainen, Panu (2015), "Supplement: The Diagonalization Lemma". In: Stanford Encyclopedia of Philosophy (Spring 2015 Edition). Ed. by Edward N. Zalta. Available online at http://plato.stanford.edu/archives/spr2015/entries/goedel-incompleteness/sup2.html (June 30, 2016). ____________________ Ken Kubota doi: 10.4444/100 http://dx.doi.org/10.4444/100 ________________________________________________________________________________ SampleProofTheoremV by Russell O'Connor ________________________________________________________________________________ [In the following, all occurrences of "substitueFormula" were replaced by "substituteFormula".] [...] formal proof of a statement like (1) forall R exists r forall x PRR1(R) -> [ Rx -> [ proofB[Sb(r,u,Z(x))] ] ] but done in Q0 instead of informal mathematics. However, to get us started we can just try proving a single instance of this more general theorem in Q0. (2) exists r forall x PRR1([\x.x>1]) -> [ [\x.x>1]x -> [ proofB[Sb(r,u,Z(x))] ] ] The sad bit is that this single instance is much much easier to prove directly than the general theorem is, so my proof of the single instance probably won't be too illuminating. First, let me partially formalize statement (1) in Q0. PRR1 : (Nat -> o) -> o PRR1 := ... to be defined later ... PR1isExpressible : o PR1isExpressible forall R : Nat -> o. PRR1(R) => exists r \in FormulaSet. exists u \in Nat. forall x \in NatSet. (R x => proves RA (substituteFormula r (at u (natToTerm x)))) /\ (~R x => proves RA (not (substituteFormula r (at u (natToTerm x))))) (everything else should be defined [below]) The simpler instance is stated in Q0 as follows GT1isExpressible : o GT1isExpressible := exists r \in FormulaSet. exists u \in Nat. forall x \in NatSet. (x > 1 => proves RA (substituteFormula r (at u x))) /\ (~x > 1 => proves RA (not (substituteFormula r (at u (natToTerm x))))) /\ Unfortu[na]tely I've lopped off the PRR1 bit which is probably what inter[e]sted you, because now the proof is too easy. Take r to be (some 1 (equal (var 0) (plus (var 1) (succ (succ zero))))) Take u to be 0. Let x be any value in NatSet. We need to show that (a) (x > 1) => proves RA (substituteFormula (some 1 (equal (var 0) (plus (var 1) (succ (succ zero))))) (at 0 (natToTerm x)))) and (b) ~(x < 1) => proves RA (not (substituteFormula (some 1 (equal (var 0) (plus (var 1) (succ (succ zero))))) (at 0 (natToTerm x)))) First thing I'd like to note is that we can use the definition of substituteFormula to prove that (substituteFormula (some 1 (equal (var 0) (plus (var 1) (succ (succ zero))))) (at 0 (natToTerm x)))) = (some 0 (equal (natToTerm x) (plus (var 0) (succ (succ zero))))) I also need a lemma that says (forall x \in NatSet. freeVarTerm (natToTerm x) = empty) This reduces our goal to (a) (x > 1) => proves RA (some 0 (equal (natToTerm x) (plus (var 0) (succ (succ zero))))) and (b) ~(x < 1) => proves RA (not (some 0 (equal (natToTerm x) (plus (var 0) (succ (succ zero)))))) Let's do (b) first because it is easier. We know x \in NatSet and that ~(x < 1) holds. So x = 0 or x = 1. Suppose x = 0. Then we have to prove goal: (proves RA (not (some 0 (equal (natToTerm 0) (plus (var 0) (succ (succ zero)))))) Using a lemma that natToTerm 0 = zero we can reduce this proving goal: (proves RA (not (some 0 (equal zero (plus (var 0) (succ (succ zero)))))) expanding the definition of some we get goal: (proves RA (not (not (all 0 (not (equal zero (plus (var 0) (succ (succ zero)))))))) Using a lemma that says that forall f \in FormulaSet. (proves RA (not (not f)))=(proves RA f) we can reduce this to showing goal: (proves RA (all 0 (not (equal zero (plus (var 0) (succ (succ zero)))))))) So we can reduce or goal to goal: (proves RA (not (equal zero (plus (var 0) (succ (succ zero))))))) One of the formulas in LA is all 1 (all 2 (impl (equal (var 1) (var 2)) (impl (all 0 (not (equal zero (var 1)))) (all 0 (not (equal zero (var 2))))))) so we know that (proves RA all 1 (all 2 (impl (equal (var 1) (var 2)) (impl (all 0 (not (equal zero (var 1)))) (all 0 (not (equal zero (var 2)))))))) from the universal instantiation lemma which says forall f \in FormulaSet. forall n \in NatSet. forall t \in TermSet. proves RA (all n f) => proves RA (substituteFormula f (at n t)) we can conclude (proves RA (impl (equal (succ (plus (var 0) (succ zero)))) (plus (var 0) (succ (succ zero)) (impl (all 0 (not (equal zero (succ (plus (var 0) (succ zero))) (all 0 (not (equal zero (plus (var 0) (succ (succ zero))) One of the axioms of RA is (all 0 (all 1 (equal (plus (var 0) (succ (var 1))) (succ (plus (var 0) (var 1)))))) So by using the universal [i]nstantiation theorem we get (proves RA (equal (plus (var 0) (succ (succ zero))) (succ (plus (var 0) (succ zero)))) We have another lemma that says forall t \in TermSet. forall s \in TermSet. (proves RA (equal t s))=(proves RA (equal s t)) which lets us deduce that (proves RA (equal (succ (plus (var 0) (succ zero))) (plus (var 0) (succ (succ zero))))) So by the modus ponens closure property that defines proves, we can conclude that (proves RA (impl (all 0 (not (equal zero (succ (plus (var 0) (succ zero))) (all 0 (not (equal zero (plus (var 0) (succ (succ zero)))) Another axiom of RA is all 0 (not (equal (succ (var 0)) zero)) So that plus universal instantiation lets us show that (proves RA (not (equal (succ (plus (var 0) (succ zero))) zero))) And another lemma that says forall t \in TermSet. forall s \in TermSet. (proves RA (not (equal t s)))=(proves RA (not (equal s t))) so we can conclude that (proves RA (not (equal zero (succ (plus (var 0) (succ zero)))))) Buy the universal gen[er]alization lemma we conclude (proves RA (all 0 (not (equal zero (succ (plus (var 0) (succ zero))))))) Using the modus ponens closure property that defines proves we can conclude t[ha]t (proves RA (all 0 (not (equal zero (plus (var 0) (succ (succ zero)))) which was our goal. [...] I'll let you do the case where x = 1. Now back to part (a) goal: (x > 1) => proves RA (some 0 (equal (natToTerm x) (plus (var 0) (succ (succ zero))))) Assuming that x > 1 that means there is some y \in NatSet such that x = S (S y) So this reduces our goal to goal: proves RA (some 0 (equal (natToTerm (S (S y))) (plus (var 0) (succ (succ zero))))) We can prove that (natToTerm (S (S y))) = succ (succ (natToTerm y)), so our goal is further reduced to goal: proves RA (some 0 (equal (succ (succ (natToTerm y))) (plus (var 0) (succ (succ zero))))) [...] the rest of the p[r]oof [...] to basical[l]y goes like this: You can show (proves RA (equal (succ (succ (natToTerm y))) (plus (natToTerm y) (succ (succ zero)))) and from this you can prove taht (proves RA (some 0 (equal (succ (succ (natToTerm y))) (plus (var 0) (succ (succ zero))))) which is the desired result. At some point you have to use induction on 'y' to do these sorts of proofs, but you might be able to get away without induction here because we were lucky. ________________________________________________________________________________ ExtendedIncompletenessInQ0 by Russell O'Connor ________________________________________________________________________________ // Define Computably Enumerable (aka recursively enumerable) predicates. CESet : (Nat -> o) -> o CESet := \p. exists f \in PRF2Set. p = (\n. exists m:Nat. 0 < f n m) // Standard Model interpT : (Nat -> Nat) -> Term -> Nat interpT := \v. TermR_(Nat) v 0 (\t. S) (\t. \s. \n, \m. n + m) (\t. \s. \n. \m. n * m) interpF : (Nat -> Nat) -> Formula -> o interpF := \v. \f. FormulaR_((Nat -> Nat) -> o) (\t. \s. \v. interpT v t = interpT v s) (\v. F) (\f. \g. \r. \s. \v. r v /\ s v) (\f. \g. \r. \s. \v. r v => s v) (\f. \n. \r. \s. \v. forall m \in NatSet. r (\x. if x = n then m else v x)) isTrue : Formula -> o isTrue := \f. f \in FormulaSet /\ freeVarFormula f = empty /\ interpF (\x. x) f // Statement of essential incompleteness of arithmetic ExtendedEssentialIncompletenessOfRA : o ExtendedEssentialIncompletenessOfRA := forall t : Theory. (t c= FormulaSet /\ RA c= proves t /\ (proves t) \in CESet) => exists g \in FormulaSet. freeVarFormula g = empty /\ ((proves t g \/ proves t (not g)) => proves t = FormulaSet) /\ (~(isTrue g) => proves t = FormulaSet) ________________________________________________________________________________ PrimitiveRecursiveFunctions by Russell O'Connor ________________________________________________________________________________ // We will make use of some object of type Nat that are not in NatSet top : Nat top := \p : (i -> o). T bottom : Nat bottom := \p : (i -> o). F // Lists of natural numbers are countable, so we code them with natural numbers. // Type Definition ListNat := nat nil : ListNat nil := 0 cons : Nat -> ListNat -> ListNat cons := \x. \l. 1 + pair x l ListNatSet : ListNat -> o ListNatSet := \l. forall p : ListNat -> o. (p nil /\ forall n \in NatSet. forall k. p k => p (cons n k)) => p l ListNatR_a : a -> (Nat -> ListNat -> a -> a) -> ListNat -> a ListNatR_a := \n. \c. \r. iota x : a. forall w : ListNat -> a -> o. (w nil n /\ (forall n \n NatSet. forall l : ListNat. forall y : a. w l y => w (cons n l) (c n l y)) ) => w r x length : ListNat -> Nat length := ListNatR_(Nat) 0 (\h. \t. S) // Returns an error, repres[en]ted by bottom, when passed nil head : ListNat -> Nat head := if (nil=l) then bottom else iota h : Nat. exists t \in ListNatSet. (cons h t)=l // Returns an error, repres[en]ted by bottom, when passed nil tail : ListNat -> ListNat tail := if (nil=l) then bottom else iota t : ListNat. exists h \in NatSet. (cons h t)=l allList : (Nat -> o) -> ListNat -> o allList := \p. ListNatR_o T (\n. \l. \r. p n /\ r) lookup : ListNat -> Nat -> Nat lookup := ListNatR_(Nat -> Nat) (\n. bottom) (\h. \t. \r. \n. R (\m. \z. r m) h) // A type for primitive recursive programs (source code) // The number of primitive recursive programs is countable, so we will represent them with natural numbers. // Type Definition PrimRecProg := Nat // Type Definition ListPrimRecProg := ListNat // the program that takes no input and outputs 0 zeroP : PrimRecProg zeroP := 0 // the program that takes one input and outputs the successor of the input succP : PrimRecProg succP := 1 // the program that takes n inputs and returns the kth input. piP : Nat -> Nat -> PrimRecProg piP := \n. \k. 2 + 3*(pair n k) // the composition of m programs each taking n inputs and with program taking m inputs to make a program that takes n inputs. composeP : PrimRecProg -> ListPrimRecProg -> PrimRecProg composeP := \p. \lp. 2 + 3*(pair n lp) + 1 // the combin[a]tion of one program taking n inputs (base case), f, and // a second programming taking n + 2 inputs (recur[s]ive case), g, and // combining them by primitive recursion to make a program, h, that takes n + 1 inputs. // where h(0,x1,x2...xn) = f(x1,x2...xn) and h(S n,x1,x2...xn) = g(n,h(n,x1,x2...xn),x1,x2...xn) primRecP : PrimRecProg -> PrimRecProg -> PrimRecProg primRecP := \f. \g. 2 + 3*(pair f g) + 2 // Not all programs are well defined. The combinators have to take the programs that have the correct number of parameters and such. // Here we define the set of well formed programs accepting n inputs. primRecProgSet : Nat -> PrimRecProg -> o primRecProgSet := \n. \p. forall (w : Nat -> PrimRecProg -> o). (w 0 zeroP /\ w 1 succP /\ (forall n \in NatSet. forall k \in NatSet. k < n. w n (pi n k)) /\ (forall n \in NatSet. forall m \in NatSet. forall q : PrimRecProg. forall qs : ListPrimRecProg. (w m q /\ allList (w n) qs) => w n (composeP q qs)) /\ (forall n \in NatSet. forall f : PrimRecProg. forall g : PrimRecProg. (w n f /\ w (S (S n)) g) => w (S n) (primRecP f g)) ) => w n p //Now we give semantics to primitive recursive programs by writing an interpreter for them. //This inte[r]preter needs to produce functions that take n arguments for various n, but we cannot write this directly in Q0. //We cheat by writing functions that operate on ListNat and expect n elements in the list. //We make note of the arity of the function by returning the arity when passed the value "top" which is of type Nat, but isn't a member of NatSet. interpret : PrimRecProg -> ListNat -> Nat interpret := \p. \a. if (a = top) then (iota r : Nat. primRecProgSet r p) else (iota r : List -> Nat. forall w : PrimRecProg -> (List -> Nat) -> o. (w zeroP (\l. 0) /\ w succP (\l. S (head l)) /\ (forall n \in NatSet. forall k \in NatSet. k < n => w (piP n k) (\l. lookup l k)) /\ (forall n \in NatSet. forall m \in NatSet. forall q \in primRecProgSet m. forall iq : ListNat -> Nat. forall qs : ListPrimRecProg. forall iqs : ListNat -> ListNat. (forall i \in NatSet. i < length qs => lookup qs i \in primRecProgSet n) => (w q iq /\ (forall i \in NatSet. i < length qs => w (lookup qs i) (\l. lookup (iqs l) i))) => w (composeP q qs) (\l. iq (iqs l))) /\ (forall n \in NatSet. forall f \in primRecProgSet n. forall if : ListNat -> Nat. forall g \in primRecProgSet (S (S n)). forall ig : ListNat -> Nat. (w f if /\ w g ig) => w (primRecP f g) (\l. R (\n. \z. g (cons n (cons z (tail l)))) (f (tail l)) (head l))) ) => w p r) l // Now we can state what it means for every primitive recursive function to be repre[se]n[ ]table by an arith[ ]metic formula. PRFRepresentable : o PRFRepr[e]sentable : forall n \in NatSet. forall p \in primRecProgSet n. exists f \in FormulaSet. (forall i \in NatSet. i \in freeVarFormula f => i < (S n)) /\ (forall l \in ListNatSet. length l = n => forall y \in NatSet. (proves RA (substituteFormula f (\i. natToTerm (lookup (cons y l) i)))) <=> interpret p l=y) // We can specialize the above general theorem to the case of Primitive Recursive Functions of 2 argume[nt]s PRF2Set : (nat -> nat -> nat) -> o PRF2Set := \f. exists p \in primRecProgSet 2. forall x \in NatSet. forall y \in NatSet. interpret p (cons x (cons y nill)) = f x y. // We can state as a corollary of PRFRepr[e]sentable that every member of PRF2Set is representable by an arith[ ]metic formula. PRF2Representable : o PRF2Representable : forall f \in PRF2Set. exists f \in FormulaSet. (forall i \in NatSet. i \in freeVarFormula f => i < 3) /\ (forall x \in NatSet. forall y \in NatSet. forall z \in NatSet. (proves RA (substituteFormula f (\i. natToTerm (if i=0 then z else if i=1 then x else if i=2 then y else 0)))) <=> f x y=z) ________________________________________________________________________________ IncompletenessOfArithmeticInQ0 by Russell O'Connor ________________________________________________________________________________ // Section: Primitive // 'a' stands for any type Q_a : a -> a -> o iota : (i -> o) -> i // Section: Logic // Notation A = B := Q A B // Notation A <=> B := Q_o A B T : o T := Q_o = Q_o F : o F := \x : o. T = \x : o. x // Notation forall x : a. A := (\x : a. T) = (\x : a. A) // Notation A /\ B := (\g : o -> o -> o. g T T) = (\g : o -> o -> o. g A B) // Notation A => B := A = (A /\ B) // Notaton ~A := A = F // Notation A \/ B := ~(~A /\ ~B) // Notation exists x : a. A := ~(forall x : a. ~A) // Notation A =/= B := ~(A = B) // Recursive Notation iota x : i. A := iota (\x. A) iota x : o. A := (\x. x) = (\x. A) iota f : a -> b. A := \x : a. iota z : b. exists f : a -> b. A /\ f x = z //Notation if A then B else C := iota x. (A /\ x = B) \/ (~A /\ x = C) // Section: sets / predicates //Notation A \in B := B A //Notation A \notin B := ~(A \in B) //Notation {A} := Q A //Notation A \intersect B := \x. x \in A /\ x \in B //Notation A \union B := \x. x \in B \/ x \in B //Notation A c= B := \x. x \in A => x \in B //Notation A \ B := A \intersect (\x. x \notin B) //Notation (usually i occurs in A) { A | i <- B } := \x. exists i \in B. x = A //Notation forall x \in A. B := forall x. x \in A => B //Notation exists x \in A. B := exists x. x \in A /\ B empty_a : a -> o empty_a := \x. F BigUnion_a : ((a -> o) -> o) -> a -> o BigUnion_a := \p. \a. exists s \in p. a \in s // Section: Natural numbers. // Type defintion Nat := (i -> o) -> o 0 : Nat 0 := Q (\x. F) S : Nat -> Nat S := \n. \p. exists x. p x /\ n (\y. y =/= x /\ p y) NatSet : Nat -> o NatSet := \n. forall p : Nat -> o. (p 0 /\ forall m : Nat. p m => p (S m)) => p n R : (Nat -> Nat -> Nat) -> Nat -> Nat -> Nat R := \h. \g. \n. iota m : Nat. forall w : Nat -> Nat -> o. (w 0 g /\ forall x : Nat. forall y : Nat. w x y => w (s x) (h x y)) => w n m 1 : Nat 1 := S 0 2 : Nat 2 := S 1 3 : Nat 3 := S 2 4 : Nat 4 := S 3 //Notation A + B := R (\x. S) A B //Notation A * B := R (\x. \y. (A + y)) 0 B triangle : Nat -> Nat triangle := R (\x. \y. (S x) + y) 0 pair : Nat -> Nat -> Nat pair := \n. \m. triangle (n + m) + m //Notation A <= B := exists n \in NatSet . A + n = B //Notation mu n. A := iota n : Nat. n \in NatSet /\ n \in A /\ forall m \in A. n <= m // Section: Syntactic Logic // Type defintion Term := Nat var : Nat -> Term var := \n. 1 + 4*n zero : Term zero := 0 succ : Term -> Term succ := \t. 1 + 4*t + 1 plus : Term -> Term -> Term plus := \t. \s. 1 + 4*(pair t s) + 2 mult : Term -> Term -> Term mult := \t. \s. 1 + 4*(pair t s) + 3 TermSet : Term -> o TermSet := \t. forall p : Term -> o. ((forall n \in NatSet. p (var n)) /\ p zero /\ (forall t : Term. p t => p (succ t)) (forall t : Term. forall s : Term. (p t /\ p s) => p (plus t s)) /\ (forall t : Term. forall s : Term. (p t /\ p s) => p (mult t s)) ) => p t TermR_a : (Nat -> a) -> a -> (Term -> a -> a) -> (Term -> Term -> a -> a -> a) -> (Term -> Term -> a -> a -> a) -> Term -> a TermR_a := \v. \z. \c. \p. \m. \r. iota x : a. forall w : Term -> a -> o. ((forall n \in NatSet. w (var n) (v n)) /\ w zero z /\ (forall t : Term. forall y : a. w t y => w (succ t) (c t y)) /\ (forall t : Term. forall s : Term. forall y : a. forall z : a. (w t y /\ w s z) => w (plus t s) (p t s y z)) /\ (forall t : Term. forall s : Term. forall y : a. forall z : a. (w t y /\ w s z) => w (mult t s) (m t s y z)) ) => w r x freeVarTerm : Term -> Nat -> o freeVarTerm := TermR_(Nat -> o) (\n. {n}) empty (\t. \p. p) (\t. \s. \p. \q. p \union q) (\t. \s. \p. \q. p \union q) subTerm : Term -> (Nat -> Term) -> Term subTerm := \r. \l. TermR_(Term) l zero (\t. succ) (\t. \s. plus) (\t. \s. mult) r at :: Nat -> Term -> Nat -> Term at := \n. \t. \m. if m = n then t else (var m) // Type definition Formula := Nat equal : Term -> Term -> Formula equal := \t. \s. 1 + 4*(pair t s) falsum : Formula falsum := 0 conj : Formula -> Formula -> Formula conj := \f. \g. 1 + 4*(pair f g) + 1 impl : Formula -> Formula -> Formula impl := \f. \g. 1 + 4*(pair f g) + 2 all : Nat -> Formula -> Formula all := \n. \f. 1 + 4*(pair n f) + 3 FormulaSet : Formula -> o FormulaSet := \f. forall p : Formula -> o. ((forall t \in Term. forall s \in Term. p (equal t s)) /\ p falsum /\ (forall f : Formula. forall g : Formula. (p f /\ p g) => p (conj f g)) /\ (forall f : Formula. forall g : Formula. (p f /\ p g) => p (impl f g)) /\ (forall n \in NatSet. forall f : Formula. p f => p (all n f)) ) => p f not : Formula -> Formula not := \f. impl f falsum disj : Formula -> Formula -> Formula disj := \f. \g. not (conj (not f) (not g)) iff : Formula -> Formula -> Formula iff := \f. \g. conj (impl f g) (impl g f) some : Nat -> Formula -> Formula some := \n. \f. not (all n (not f)) FormulaR_a : (Term -> Term -> a) -> a -> (Formula -> Formula -> a -> a -> a) -> (Formula -> Formula -> a -> a -> a) -> (Formula -> Nat -> a -> a) -> Formula -> a FormulaR_a := \e. \m. \c. \i. \l. \r. iota x : a. forall w : Formula -> a -> o. ((forall t \in TermSet. forall s \in TermSet. w (equal t s)) /\ w falsum m /\ (forall f : Formula. forall g : Formula. forall y : a. forall z : a. (w f y /\ w g z) => w (conj f g) (c f g y z)) /\ (forall f : Formula. forall g : Formula. forall y : a. forall z : a. (w f y /\ w g z) => w (impl f g) (i f g y z)) /\ (forall n \in NatSet. forall f : Formula. forall y : a. w f y => w (all n f) (l f n y)) ) => w r x freeVarFormula : Formula -> Nat -> o freeVarFormula := FormulaR_(Nat -> o) (\t. \s. freeVarTerm t \union freeVarTerm s) empty (\f. \g. \p. \q. p \union q) (\f. \g. \p. \q. p \union q) (\f. \n. \p. p \ {n}) fresh : (Nat -> o) -> Nat fresh := \p. mu x. ~p x subFormula : Formula -> (Nat -> Term) -> Formula subFormula := FormulaR_((Nat -> Term) -> Formula) (\t. \s. \l. equal (subTerm t l) (subTerm s l)) (\l. falsum) (\f. \g. \r. \s. \l. conj (r l) (s l)) (\f. \g. \r. \s. \l. impl (r l) (s l)) (\f. \n. \r. \l. (\z. all z (r (\m. if m = n then var z else l m))) (fresh (BigUnion {freeVarTerm (l i) | i <- freeVarFormula f}))) // Type definition Theory := Formula -> o // Close a set of formulas under universal generalization. gen :: (Formula -> o) -> Theory gen := \q. \f. forall p : Formula -> o. (q c= p /\ (forall n \in NatSet. forall g : Formula. p g => p (all n g))) => p f // Logical Axioms for syntactic formulas LA : Theory LA := gen (\f. (exists a \in FormulaSet. exists b \in FormulaSet. f = impl a (impl b a)) \/ (exists a \in FormulaSet. exists b \in FormulaSet. exists c \in FormulaSet. f = impl (impl a (impl b c)) (impl (impl a b) (impl a c))) \/ (exists a \in FormulaSet. exists b \in FormulaSet. f = impl (conj a b) a) \/ (exists a \in FormulaSet. exists b \in FormulaSet. f = impl (conj a b) b) \/ (exists a \in FormulaSet. exists b \in FormulaSet. f = impl a (impl b (conj a b))) \/ (exists a \in FormulaSet. f = impl falsum a) \/ (exists a \in FormulaSet. exists b \in FormulaSet. f = impl (impl (impl a b) a) a) \/ (exists n \in NatSet. exists. a \in FormulaSet. exists t \in TermSet. f = impl (all n a) (subFormula a (at n t))) \/ (exists n \in NatSet. exists. a \in FormulaSet. exists b \in FormulaSet. f = impl (all n (impl a b)) (impl (all n a) (all n b))) \/ (exists n \in NatSet. exists. a \in FormulaSet. n \notin freeVarFormula a /\ f = impl a (all n a)) \/ (exists n \in NatSet. f = equal (var n) (var n)) \/ (exists n \in NatSet. exists m \in NatSet. exists z \in NatSet. exists a \in FormulaSet. f = impl (equal (var n) (var m)) (impl (subFormula a (at z (var n))) (subFormula a (at z (var m)))))) // Close a set of formulas under modus ponens proves : Theory -> Formula -> o proves := \t. \f. forall p : Formula -> o. (t c= p /\ LA c= p /\ (forall f : Formula. forall g : Formula. (p f /\ p (impl f g)) => p g)) => p f // Section Goedel // Axioms of Robinson Arithmetic RA : Theory RA := \f. f = all 0 (not (equal (succ (var 0)) zero)) \/ f = all 0 (all 1 (impl (equal (succ (var 0)) (succ (var 1))) (equal (var 0) (var 1)))) \/ f = all 0 (or (equal (var 0) zero) (some 1 (equal (var 0) (succ (var 1))))) f = all 0 (equal (plus (var 0) zero) (var 0)) \/ f = all 0 (all 1 (equal (plus (var 0) (succ (var 1))) (succ (plus (var 0) (var 1))))) \/ f = all 0 (equal (mult (var 0) zero) zero) \/ f = all 0 (all 1 (equal (mult (var 0) (succ (var 1))) (plus (mult (var 0) (var 1)) (var 0)))) natToTerm : Nat -> Term natToTerm := R (\x. succ) zero codeTerm : Term -> Nat codeTerm : TermR_(Nat) (\n. 1 + 4*n) 0 (\t. \n. 1 + 4*n + 1) (\t. \s. \n. \m. 1 + 4*(pair n m) + 2) (\t. \s. \n. \m. 1 + 4*(pair n m) + 3) codeFormula : Formula -> Nat codeFormula : FormulaR_(Nat) (\t. \s. 1 + 4*(pair (codeTerm t) (codeTerm s))) 0 (\f. \g. \n. \m. 1 + 4*(pair n m) + 1) (\f. \g. \n. \m. 1 + 4*(pair n m) + 2) (\f. \n. \m. 1 + 4*(pair n m) + 3) quotF : Formula -> Term quotF := \f. natToTerm (codeFormula f) expressableF : (Formula -> o) -> Theory -> o expressableF := \p. \t. exists n \in NatSet. exists f \in FormulaSet. {n} = freeVarFormula f /\ (forall m \in p => proves t (subFormula f (at n (quotF m)))) /\ (forall m \in Formula. m \notin p => proves t (not (subFormula f (at n (quotF m))))) // Statement of the diagona[l] lemma: https://en.wikipedia.org/wiki/Diagonal_lemma diagonal_lemma : o diagonal_lemma := forall t : Theory. (t c= FormulaSet /\ RA c= proves t) => forall n \in natSet. forall f \in FormulaSet. exists g \in FormulaSet. freeVarFormula g = freeVarFormula f \ {n} /\ (proves t (iff g (subFormula f (at n (quotF g))))) // Statement of essential incompleteness of (Robins[ ]on) arithmetic EssentialIncompletenessOfRA : o EssentialIncompletenessOfRA := forall t : Theory. (t c= FormulaSet /\ RA c= proves t /\ expressibleF t t) => exists g \in FormulaSet. freeVarFormula g = empty /\ ((proves t g \/ proves t (not g)) => proves t = FormulaSet) ________________________________________________________________________________

- Previous by Date: [isabelle] Some corrections and amendments
- Next by Date: [isabelle] Output panel sometimes does not properly update with results of "try" or "sledgehammer"
- Previous by Thread: [isabelle] Specification of the type system of Isabelle/HOL, expressiveness (was: Declaration of (co)datatypes)
- Next by Thread: [isabelle] Output panel sometimes does not properly update with results of "try" or "sledgehammer"
- Cl-isabelle-users July 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list