These submarines are a little brittle, they quickly implode.
Especially the Joysticks are a sore point. Same for axioms that
are definitions that make use of impredicativity.

There are now serious doubts that this here holds for any island:

https://www.dcproof.com/EpimenidesParadox.htm

Take an island which has only one statement x, and
only one inhabitant epi. It could be formalized by:

ALL(a):[Stmt(a) <=> a=x]

ALL(a):[Cretan(a) <=> a=epi]

Now its well known that ALL(a):[a = t => P(a)] is logically
equivalent to P(t) if t is a singular term that denotes.

But then we can also prove this axiom here used by Dan Christensen:

3 True(x) <=> ALL(a):ALL(b):[Cretan(a) & Stmt(b) & Said(a,b) => ~True(b)]
Axiom

Equivalent to:

3 True(x) <=> ~True(x)
Axiom'

Which I guess is an impossible island.

On Thursday, August 31, 2023 at 6:40:34 PM UTC-4, Mild Shock wrote:
> These submarines are a little brittle, they quickly implode.
> Especially the Joysticks are a sore point. Same for axioms that
> are definitions that make use of impredicativity.
>
> There are now serious doubts that this here holds for any island:
>
> https://www.dcproof.com/EpimenidesParadox.htm
>
> Take an island which has only one statement x, and
> only one inhabitant epi. It could be formalized by:
>
> ALL(a):[Stmt(a) <=> a=x]
>
> ALL(a):[Cretan(a) <=> a=epi]
>
> Now its well known that ALL(a):[a = t => P(a)] is logically
> equivalent to P(t) if t is a singular term that denotes.
>
> But then we can also prove this axiom here used by Dan Christensen:
>
> 3 True(x) <=> ALL(a):ALL(b):[Cretan(a) & Stmt(b) & Said(a,b) => ~True(b)]
> Axiom
>
> Equivalent to:
>
> 3 True(x) <=> ~True(x)
> Axiom'
>
> Which I guess is an impossible island.

Wrong. At minimum, Epimenides could have been the only Cretan, but he would have to have made at least TWO statements--one true, another not true.

EXIST(a):EXIST(b):[Cretan(a) & Stmt(b) & Said(a,b) & True(b)] (line 27)

Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

TWO statements would violate:

ALL(a):[Stmt(a) <=> a=x]

Dan Christensen schrieb am Freitag, 1. September 2023 um 04:42:50 UTC+2:
> Wrong. At minimum, Epimenides could have been the
> only Cretan, but he would have to have made at least
> TWO statements--one true, another not true.