Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] A tautological error?

Email Gateway (Aug 22 2022 at 13:46):

From: Andreas Röhler <andreas.roehler@easy-emacs.de>
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

Email Gateway (Aug 22 2022 at 13:46):

From: Lawrence Paulson <lp15@cam.ac.uk>
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

Email Gateway (Aug 22 2022 at 13:46):

From: Mario Carneiro <di.gama@gmail.com>
Ha, I thought I was reading something from the FOM mailing list. They are
more interested in this sort of thing:
http://www.cs.nyu.edu/mailman/listinfo/fom .

Email Gateway (Aug 22 2022 at 13:46):

From: Andreas Röhler <andreas.roehler@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

Email Gateway (Aug 22 2022 at 13:46):

From: Gergely Buday <buday.gergely@uni-eszterhazy.hu>
Andreas,

there might indeed be people here who are interested in this question and
able to answer

but I recommend to ask such questions at

http://philosophy.stackexchange.com/questions/tagged/philosophy-of-mathemat
ics

or at

http://mathoverflow.net/questions/tagged/math-philosophy

• Gergely

-----Original Message-----
From: cl-isabelle-users-bounces@lists.cam.ac.uk
[mailto:cl-isabelle-users-
bounces@lists.cam.ac.uk] On Behalf Of Andreas Röhler
Sent: Monday, July 11, 2016 2:41 PM
To: cl-isabelle-users@lists.cam.ac.uk
Subject: [isabelle] A tautological error?

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
winmail.dat

Last updated: Nov 21 2024 at 12:39 UTC