*To*: Andreas RÃhler <andreas.roehler at easy-emacs.de>, Joachim Breitner <breitner at kit.edu>*Subject*: [isabelle] Isabelle design decisions, natural deduction vs. Hilbert-style, model theory vs. dependent type theory, and the class of all sets*From*: Ken Kubota <mail at kenkubota.de>*Date*: Wed, 13 Jul 2016 16:31:33 +0200*Cc*: "Prof. Lawrence C. Paulson" <lp15 at cam.ac.uk>, "Prof. Peter B. Andrews" <andrews at cmu.edu>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <f1e2483e-11fd-bc6b-f8d0-cefaa33c248c@easy-emacs.de>*References*: <994a5f10-1f0a-0c67-d27a-02cf805c4722@easy-emacs.de> <F21B3307-18BC-46AC-B3C7-2939C702A5EB@cam.ac.uk> <f1e2483e-11fd-bc6b-f8d0-cefaa33c248c@easy-emacs.de>

Although this mailing list is dedicated to the proof assistant, some basic issues appear relevant as they are implicit to the design of Isabelle, and for this reason should be mentioned in the documentation, too. For example, Isabelle seems to follow the semantic approach (model theory) with its independence of specific axiomatizations (particular linguistic formulations), resulting in a plurality of (object) logics, which is unsatisfactory to some, including myself, as I follow the syntactic approach and believe in the existence of an optimal formulation, of a natural mathematical language. Also, many other major decisions, such as opting for natural deduction or the non-standard use of the turnstile symbol (either in the "system infrastructure for local context management" or freely definable as in Paulson's Goedel proof), should at least be shortly explained in some form of introduction that is easy to find, as the lack of information causes misunderstanding. Of course, natural deduction is better suited for automation, but not every logician or mathematician has a long history of automated theorem proving, such that for one trying to understand the concept of the software from scratch, it is tedious to have to search older articles even from as far back as the 1980s in order to follow the major design decisions of the software, as, for example, published in 1989: "Natural deduction is far superior for automated proof." https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-175.pdf (p. 3) In the same sense, a logician or mathematician may not be familiar with the concept of a logical framework (also called "meta-logic") of computer science, which would make a short introduction to the terminology ("meta-logic", "object logics") desirable, as it easily leads to confusion with metamathematical notions, may it be Hilbert-style metatheorems or the arithmetization of proofs, or notions of the semantic approach, where the evaluation is performed at a meta-level. A short reference for the type system of both meta-logic and object logics would do away with the effort of having to scan hundreds of pages of documentation. If the focus is expressiveness instead of automation, axiomatic (Hilbert-style) deductive systems (e.g., Andrews' Q0) are the natural choice. So I definitely agree with the statements made by Andreas RÃhler and Joachim Breitner about "natural deduction" being rather artificial, and a misnomer which should be replaced by "Gentzen-style" systems. Concerning model theory, new light is shed on the field when dependent type theory becomes available. In traditional model theory, the syntax (the formal language, the theory) is expressed in a sphere separated from its semantics (the interpretation or evaluation) as well as the statement that a certain model satisfies the theory. In dependent type theory, the latter statement can be expressed within (!) the logic in which the proof is undertaken, for example, that (o, XOR) is a group consisting of the set (type) of truth values ('o'), and the operation XOR, can be expressed as the proven theorem Grp o XOR formed simply by lambda-application as wff 6955 at http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf (p. 416) where "Grp" is defined (p. 359; note the prefix notation) on the basis of the group properties of associativity, identity element, and inverse element: := Grp [Îg.[Îl.(â GrpAss (â g [Îe.(â GrpIdy GrpInv)]))]] Since in R0 every non-empty set becomes a type, no language restrictions apply, and any (non-empty) set can be the first argument of the binary predicate "Grp". The first argument has type "tau" (Ï), which is the type of types. Hence, from the perspective of dependent type theory, model theory was the only possibility of expressing a mathematical fact in a deficient way (outside of the logic, "outward"), while now, with dependent type theory, it can be expressed within the logic ("immanent"), i.e., using the means of the language in which the proof is undertaken, yielding a higher expressiveness. A stronger variant of type theory than the current Isabelle/HOL, which is just a polymorphic version of Church's simple type theory, would be desirable. The statement "The class of all sets, V, cannot be a set without admitting Russell's Paradox." http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2016/doc/logics-ZF.pdf (p. 20) is incorrect, as for Russell's Paradox not only self-reference, but also negation is required ("the set of all sets that are NOT members of themselves"). The philosophical antinomy always has both properties (self-reference and negativity) in its main form. The set of all sets (the universal class/set V) is usually referred to in the context of Cantor's paradox, saying that the power set of the set of all sets must have a larger cardinality, although, at the same time, it must be a subset of the set of all sets, and therefore have a smaller or equal cardinality. In dependent type theory, due to its subtle type system, it is easy to demonstrate that neither Russell's Paradox nor Cantor's paradox can be expressed, since both of them violate type restrictions [cf. Kubota, 2015, pp. 24 f.]. Nevertheless, it is possible (in the dependent type theory R0) to construe a universal set V without, as I believe, rendering the system inconsistent, cf. "Definition of the universal set" at http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf (p. 358) R0 also has the universal type "omega" (Ï), which replaces the primitive type for individuals "iota" ('i') used by Church and Andrews (and which is, in some sense, identical with the universal set V). Ken Kubota References Kubota, Ken (2015), On the Theory of Mathematical Forms (draft from May 18, 2015). Unpublished manuscript. SHA-512: a0dfe205eb1a2cb29efaa579d68fa2e5 45af74d8cd6c270cf4c95ed1ba6f7944 fdcffaef2e761c8215945a9dcd535a50 011d8303fd59f2c8a4e6f64125867dc4. DOI: 10.4444/100.10. See: http://dx.doi.org/10.4444/100.10 Kubota, Ken (2015a), Excerpt from [Kubota, 2015] (pp. 356-364, pp. 411-420, and pp. 754-755). Available online at http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf (January 24, 2016). SHA-512: 67a48ee12a61583bd82c286136459c0c 9fd77f5fd7bd820e8b6fe6384d977eda 4d92705dac5b3f97e7981d7b709fc783 3d1047d1831bc357eb57b263b44c885b. ____________________ Ken Kubota doi: 10.4444/100 http://dx.doi.org/10.4444/100 > Am 12.07.2016 um 09:43 schrieb Andreas RÃhler <andreas.roehler at easy-emacs.de>: > > Hi Lawrence, > > just to give an example: please consider from > > Isabelle2016/src/Doc/Logics_ZF/document/ZF.tex > > Which version of axiomatic set theory? > > [...] > > The class of all sets,~$V$,cannot be a set without admitting Russell's Paradox. > > And above: > > ZF does nothave a finite axiom system because of its Axiom Scheme of Replacement. > This makes it awkward to use with many theorem provers, since instances > of the axiom scheme have to be invoked explicitly. Since Isabelle has no > difficulty with axiom schemes, we may adopt either axiom system. > > ;;;; > > Probably you will agree saying "we may adopt either axiom system" --while true, as it's all about models-- doesn't sound satisfying. > > There will be no reliable system, if the basement isn't certain. > > With all due respect, > > Andreas > > > On 11.07.2016 15:08, Lawrence Paulson wrote: >> Iâm afraid your question is off topic for this mailing list. Please ask questions directly connected with Isabelle. There are plenty of forums where you can discuss the philosophy of mathematics. >> >> Larry Paulson >> >> >>> On 11 Jul 2016, at 13:40, Andreas RÃhler <andreas.roehler at easy-emacs.de> wrote: >>> >>> Hi all, >>> >>> the Russel's Paradox constitutes a surprise: >>> >>> Doesn't it ignore the Subject-Object-Relation of all statement?No definition might define it's own definition. As someone upheld a recursive function here: Any recursive function must be defined before calling it, the recursion is no defining-process, it comes afterwards. >>> >>> Kind of a tautological error? >>> As far as Cantor is the guilty, well, Russell should have rejected Cantors exaggeration... >>> >>> Cheers, >>> >>> Andreas >>> > >

**References**:**[isabelle] A tautological error?***From:*Andreas RÃhler

**Re: [isabelle] A tautological error?***From:*Lawrence Paulson

**Re: [isabelle] A tautological error?***From:*Andreas RÃhler

- Previous by Date: [isabelle] Clone detection for Isabelle theories
- Next by Date: [isabelle] simp only:
- Previous by Thread: Re: [isabelle] A tautological error?
- Next by Thread: [isabelle] using oops in document preparation
- 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