*To*: Andrei Popescu <a.popescu at mdx.ac.uk>, Ramana Kumar <rk436 at cam.ac.uk>*Subject*: [isabelle] Some corrections and amendments*From*: Ken Kubota <mail at kenkubota.de>*Date*: Thu, 7 Jul 2016 18:26:50 +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>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <5F22105EAD3CAD4689EC4570AA1802B0BF0197C539@WGFP-EXMAV1.uni.mdx.ac.uk>*References*: <2D14D352-3D4D-4FDE-ABA4-0168BF6E04F3@kenkubota.de> <5F22105EAD3CAD4689EC4570AA1802B0BF0197C539@WGFP-EXMAV1.uni.mdx.ac.uk>

Dear Andrei Popescu, dear Ramana Kumar, dear Members of the Research Community, As a matter of fairness, I have to correct one of my earlier statements. Andrei Popescu correctly pointed out at https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-December/msg00059.html that neither "being based on a meta-logic" (i.e., a logical framework) nor "featuring a natural deduction system" creates a problem. There has been a misunderstanding on my part. However, I have to say that Paulson's definition of the turnstile as a symbol for the predicate "hfthm" in "inductive hfthm :: "fm set => fm => bool" (infixl "â" 55)" https://www.isa-afp.org/browser_info/current/AFP/Incompleteness/SyntaxN.html somewhere hidden in the proof files without being prominently announced in his articles is strongly misleading and inevitably creates misinterpretations. Usually (such as in [Andrews, 2002]), the turnstile is used to indicate the provability of a theorem of the logic in which the proof is undertaken, not the provability of theorems of the embedded logic. Also, for the predicate of provability of theorems of the embedded (represented, formalized) logic, a label is usually used, not a symbolic notation (e.g., Goedel uses "Bew" - for "beweisbare Formel", the German expression for "provable formula" -, and O'Connor in Coq uses "SysPrf"). Moreover, without some short introduction to the notation and the type system it is nearly impossible to analyze the proof in detail unless one has advanced experience with the Isabelle proof assistant, leaving aside that with a logical framework there are not only three, but four language levels involved, all of which one would ideally need to understand in order to verify the proof. The result of the formal proof ~Bew(g) /\ ~Bew(not g) can be interpreted in the sense that it is possible to construe a formula with the form of a sentence (i.e., a boolean-valued well-formed formula with no free variables) neither provable nor refutable. Nevertheless, the claim of "incompleteness" depends on a philosophical assumption. One who shares the semantic view (model theory) will conclude that there is a meaningful (and true) sentence that is neither provable nor refutable, and will call the discrepancy between syntax and semantics "incompleteness". But one who shares the syntactic view will conclude that it is possible to create a meaningless formula which has the form of a syntactically correct sentence (similar, in natural language, to a grammatically correct but meaningless statement like "mathematics is liquid"). Concerning the two objections of Ramana Kumar at https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-December/msg00061.html the first one was a misunderstanding clarified at https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-January/msg00029.html But the second, Ramana Kumar's claim that type "tm" can be defined like type "nat", is not correct. Andrews' logic Q0, being an improved variant of Church's original simple type theory, only allows the types iota (i) and omicron (o), and combinations of them. Andrews' type "nat" is such a combination ( nat := (o(oi)) ). On the contrary, Paulson's type "tm" is an inductively defined type, which is not possible in Q0: "nominal_datatype tm = Zero | Var name | Eats tm tm" https://www.isa-afp.org/browser_info/current/AFP/Incompleteness/SyntaxN.html In an e-mail, Paulson basically argued that there should be ways to introduce further types (instead of restricting oneself to combinations of 'i' and 'o'). This is, of course, correct, but doesn't justify the specific mode of type introduction used here, namely the Backus-Naur form (BNF). The BNF was designed to specify formal grammars in computer science, but (mathematical) types are objects that must have certain logical properties, such as being non-empty. Thus the introduction of additional mathematical types should be subject to proof, and not a matter of mere declaration via the BNF. With some more knowledge about the concept of the current proof assistants, I can answer Ramana Kumar's question at https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-July/msg00149.html concerning the motivation of my project announcement at https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-July/msg00147.html from his perspective now. Current proof assistants seem to follow the semantic approach, in which the theory is distinguished from a specific linguistic (formal) formulation, or use of model theoretic notions like satisfiability is made. For example, in Isabelle there are implementations of both axiomatic set theory (Isabelle/ZF) and type theory (Isabelle/HOL), but neither one is explicitly preferred, and the question of which is more adequate for representing mathematics is not even raised. (Although, unlike in informal mathematics, in formalized proofs type theory seems to prevail, e.g., within Isabelle the logic Isabelle/HOL, a polymorphic version of Church's simple type theory.) If one follows the syntactic approach, then there is a desire for something like the ideal formulation or the natural language of formal logic and mathematics. The main criterion is expressiveness [cf. Andrews, 2002, p. 205], or, vice versa, the reducibility of mathematics to a minimal set of primitive rules and symbols. If we leave away for a moment the restrictions of Q0 of still being a formulation of simple type theory (i.e., without type variables and dependent types), all of formal logic and mathematics can be expressed on the basis of only a "single rule of inference (substitution, from which the rule of modus ponens is derived)" and "only two basic types (individuals and truth values) and only two basic constants (identity/equality and its counterpart, description)" https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-July/msg00147.html Paulson argued that natural deduction is far superior to Hilbert-style systems for automated proof. This is, of course, correct, since Hilbert-style metatheorems become symbolically representable in natural deduction as regular theorems (and not just metatheorems), but this only reflects the engineer's perspective with the pragmatic aim of quickly obtaining proofs. For the philosopher it is not proof automation but expressiveness that is the main criterion, such that the method with the least amount of rules of inferences, i.e., a Hilbert-style system, is preferred, and all other rules become derived rules. Hence, from the perspective of the syntactic view, Andrews' elegant logic Q0 is the natural point to start with. Overcoming its restrictions by extending it to a polymorphic (with type variables) and dependent type theory (with dependent types) is the motivation of my logic R0, which I hope to be able to publish soon. A preliminary excerpt with some definitions and a sample proof is available online at http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf Kind regards, Ken Kubota ____________________ Ken Kubota doi: 10.4444/100 http://dx.doi.org/10.4444/100

**Follow-Ups**:**Re: [isabelle] Some corrections and amendments***From:*Gottfried Barrow

**[isabelle] Declaration of (co)datatypes (was: Some corrections and amendments)***From:*Corey Richardson

- Previous by Date: [isabelle] Isabelle and the text console
- Next by Date: [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
- Previous by Thread: Re: [isabelle] Isabelle and the text console
- Next by Thread: Re: [isabelle] Some corrections and amendments
- 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