Re: [isabelle] A tautological error?



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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.