*To*: Lawrence Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] A tautological error?*From*: Andreas RÃhler <andreas.roehler at easy-emacs.de>*Date*: Tue, 12 Jul 2016 09:43:40 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <F21B3307-18BC-46AC-B3C7-2939C702A5EB@cam.ac.uk>*References*: <994a5f10-1f0a-0c67-d27a-02cf805c4722@easy-emacs.de> <F21B3307-18BC-46AC-B3C7-2939C702A5EB@cam.ac.uk>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:45.0) Gecko/20100101 Icedove/45.1.0

Hi Lawrence, just to give an example: please consider from Isabelle2016/src/Doc/Logics_ZF/document/ZF.tex Which version of axiomatic set theory? [...]

And above:

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. ;;;;

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 PaulsonOn 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

**Follow-Ups**:

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

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

- Previous by Date: [isabelle] using oops in document preparation
- Next by Date: [isabelle] using a remote server behind Isabelle/jEdit
- Previous by Thread: Re: [isabelle] A tautological error?
- Next by Thread: [isabelle] Isabelle design decisions, natural deduction vs. Hilbert-style, model theory vs. dependent type theory, and the class of all sets
- 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