On Friday, 25 August 2023 at 12:29:55 UTC+2, Julio Di Egidio wrote:
<snip>
> (** Grelling–Nelson Paradox. *)
These all have the form "I am not provable"
(in particular, as opposed to "I am not true"):
- The Grelling–Nelson Paradox
- The Barber Paradox (see below)
- The Diagonal Argument (see below)
- Goedel's Incompleteness Theorem (not yet)
In fact, I still have to try GIT, which looks more
complicated than the straight translations below,
although the form should be the same: GIT is a
"complicated" diagonal argument...
I also have to try and see what happens if we extend
the initial set with the "non-standard" element: is it
necessarily turtles all the way up, or can we close the
system?
To be continued...
================================
The Barber Paradox
================================
> (* The "set" of words. *)
> Parameter W : Type.
The "set" of men.
> (* A word is "applicable" to a word. *)
> Parameter phi : W -> W -> Prop.
A man "shaves" a man?
> (* Word [w] is "autological". *)
> Definition aut (w : W) : Prop := phi w w.
Man [w] shaves himself?
> (* Word [w] is "heterological". *)
> Definition het (w : W) : Prop := not (aut w).
Man [w] does NOT shave himself?
> (* Exists word [h] to "represent" [het]. *)
> Definition exists_h : Prop :=
> exists (h : W), forall (w : W), phi h w <-> het w.
Exists man [h] s.t. [h] shaves [w]
iff [w] does NOT shave himself?
> (* [exists_h] is "inconsistent". *)
> Theorem exists_h_to_false : exists_h -> False.
Exists such man [h] is false! QED.
================================
================================
The Diagonal Argument
================================
> (* The "set" of words. *)
> Parameter W : Type.
The "set" of natural numbers.
> (* A word is "applicable" to a word. *)
> Parameter phi : W -> W -> Prop.
A "total" list of binary strings
(in Prop instead of bool covers also
the undecidable ones...)
Equivalently, a function of (i,j) that
returns the j-th digit of the i-th string.
> (* Word [w] is "autological". *)
> Definition aut (w : W) : Prop := phi w w.
The [w]-th diagonal digit of the list is True (i.e. 1)?
> (* Word [w] is "heterological". *)
> Definition het (w : W) : Prop := not (aut w).
The [w]-th diagonal digit is NOT True (i.e. 0)?
> (* Exists word [h] to "represent" [het]. *)
> Definition exists_h : Prop :=
> exists (h : W), forall (w : W), phi h w <-> het w.
Exists natural number [h] s.t. the [w]-th digit
of the [h]-th string is True iff the [w]-th diagonal
digit is NOT True?
> (* [exists_h] is "inconsistent". *)
> Theorem exists_h_to_false : exists_h -> False.
Exists such natural number [h] is false! QED.
(Namely: the "diagonal" here is represented by the
function [aut], the "antidiagonal" is represented by
[het], and, as expected, we have proven that there
is NO natural number [h] such that the antidiagonal
is at place [h] in any list [phi].)
================================
Julio