info
Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss
Grelling–Nelson Paradox (in Coq)
454 views
Skip to first unread message
Julio Di Egidio
Aug 25, 2023, 6:29:55 AM8/25/23
to
By popular demand, here it is in Coq, plainest and simplest,
indeed just *constructive FOPL* if I am not mistaken.
This was a nice exercise: it wasn't trivial (for me) to come
up with a formalization, so I'd encourage you to play with
the problem (in any formalism) before you look at my solution.
Spoiler.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
The gist of it is that `forall w, phi h w <-> het w`
unfolds to `forall w, phi h w <-> ~ phi w w`, which,
in turn, by specializing with `w:=h`, becomes
`phi h h <-> ~ phi h h`.
```coq
(** Grelling–Nelson Paradox. *)
(* The "set" of words. *)
Parameter W : Type.
(* A word is "applicable" to a word. *)
Parameter phi : W -> W -> Prop.
(* Word [w] is "autological". *)
Definition aut (w : W) : Prop := phi w w.
(* Word [w] is "heterological". *)
Definition het (w : W) : Prop := not (aut w).
(* Exists word [h] to "represent" [het]. *)
Definition exists_h : Prop :=
exists (h : W),
forall (w : W), phi h w <-> het w.
(* [exists_h] is "inconsistent". *)
Theorem exists_h_to_false :
exists_h -> False.
Proof.
unfold exists_h, het, aut.
intros [h H].
destruct (H h) as [PN NP].
tauto.
Qed.
```
Julio
indeed just *constructive FOPL* if I am not mistaken.
This was a nice exercise: it wasn't trivial (for me) to come
up with a formalization, so I'd encourage you to play with
the problem (in any formalism) before you look at my solution.
Spoiler.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
The gist of it is that `forall w, phi h w <-> het w`
unfolds to `forall w, phi h w <-> ~ phi w w`, which,
in turn, by specializing with `w:=h`, becomes
`phi h h <-> ~ phi h h`.
```coq
(** Grelling–Nelson Paradox. *)
(* The "set" of words. *)
Parameter W : Type.
(* A word is "applicable" to a word. *)
Parameter phi : W -> W -> Prop.
(* Word [w] is "autological". *)
Definition aut (w : W) : Prop := phi w w.
(* Word [w] is "heterological". *)
Definition het (w : W) : Prop := not (aut w).
(* Exists word [h] to "represent" [het]. *)
Definition exists_h : Prop :=
exists (h : W),
forall (w : W), phi h w <-> het w.
(* [exists_h] is "inconsistent". *)
Theorem exists_h_to_false :
exists_h -> False.
Proof.
unfold exists_h, het, aut.
intros [h H].
destruct (H h) as [PN NP].
tauto.
Qed.
```
Julio
Julio Di Egidio
Aug 25, 2023, 7:27:42 AM8/25/23
to
On Friday, 25 August 2023 at 12:29:55 UTC+2, Julio Di Egidio wrote:
> (* [exists_h] is "inconsistent". *)
> Theorem exists_h_to_false :
> exists_h -> False.
A comment:
> (* [exists_h] is "inconsistent". *)
> Theorem exists_h_to_false :
> exists_h -> False.
By Curry-Howard, `exists h -> False` is synonym with `~ (exists h)`,
i.e. we actually have a (*constructive*) proof that, under the given
assumptions [*], there can be no such `h` in `W`.
(*) As far as I can see, the assumption essentially being that we
have a total binary relation `phi` (formalized as a propositional
function) that expresses "applicable" of words in `W`, and we
needn't even require that it be decidable.
Julio
Julio Di Egidio
Aug 25, 2023, 7:56:09 AM8/25/23
to
On Friday, 25 August 2023 at 13:27:42 UTC+2, Julio Di Egidio wrote:
> a total binary relation `phi` (formalized as a
> propositional function)
...a binary relation `phi` (formalized as a
> a total binary relation `phi` (formalized as a
> propositional function)
total propositional function)...
Julio
Mild Shock
Aug 26, 2023, 6:31:11 AM8/26/23
to
The axiom here, is not constructive:
> Definition exists_h : Prop :=
> exists (h : W),
> forall (w : W), phi h w <-> het w.
What would be the witness for h? I guess it violates
some of the "hallmarks" of constructive theories,
since it stipulates without proof an existence.
In mathematical logic, the disjunction and existence properties
are the "hallmarks" of constructive theories such as Heyting
arithmetic and constructive set theories
https://en.wikipedia.org/wiki/Disjunction_and_existence_properties
On the other hand, such rules as U Spec are usually
considered intuitionistically valid and I guess are
also part and parcel of constructive logic. So steps like
this here, are on the other hand not problematic:
> The gist of it is that `forall w, phi h w <-> het w`
> unfolds to `forall w, phi h w <-> ~ phi w w`, which,
> in turn, by specializing with `w:=h`, becomes
> `phi h h <-> ~ phi h h`.
BTW: In as far that exist_h is not constructive it has the
same problem as my proof here. The definiton Axiom is
problematic, the U Spec step is not problematic:
1 ALL(v):[h(v)=1 <=> ~v(v)=1]
Axiom
2 h(h)=1 <=> ~h(h)=1
U Spec, 1
The result is totally different if you try a more constructive
"het", like derive it from subset, instead of using a blant
definition, at least in DC Proof I get, not anymore a contradiction,
rather the conclusion that "het" cannot be in the domain of "het":
402 ~h @ dom
5 Conclusion, 389
See the other thread "AmateurGate".
> Definition exists_h : Prop :=
> exists (h : W),
> forall (w : W), phi h w <-> het w.
some of the "hallmarks" of constructive theories,
since it stipulates without proof an existence.
In mathematical logic, the disjunction and existence properties
are the "hallmarks" of constructive theories such as Heyting
arithmetic and constructive set theories
https://en.wikipedia.org/wiki/Disjunction_and_existence_properties
On the other hand, such rules as U Spec are usually
considered intuitionistically valid and I guess are
also part and parcel of constructive logic. So steps like
this here, are on the other hand not problematic:
> The gist of it is that `forall w, phi h w <-> het w`
> unfolds to `forall w, phi h w <-> ~ phi w w`, which,
> in turn, by specializing with `w:=h`, becomes
> `phi h h <-> ~ phi h h`.
same problem as my proof here. The definiton Axiom is
problematic, the U Spec step is not problematic:
1 ALL(v):[h(v)=1 <=> ~v(v)=1]
Axiom
2 h(h)=1 <=> ~h(h)=1
U Spec, 1
The result is totally different if you try a more constructive
"het", like derive it from subset, instead of using a blant
definition, at least in DC Proof I get, not anymore a contradiction,
rather the conclusion that "het" cannot be in the domain of "het":
402 ~h @ dom
5 Conclusion, 389
See the other thread "AmateurGate".
Mild Shock
Aug 26, 2023, 6:41:00 AM8/26/23
to
If you read the Alonzo Church paper, and use its
decoupled version of "het", the paper also starts with
a nice explanation of what kind of non-constructivity
is involved. The paper starts with a short excursion
into "impredicativity". Basically there is some circularity
in defining "het", since the definition depends on what
is defined. Roughly speaking, a definition is impredicative
if it invokes (mentions or quantifies over) the set being
defined, or (more commonly) another set that
contains the thing being defined. I think its the second
case, i.e. only a reference to a totality that contains what
is is defined, which is then revealed through U Spec.
See also:
https://en.wikipedia.org/wiki/Impredicativity
Negative cycle impredicativity is hard to "resolve". You
can "resolve" positive cycle impredicativity, by for example
defaulting to some smallest solution or somesuch.
But negative cycle impredicativity, well I am still waiting
for the "resolution" announced by Dan Christensen. There
exist actually some "resolutions" in non-classical logics,
which avoid a contradiction. I am still waiting to see that here.
decoupled version of "het", the paper also starts with
a nice explanation of what kind of non-constructivity
is involved. The paper starts with a short excursion
into "impredicativity". Basically there is some circularity
in defining "het", since the definition depends on what
is defined. Roughly speaking, a definition is impredicative
if it invokes (mentions or quantifies over) the set being
defined, or (more commonly) another set that
contains the thing being defined. I think its the second
case, i.e. only a reference to a totality that contains what
is is defined, which is then revealed through U Spec.
See also:
https://en.wikipedia.org/wiki/Impredicativity
Negative cycle impredicativity is hard to "resolve". You
can "resolve" positive cycle impredicativity, by for example
defaulting to some smallest solution or somesuch.
But negative cycle impredicativity, well I am still waiting
for the "resolution" announced by Dan Christensen. There
exist actually some "resolutions" in non-classical logics,
which avoid a contradiction. I am still waiting to see that here.
Julio Di Egidio
Aug 26, 2023, 6:44:04 AM8/26/23
to
On Saturday, 26 August 2023 at 12:31:11 UTC+2, Mild Shock wrote:
> The axiom here, is not constructive:
> > Definition exists_h : Prop :=
> > exists (h : W),
> > forall (w : W), phi h w <-> het w.
> What would be the witness for h? I guess it violates
You keep guessing wrongly. That is not an axiom, it just
> The axiom here, is not constructive:
> > Definition exists_h : Prop :=
> > exists (h : W),
> > forall (w : W), phi h w <-> het w.
> What would be the witness for h? I guess it violates
defines a proposition: and the theorem that follows proves
that proposition identically false.
But you still have no clue what "constructive" even means:
it would be non-constructive had I used LEM or equivalent,
or had I assumed inhabitance, which I didn't.
*Spammer Alert*
Julio
Mild Shock
Aug 26, 2023, 7:03:54 AM8/26/23
to
I am not guessing. Definitions are Axioms. In Coq:
"Definitions extend the global environment
by associating names to terms."
https://coq.inria.fr/refman/language/core/definitions.html
Everything that goes into global environment is an Axiom,
even if it doesn't start with Coq keyword "Axiom". Its the
same in any other logic, this here can be also called a Definition:
1 ALL(v):[h(v)=1 <=> ~v(v)=1]
Axiom
It also associates the name "h" with the term lambda v.(~v(v)=1).
"Definitions extend the global environment
by associating names to terms."
https://coq.inria.fr/refman/language/core/definitions.html
Everything that goes into global environment is an Axiom,
even if it doesn't start with Coq keyword "Axiom". Its the
same in any other logic, this here can be also called a Definition:
1 ALL(v):[h(v)=1 <=> ~v(v)=1]
Axiom
Mild Shock
Aug 26, 2023, 7:11:46 AM8/26/23
to
Its much harder to make a "Definition & Axiom Free Proof" of
Grellings Antinomy. But this would assure that you
didn't use some Axioms, and that you have derived
the Antinomy from the logic of Coq only. You would
obtain a proof:
|- "Grellings Antinomy"
And not a proof:
"Global Context" |- "Grellings Antinomy"
Your proof has 3 definitions. Only 1 definition is problematic,
since it introduces a constant for a new existence. Can
you eliminate these definitions, and make a purely
logical proof? I hope this isn't the case, since it would
show Coq inconsistent.
BTW: But I guess you didn't wrote the proof by yourself,
since the Author who wrote the proof was careful enough
to not include the problematic Definition in his result, he proved:
> (* [exists_h] is "inconsistent". *)
> Theorem exists_h_to_false :
> exists_h -> False.
So we can indeed eliminate exists_h from the "Global Context",
and what he proved was:
> (* [exists_h] is "inconsistent". *)
> Theorem exists_h_to_false :
> (exists (h : W),
forall (w : W), phi h w <-> het w) -> False.
Grellings Antinomy. But this would assure that you
didn't use some Axioms, and that you have derived
the Antinomy from the logic of Coq only. You would
obtain a proof:
|- "Grellings Antinomy"
And not a proof:
"Global Context" |- "Grellings Antinomy"
Your proof has 3 definitions. Only 1 definition is problematic,
since it introduces a constant for a new existence. Can
you eliminate these definitions, and make a purely
logical proof? I hope this isn't the case, since it would
show Coq inconsistent.
BTW: But I guess you didn't wrote the proof by yourself,
since the Author who wrote the proof was careful enough
to not include the problematic Definition in his result, he proved:
> (* [exists_h] is "inconsistent". *)
> Theorem exists_h_to_false :
> exists_h -> False.
and what he proved was:
> (* [exists_h] is "inconsistent". *)
> Theorem exists_h_to_false :
forall (w : W), phi h w <-> het w) -> False.
Mild Shock
Aug 26, 2023, 7:25:03 AM8/26/23
to
But your proof is closer to Alonzo Churchs decoupling
version, because you cannot ask for (het het), this wouldn't
be well type. So you need to indirectly find a "word" h with:
forall (w : W), phi h w <-> het w
Alonzo Churchs was mocking his own approach, and even
any approach that would use a domain "W" with the
intention of words, and thus appealing to a
mention and use distinction. He says this is irrelevant,
the domain "W" would not need to be words. Can be also
something else, and he makes use of this feature.
See also:
"A Comparison of Russell’s Resolution of the Semantical Antinomies
with that of Tarski" Alonzo Church - 1976
The Journal of Symbolic Logic, Volume 41 Issue 4
https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/abs/0E1F24F9F14EB30A01C164B536EDC5DE
version, because you cannot ask for (het het), this wouldn't
be well type. So you need to indirectly find a "word" h with:
forall (w : W), phi h w <-> het w
any approach that would use a domain "W" with the
intention of words, and thus appealing to a
mention and use distinction. He says this is irrelevant,
the domain "W" would not need to be words. Can be also
something else, and he makes use of this feature.
See also:
"A Comparison of Russell’s Resolution of the Semantical Antinomies
with that of Tarski" Alonzo Church - 1976
The Journal of Symbolic Logic, Volume 41 Issue 4
https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/abs/0E1F24F9F14EB30A01C164B536EDC5DE
Mild Shock
Aug 27, 2023, 7:53:30 AM8/27/23
to
Hey Culio, I guess you need a little Crank Spank. Can you
explain how your proof is constructive? You use "tauto".
And what about Unicode, can you not use Greek Letters in Coq.
Also a pitty that DC Proof cannot do Unicode. I cannot use the Greek φ ?
How annoying. Anyway here is the DC Proof proof. The proof
is a little shorter, I think my gentzen/1 proof search generates
some longer detours because of the way it deals with negation,
since it doesn't directly search shortest natural deduction proof,
but rather works its way through search a Gentzen style proof,
but then manually doing the proof, gives something much shorter.
But can we get rid of the two Rem DNeg, to make it constructive?
Or at least can we get rid of the inner Rem DNeg?
15 ALL(u):~ALL(w):[~Phi(w,w) <=> Phi(u,w)]
Rem DNeg, 14
------------------------------------ begin proof ------------------------------------------
1 ALL(w):[~Phi(w,w) <=> Phi(u,w)]
Premise
2 ~Phi(u,u) <=> Phi(u,u)
U Spec, 1
3 [~Phi(u,u) => Phi(u,u)] & [Phi(u,u) => ~Phi(u,u)]
Iff-And, 2
4 ~Phi(u,u) => Phi(u,u)
Split, 3
5 Phi(u,u) => ~Phi(u,u)
Split, 3
6 ~Phi(u,u)
Premise
7 Phi(u,u)
Detach, 4, 6
8 ~Phi(u,u) & Phi(u,u)
Join, 6, 7
9 ~~Phi(u,u)
4 Conclusion, 6
10 Phi(u,u)
Rem DNeg, 9
11 ~Phi(u,u)
Detach, 5, 10
12 Phi(u,u) & ~Phi(u,u)
Join, 10, 11
13 ~EXIST(u):ALL(w):[~Phi(w,w) <=> Phi(u,w)]
4 Conclusion, 1
14 ~~ALL(u):~ALL(w):[~Phi(w,w) <=> Phi(u,w)]
Quant, 13
15 ALL(u):~ALL(w):[~Phi(w,w) <=> Phi(u,w)]
Rem DNeg, 14
------------------------------------ end proof ------------------------------------------
explain how your proof is constructive? You use "tauto".
And what about Unicode, can you not use Greek Letters in Coq.
Also a pitty that DC Proof cannot do Unicode. I cannot use the Greek φ ?
How annoying. Anyway here is the DC Proof proof. The proof
is a little shorter, I think my gentzen/1 proof search generates
some longer detours because of the way it deals with negation,
since it doesn't directly search shortest natural deduction proof,
but rather works its way through search a Gentzen style proof,
but then manually doing the proof, gives something much shorter.
But can we get rid of the two Rem DNeg, to make it constructive?
Or at least can we get rid of the inner Rem DNeg?
15 ALL(u):~ALL(w):[~Phi(w,w) <=> Phi(u,w)]
Rem DNeg, 14
------------------------------------ begin proof ------------------------------------------
1 ALL(w):[~Phi(w,w) <=> Phi(u,w)]
Premise
2 ~Phi(u,u) <=> Phi(u,u)
U Spec, 1
3 [~Phi(u,u) => Phi(u,u)] & [Phi(u,u) => ~Phi(u,u)]
Iff-And, 2
4 ~Phi(u,u) => Phi(u,u)
Split, 3
5 Phi(u,u) => ~Phi(u,u)
Split, 3
6 ~Phi(u,u)
Premise
7 Phi(u,u)
Detach, 4, 6
8 ~Phi(u,u) & Phi(u,u)
Join, 6, 7
9 ~~Phi(u,u)
4 Conclusion, 6
10 Phi(u,u)
Rem DNeg, 9
11 ~Phi(u,u)
Detach, 5, 10
12 Phi(u,u) & ~Phi(u,u)
Join, 10, 11
13 ~EXIST(u):ALL(w):[~Phi(w,w) <=> Phi(u,w)]
4 Conclusion, 1
14 ~~ALL(u):~ALL(w):[~Phi(w,w) <=> Phi(u,w)]
Quant, 13
15 ALL(u):~ALL(w):[~Phi(w,w) <=> Phi(u,w)]
Rem DNeg, 14
------------------------------------ end proof ------------------------------------------
Julio Di Egidio
Aug 27, 2023, 10:58:27 AM8/27/23
to
On 27/08/2023 13:53, Mild Shock wrote:
> explain how your proof is constructive? You use "tauto".
<< `tauto` succeeds on any instance of an *intuitionistic
> explain how your proof is constructive? You use "tauto".
tautological proposition*. >> (my emphasis, on RTFM.)
<https://coq.inria.fr/refman/proofs/automatic-tactics/logic.html?highlight=tauto#coq:tacn.tauto>
That said, here is the simplest explicit (still constructive)
proof of a `forall P, ~ (P <-> ~ P)` that I have been able
to concoct (I wouldn't be surprised if it can be simplified
further) (note: here I use an axiom instead of a theorem
assumption, but this is no substantial difference):
```coq
Module ex_falso''.
Parameter P : Prop. (* i.e. [forall P] *)
Axiom P_iff_not_P : P <-> ~ P.
Lemma ex_falso_quodlibet :
False.
Proof.
assert (H : P <-> ~ P)
by apply P_iff_not_P.
destruct H as [HPN HNP].
assert (HP : P).
{
apply HNP.
intros HP.
apply (HPN HP HP).
}
apply (HPN HP HP).
Qed.
End ex_falso''.
```
HTH,
Julio
Mild Shock
Aug 27, 2023, 11:00:04 AM8/27/23
to
Ok "tauto" is not that bad, it doesn't refer to classical tautology
but to tautology in the constructive logic of Coq. Here is
a little test that shows, that it doesn't cover classical logic:
Coq < Theorem couterexample: forall (P Q : Prop), ~ (P -> Q) -> P /\ ~ Q.
1 goal
============================
forall P Q : Prop, ~ (P -> Q) -> P /\ ~ Q
couterexample < tauto.
Toplevel input, characters 0-5:
> tauto.
> ^^^^^
Error: Tactic failure: tauto failed.
couterexample <
Ok here is a different proof of Grellings Paradox in DC
Proof which doesn't use Rem DNeg, even not once. Instead
starting with the Premise ~Phi(u,u) inside the proof, I do now
start with the Premise Phi(u,u). Also I formulate the result with
~EXIST(u) instead of ALL(u)~, assuming that the exist inference
rule from DC Proof is already constructive?
12 ~EXIST(u):ALL(w):[~Phi(w,w) <=> Phi(u,w)]
4 Conclusion, 1
----------------------------- begin proof ----------------------------------------
1 ALL(w):[~Phi(w,w) <=> Phi(u,w)]
Premise
2 ~Phi(u,u) <=> Phi(u,u)
U Spec, 1
3 [~Phi(u,u) => Phi(u,u)] & [Phi(u,u) => ~Phi(u,u)]
Iff-And, 2
4 ~Phi(u,u) => Phi(u,u)
Split, 3
5 Phi(u,u) => ~Phi(u,u)
Split, 3
9 ~Phi(u,u)
5 Conclusion, 6
10 Phi(u,u)
Detach, 4, 9
11 ~Phi(u,u) & Phi(u,u)
Join, 9, 10
12 ~EXIST(u):ALL(w):[~Phi(w,w) <=> Phi(u,w)]
4 Conclusion, 1
----------------------------- end proof ----------------------------------------
but to tautology in the constructive logic of Coq. Here is
a little test that shows, that it doesn't cover classical logic:
Coq < Theorem couterexample: forall (P Q : Prop), ~ (P -> Q) -> P /\ ~ Q.
1 goal
============================
forall P Q : Prop, ~ (P -> Q) -> P /\ ~ Q
couterexample < tauto.
Toplevel input, characters 0-5:
> tauto.
> ^^^^^
Error: Tactic failure: tauto failed.
couterexample <
Ok here is a different proof of Grellings Paradox in DC
Proof which doesn't use Rem DNeg, even not once. Instead
starting with the Premise ~Phi(u,u) inside the proof, I do now
start with the Premise Phi(u,u). Also I formulate the result with
~EXIST(u) instead of ALL(u)~, assuming that the exist inference
rule from DC Proof is already constructive?
12 ~EXIST(u):ALL(w):[~Phi(w,w) <=> Phi(u,w)]
4 Conclusion, 1
----------------------------- begin proof ----------------------------------------
1 ALL(w):[~Phi(w,w) <=> Phi(u,w)]
Premise
2 ~Phi(u,u) <=> Phi(u,u)
U Spec, 1
3 [~Phi(u,u) => Phi(u,u)] & [Phi(u,u) => ~Phi(u,u)]
Iff-And, 2
4 ~Phi(u,u) => Phi(u,u)
Split, 3
5 Phi(u,u) => ~Phi(u,u)
Split, 3
5 Conclusion, 6
10 Phi(u,u)
Detach, 4, 9
11 ~Phi(u,u) & Phi(u,u)
Join, 9, 10
12 ~EXIST(u):ALL(w):[~Phi(w,w) <=> Phi(u,w)]
4 Conclusion, 1
----------------------------- end proof ----------------------------------------
Mild Shock
Aug 27, 2023, 11:03:41 AM8/27/23
to
Sorry, I didn't expand the proof completely:
12 ~EXIST(u):ALL(w):[~Phi(w,w) <=> Phi(u,w)]
4 Conclusion, 1
---------------- begin proof, now completely expanded ----------------------------
1 ALL(w):[~Phi(w,w) <=> Phi(u,w)]
Premise
2 ~Phi(u,u) <=> Phi(u,u)
U Spec, 1
3 [~Phi(u,u) => Phi(u,u)] & [Phi(u,u) => ~Phi(u,u)]
Iff-And, 2
4 ~Phi(u,u) => Phi(u,u)
Split, 3
5 Phi(u,u) => ~Phi(u,u)
Split, 3
6 Phi(u,u)
Premise
7 ~Phi(u,u)
Detach, 5, 6
8 Phi(u,u) & ~Phi(u,u)
Join, 6, 7
9 ~Phi(u,u)
4 Conclusion, 6
10 Phi(u,u)
Detach, 4, 9
11 ~Phi(u,u) & Phi(u,u)
Join, 9, 10
12 ~EXIST(u):ALL(w):[~Phi(w,w) <=> Phi(u,w)]
4 Conclusion, 1
---------------- end proof, now completely expanded -----------------------
12 ~EXIST(u):ALL(w):[~Phi(w,w) <=> Phi(u,w)]
4 Conclusion, 1
1 ALL(w):[~Phi(w,w) <=> Phi(u,w)]
Premise
2 ~Phi(u,u) <=> Phi(u,u)
U Spec, 1
3 [~Phi(u,u) => Phi(u,u)] & [Phi(u,u) => ~Phi(u,u)]
Iff-And, 2
4 ~Phi(u,u) => Phi(u,u)
Split, 3
5 Phi(u,u) => ~Phi(u,u)
Split, 3
Premise
7 ~Phi(u,u)
Detach, 5, 6
8 Phi(u,u) & ~Phi(u,u)
Join, 6, 7
9 ~Phi(u,u)
4 Conclusion, 6
10 Phi(u,u)
Detach, 4, 9
11 ~Phi(u,u) & Phi(u,u)
Join, 9, 10
12 ~EXIST(u):ALL(w):[~Phi(w,w) <=> Phi(u,w)]
4 Conclusion, 1
Julio Di Egidio
Aug 28, 2023, 5:11:47 AM8/28/23
to
On Friday, 25 August 2023 at 12:29:55 UTC+2, Julio Di Egidio wrote:
<snip>
(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
<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.
> (* A word is "applicable" to a word. *)
> Parameter phi : W -> W -> Prop.
> (* Word [w] is "autological". *)
> Definition aut (w : W) : Prop := phi w w.
> (* Word [w] is "heterological". *)
> Definition het (w : W) : Prop := not (aut w).
> (* Exists word [h] to "represent" [het]. *)
> Definition exists_h : Prop :=
> exists (h : W), forall (w : W), phi h w <-> het w.
iff [w] does NOT shave himself?
> (* [exists_h] is "inconsistent". *)
> Theorem exists_h_to_false : exists_h -> False.
================================
================================
The Diagonal Argument
================================
> (* The "set" of words. *)
> Parameter W : Type.
> (* A word is "applicable" to a word. *)
> Parameter phi : W -> W -> Prop.
(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.
> (* Word [w] is "heterological". *)
> Definition het (w : W) : Prop := not (aut w).
> (* Exists word [h] to "represent" [het]. *)
> Definition exists_h : Prop :=
> exists (h : W), forall (w : W), phi h w <-> het w.
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.
(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
Mild Shock
Aug 28, 2023, 8:51:38 AM8/28/23
to
Very Good! Congratulations! Now I am waiting for a
further Coq formalization. To learn something about
Russells Type levels. Alonzo Church managed a
completely different result, using Russells Type levels.
Namely he had a form of Grelling Paradox, which
said exist_h is "ok" and (het h) is sometimes had
"yes" and sometimes "no". How was this possible, is
this even correct? Can you model that in Coq?
Try sci-hub.se to get this paper, just use the DOI:
Comparison of Russell's Resolution of the Semantical
Antinomies with that of Tarski - Alonzo Church
The Journal of Symbolic Logic
Vol. 41, No. 4 (Dec., 1976), pp. 747-760 (14 pages)
https://doi.org/10.2307/2272393
further Coq formalization. To learn something about
Russells Type levels. Alonzo Church managed a
completely different result, using Russells Type levels.
Namely he had a form of Grelling Paradox, which
said exist_h is "ok" and (het h) is sometimes had
"yes" and sometimes "no". How was this possible, is
this even correct? Can you model that in Coq?
Try sci-hub.se to get this paper, just use the DOI:
Comparison of Russell's Resolution of the Semantical
The Journal of Symbolic Logic
Vol. 41, No. 4 (Dec., 1976), pp. 747-760 (14 pages)
https://doi.org/10.2307/2272393
Mild Shock
Aug 28, 2023, 9:02:34 AM8/28/23
to
A way to get "exist_h" ok, is to add a type
where h comes form, and some comprehension
axiom, and formulate "exist h" slightly different.
Like here, where comprehension is done over
the type "rel":
13 EXIST(gra):[Set'(gra) & ALL(x):ALL(y):[(x,y) @ gra <=>
(x,y) @ rel & [EXIST(fun):[Function(fun,dom,cod) &
ALL(a):[a @ dom => x(a)=fun(a)] & ~[x @ dom & fun(x)=1]] <=> y=1]]]
Subset, 11
The result was not "exist_h" is identically false, but
the "rel" I used led me to a h, which had "~h e dom". But
having "exist_h" ok is rather on the line of "resolving" the
paradox, than just state it "unresolved" as "exist_h"
identically false. And Alonzo Church was showing this
resolution used in the Principia and then compared it to
some discussion by Tarski. Concerning the Principia,
Alonzo Church mentions even two resolutions, two
printed versions of resolutions, see footnote 1:
"Russell's earlier version of the ramified type hierarchy is
in [6] and in the Introduction to the first edition of (Principia)
[12]. The later version is in *12 and in (Russell's) Introduction
to the second edition (Principia) of [12]."
https://doi.org/10.2307/2272393
Julio Di Egidio
Aug 28, 2023, 1:48:09 PM8/28/23
to
On Monday, 28 August 2023 at 15:02:34 UTC+2, Mild Shock wrote:
> But having "exist_h" ok is rather on the line of "resolving"
> the paradox, than just state it "unresolved" as "exist_h"
> identically false.
The "paradox" *is* resolved, `~ exists h` as in "there can
> But having "exist_h" ok is rather on the line of "resolving"
> the paradox, than just state it "unresolved" as "exist_h"
> identically false.
be no such barber (on that island)" is a definite answer.
> And Alonzo Church was showing this
> resolution used in the Principia and then compared it to
> some discussion by Tarski. Concerning the Principia,
> Alonzo Church mentions even two resolutions, two
> printed versions of resolutions, see footnote 1:
the way up, and provably so, courtesy Burali-Forti. I was
proposing we rather try closing the system, adding one
and only one non-standard element: but I am still playing
with it...
Julio
Mild Shock
Aug 28, 2023, 2:28:44 PM8/28/23
to
Thats not what started the discussion. The paper
I was citing to start a discussion was this here,
because it shows what traditionally "resolve" means,
Comparison of Russell's Resolution of the Semantical
Antinomies with that of Tarski - Alonzo Church
The Journal of Symbolic Logic
Vol. 41, No. 4 (Dec., 1976), pp. 747-760 (14 pages)
https://doi.org/10.2307/2272393
"resolves" anything. There is nothing about non-standard
elements in Alonzo Churchs paper. Then I figured
out that the paper discusses Grellings Paradox and
its resolution. Then you hitch hicked the topic and
claimed Grellings Paradox in Coq. Now please finish
the business and show a resolution as Alonzo Church does.
Julio Di Egidio
Aug 29, 2023, 9:29:25 AM8/29/23
to
On Monday, 28 August 2023 at 11:11:47 UTC+2, Julio Di Egidio wrote:
> 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)
But I have said that upside down: it's "I am not true"
> 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)
that is self-contradictory, while "I am not provable"
is necessarily true (under the given assumptions
and semantics).
Should add Russell Paradox to that list, and check
why with Epimenides Paradox I got a somewhat
different result...
> GIT is a "complicated" diagonal argument...
Julio
Julio Di Egidio
Aug 31, 2023, 1:48:30 PM8/31/23
to
On Monday, 28 August 2023 at 19:48:09 UTC+2, Julio Di Egidio wrote:
> On Monday, 28 August 2023 at 15:02:34 UTC+2, Mild Shock wrote:
>
> > But having "exist_h" ok is rather on the line of "resolving"
> > the paradox, than just state it "unresolved" as "exist_h"
> > identically false.
>
> The "paradox" *is* resolved, `~ exists h` as in "there can
> be no such barber (on that island)" is a definite answer.
But I must concede this "resolution" falls somewhat short: while
> On Monday, 28 August 2023 at 15:02:34 UTC+2, Mild Shock wrote:
>
> > But having "exist_h" ok is rather on the line of "resolving"
> > the paradox, than just state it "unresolved" as "exist_h"
> > identically false.
>
> The "paradox" *is* resolved, `~ exists h` as in "there can
> be no such barber (on that island)" is a definite answer.
it is reasonable that << there is no such barber on that island >>,
it does sound unsatisfactory if not ridiculous that << in the realm
of denotation, no word denotes... "heterological" >>...
Julio
Julio Di Egidio
Aug 31, 2023, 1:50:57 PM8/31/23
to
I am still unclear about the Liar proper, namely as
opposed to Grelling's and co.: SEP insists (*) that
<< The first ingredient in building a Liar is a truth
predicate >>, while our `phi` can be anything... but,
in fact, I (still?) cannot find a way to apply our (truly
basic) scheme to "I am not true": what `W` and
`phi` be in this case?
OTOH "I am not true" indeed is not as simple (basic)
as "I do not tell the truth": so maybe Russell does go
with Epimenides...
(*) <https://plato.stanford.edu/entries/liar-paradox/#TrutPred>
Julio
Julio Di Egidio
Aug 31, 2023, 1:56:04 PM8/31/23
to
On Thursday, 31 August 2023 at 19:50:57 UTC+2, Julio Di Egidio wrote:
> OTOH "I am not true" indeed is not as simple (basic)
> as "I do not tell the truth"
Sorry, of course I meant the other way around...
> OTOH "I am not true" indeed is not as simple (basic)
> as "I do not tell the truth"
Julio
Julio Di Egidio
Aug 31, 2023, 2:05:42 PM8/31/23
to
On Thursday, 31 August 2023 at 19:50:57 UTC+2, Julio Di Egidio wrote:
[Corrected:]
> OTOH "I do not tell the truth" indeed is not as simple (basic)
> as "I am not true": so maybe Russell does go with Epimenides...
Here is (my) Epimenides' for comparison:
<https://groups.google.com/g/sci.logic/c/27ig6u97dgM/m/swXAFyDkAQAJ>
with the caution that it is not finished, i.e. it's neither polished
nor, more importantly, I have tried all conclusions I could draw.
Julio
[Corrected:]
> OTOH "I do not tell the truth" indeed is not as simple (basic)
> as "I am not true": so maybe Russell does go with Epimenides...
Here is (my) Epimenides' for comparison:
<https://groups.google.com/g/sci.logic/c/27ig6u97dgM/m/swXAFyDkAQAJ>
with the caution that it is not finished, i.e. it's neither polished
nor, more importantly, I have tried all conclusions I could draw.
Julio
Mild Shock
Aug 31, 2023, 5:55:47 PM8/31/23
to
The Epimenides Paradox is not an Antinomy like the Liar Paradox.
If we take the Liar Paradox to be Q <=> ~Q, we see that this here
is also a Liar Paradox, when we replace Q by ALL(x):P(x):
ALL(x):P(x) <=> ~ALL(x):P(x)
Wolfgang Scharz tree tool indeed confirms that it is an Antinomy,
in that it can be Refuted, i.e. Disproved by producing a proof
of its negation. The proof tells me the truth table has "F" everywhere:
¬(∀xPx ↔ ¬∀xPx) is valid.
https://www.umsu.de/trees/#~3(~6xPx~4~3~6xPx)
Now how do we get the Epimenides Paradox? You only need to
tweak the above formula a little bit, and you get not anymore
an Antinomy. Negation is not provable so the truth table has somewhere "T":
¬(∀xPx ↔ ¬∃xPx) is invalid.
https://www.umsu.de/trees/#~3(~6xPx~4~3~7xPx)
But the above formula has another advantage, you can use
it to prove the contrary of what it has inside:
(∀xPx ↔ ¬∃xPx) → ∃xPx is valid.
https://www.umsu.de/trees/#(~6xPx~4~3~7xPx)~5~7xPx
This is similar to the True(x) that appears inside the Epimenides
proof in DC Proof, that then leads to ~True(x). Actually I think
the Epimenides proof can be reduced to the above, I found
it my some manipulations of the Epimendides proof.
If we take the Liar Paradox to be Q <=> ~Q, we see that this here
is also a Liar Paradox, when we replace Q by ALL(x):P(x):
ALL(x):P(x) <=> ~ALL(x):P(x)
Wolfgang Scharz tree tool indeed confirms that it is an Antinomy,
in that it can be Refuted, i.e. Disproved by producing a proof
of its negation. The proof tells me the truth table has "F" everywhere:
¬(∀xPx ↔ ¬∀xPx) is valid.
https://www.umsu.de/trees/#~3(~6xPx~4~3~6xPx)
Now how do we get the Epimenides Paradox? You only need to
tweak the above formula a little bit, and you get not anymore
an Antinomy. Negation is not provable so the truth table has somewhere "T":
¬(∀xPx ↔ ¬∃xPx) is invalid.
https://www.umsu.de/trees/#~3(~6xPx~4~3~7xPx)
But the above formula has another advantage, you can use
it to prove the contrary of what it has inside:
(∀xPx ↔ ¬∃xPx) → ∃xPx is valid.
https://www.umsu.de/trees/#(~6xPx~4~3~7xPx)~5~7xPx
This is similar to the True(x) that appears inside the Epimenides
proof in DC Proof, that then leads to ~True(x). Actually I think
the Epimenides proof can be reduced to the above, I found
it my some manipulations of the Epimendides proof.
Mild Shock
Aug 31, 2023, 6:03:54 PM8/31/23
to
Nope, I made an error, I have to retract my claim.
I think I nevertheless found the Liar Paradox inside
the Epimenides Paradox. I think Dan Christensen used
something like:
(Pb ↔ ∀x¬Px) → ¬Pb is valid.
https://www.umsu.de/trees/#(Pb~4~6x~3Px)~5~3Pb
We can also write it like this, there is now a collection of b's
that satisfies Pb, and this collection is non-empty, this is what ∃xPx says.
(∃xPx ↔ ∀x¬Px) → ¬∃xPx is valid.
https://www.umsu.de/trees/#(~7xPx~4~6x~3Px)~5~3~7xPx
But the above is a vacous truth, since ∃xPx ↔ ∀x¬Px is
logically equivalent to ∃xPx ↔ ¬∃xPx which is an
antinomy, namely we have:
¬(∃xPx ↔ ¬∃xPx) is valid.
https://www.umsu.de/trees/#~3(~7xPx~4~3~7xPx)
I think I nevertheless found the Liar Paradox inside
the Epimenides Paradox. I think Dan Christensen used
something like:
(Pb ↔ ∀x¬Px) → ¬Pb is valid.
https://www.umsu.de/trees/#(Pb~4~6x~3Px)~5~3Pb
We can also write it like this, there is now a collection of b's
that satisfies Pb, and this collection is non-empty, this is what ∃xPx says.
(∃xPx ↔ ∀x¬Px) → ¬∃xPx is valid.
https://www.umsu.de/trees/#(~7xPx~4~6x~3Px)~5~3~7xPx
But the above is a vacous truth, since ∃xPx ↔ ∀x¬Px is
logically equivalent to ∃xPx ↔ ¬∃xPx which is an
antinomy, namely we have:
¬(∃xPx ↔ ¬∃xPx) is valid.
Mild Shock
Aug 31, 2023, 6:22:39 PM8/31/23
to
The main problem is again impredicativity. See Alonzo
Churchs paper, it contains a nice explanation of
impredicativity. Namely this definition is impredicative:
True(x) <=> ALL(a):ALL(b):[Cretan(a) & Stmt(b) & Said(a,b) => ~True(b)]
https://www.dcproof.com/EpimenidesParadox.htm
True depends on True. Its even an impredicative definition
with a negative cycle. i.e. a positive True depends on a negative
True. This kind of impredicativity is notorious for producing
an Antinomy. Dan Christensen didn't show that the
impredicative definition is consistent. If it is not consistent,
then the conclusion is moot, since an inconsistent theory
can prove anything.
Steven Lahkmi
Sep 4, 2023, 3:44:45 PM9/4/23
to
Guys, of course, I almost forget about you. Do you have some non-solved mathematical problems/challenges that you want to propose here ?
(on dogelog, Coq, DcProof or related topics)
Best Regards
(on dogelog, Coq, DcProof or related topics)
Best Regards
Julio Di Egidio
Sep 4, 2023, 4:47:20 PM9/4/23
to
On 01/09/2023 00:22, Mild Shock wrote:
> The main problem is again impredicativity.
There is nothing impredicative about the formalization in question.
> The main problem is again impredicativity.
Sure, `het` is defined in terms of `phi`, but the statement of the
theorem is about logical equivalence, as per the usual notion of
"representability": it isn't saying that `het` is (is not) *equal*
to `phi h` for some (no) `h`.
Indeed, I am thinking that's rather the culprit, that when (at the
meta-level) we say "phi is incomplete", we can say it insofar as
we are assuming (at the same level) *functional extensionality*
(aka a Leibniz/extensional notion of equality).
(E.g. the list of binary strings is "incomplete" only insofar as
two strings are "the same" iff they have *the same digits*.)
Julio
Julio Di Egidio
Sep 4, 2023, 5:03:06 PM9/4/23
to
```coq
Definition leibniz_eq {U : Type} (x y : U) : Prop :=
forall (V : Type) (p : U -> V), p x = p y.
Theorem leibniz_eq_equiv_eq {U : Type} (x y : U) :
leibniz_eq x y <-> x = y.
Proof. (* relatively easy: left as an exercise *) Admitted.
Definition leibniz_eq_prop {U : Type} (x y : U) : Prop :=
forall (p : U -> Prop), p x <-> p y.
Theorem leibniz_eq_prop_equiv_eq {U : Type} (x y : U) :
leibniz_eq_prop x y <-> x = y.
Proof. (* relatively easy: left as an exercise *) Admitted.
Lemma leibniz_eq_prop_equiv_leibniz_eq {U : Type} (x y : U) :
leibniz_eq_prop x y <-> leibniz_eq x y.
Proof. (* relatively easy: left as an exercise *) Admitted.
```
I find quite puzzling that `leibniz_eq` and `leibniz_eq_prop`
come up equivalent, despite the latter is (almost) only a
special case of the former...
Julio
Mild Shock
Sep 4, 2023, 7:04:45 PM9/4/23
to
Thats not originally my idea that the Grelling Paradox is
impredicative. You might not hear the notion so much
nowadays, it has become a little bit out of fashion.
But you could read Alonzo Churchs paper, and
see how he explains impredicativity and applies
the notion to the Grelling paradox. Its not rocket science.
Alonzo Churchs uses another equality!
You use this equality, in your leibniz_eq, which is not
extensionality, using higher order object to decide
equality of lower order object:
/* identity via indiscernibility */
∀p (p x = p y).
Alonzo Church uses this equality, namely extensionality,
he is coupling via. Using lower order object to
decide equality of higher order object:
/* identity via extensionality */
∀p (x p = y p).
Just read the paper!
See also the original Thread AmateurGate, extensionality
was used and not indiscernibility:
Mild Shock schrieb am Dienstag, 22. August 2023 um 17:13:12 UTC+2:
> 1 ALL(f):ALL(g):[ALL(x):f(x)=g(x) <=> f=g]
> Axiom
https://groups.google.com/g/sci.logic/c/TaIENB54MNQ/m/IiCNfP3ZFQAJ
impredicative. You might not hear the notion so much
nowadays, it has become a little bit out of fashion.
But you could read Alonzo Churchs paper, and
see how he explains impredicativity and applies
the notion to the Grelling paradox. Its not rocket science.
Alonzo Churchs uses another equality!
You use this equality, in your leibniz_eq, which is not
extensionality, using higher order object to decide
equality of lower order object:
/* identity via indiscernibility */
∀p (p x = p y).
Alonzo Church uses this equality, namely extensionality,
he is coupling via. Using lower order object to
decide equality of higher order object:
/* identity via extensionality */
∀p (x p = y p).
Just read the paper!
See also the original Thread AmateurGate, extensionality
was used and not indiscernibility:
Mild Shock schrieb am Dienstag, 22. August 2023 um 17:13:12 UTC+2:
> 1 ALL(f):ALL(g):[ALL(x):f(x)=g(x) <=> f=g]
> Axiom
https://groups.google.com/g/sci.logic/c/TaIENB54MNQ/m/IiCNfP3ZFQAJ
Mild Shock
Sep 4, 2023, 7:10:08 PM9/4/23
to
Disclaimer: I do not claim the Grelling Paradox and what
Alonzo Church wrote cannot be done by using indiscernibility as well.
Actually I don't know. I only wanted to point out that you
are now walking by yourself on uncharted grounds.
Neither Alonzo Church paper used indiscernibility in its
core, maybe it appears elsewhere in the paper, not sure,
nor did my proof use it. The coupling was based on,
in the second axiom, which houses the coupling of v and
f in the form of a little use of extensionality, if I am not
mistaken, thats the same what you find in Alonzo Church:
Mild Shock schrieb am Dienstag, 22. August 2023 um 17:13:12 UTC+2:
> Axiom
https://groups.google.com/g/sci.logic/c/TaIENB54MNQ/m/IiCNfP3ZFQAJ
Julio Di Egidio
Sep 4, 2023, 7:14:20 PM9/4/23
to
On Tuesday, 5 September 2023 at 01:04:45 UTC+2, Mild Shock wrote:
> Thats not originally my idea that the Grelling Paradox is
> impredicative. [...] Alonzo Churchs uses another equality!
> Thats not originally my idea that the Grelling Paradox is
Indeed, as I have tried to say, it all seems to boil down to
what "equality"/"equalities".
> You use this equality, in your leibniz_eq, which is not
> extensionality, using higher order object to decide
> equality of lower order object:
> /* identity via indiscernibility */
> ∀p (p x = p y).
<< In logic, extensionality, or extensional equality, refers
to principles that judge objects to be equal if they have
the same external properties. >>
<https://en.wikipedia.org/wiki/Extensionality>
Just stop posting links that you do not understand
to begin with.
Julio
Mild Shock
Sep 4, 2023, 7:23:08 PM9/4/23
to
Well its up to you that what Alonzo Church did can be
also done with indiscernibility. If you manage to turn
extensional into indiscernibility and vice versa,
well then this is possibly a way forward. But for example
in DC Proof you cannot prove Dana Scotts trick, because
it has missing Peano unit. You cannot prove in DC Proof:
/* Existence of Singleton */
ALL(x):EXIST(y):ALL(z):[z e y <=> z = x]
This can help to show one direction, for example that
indiscernibility implies extensionality:
/* indiscernibility */
ALL(y):[a e y <=> b e y] =>
/* extensionality */
ALL(y):[y e a <=> y e b]
Proof: Sketch, if we have Singleton we can use:
y = {a} in ALL(y):[a e y <=> b e y] and therefore:
a e {a} <=> b e {a}
And therefore:
a=a <=> b=a
And therefore
b=a
And therefore, trivially:
ALL(y):[y e a <=> y e b]
Q.E.D.
But Singletons are Missing in DC Proof. So what then?
also done with indiscernibility. If you manage to turn
extensional into indiscernibility and vice versa,
well then this is possibly a way forward. But for example
in DC Proof you cannot prove Dana Scotts trick, because
it has missing Peano unit. You cannot prove in DC Proof:
/* Existence of Singleton */
ALL(x):EXIST(y):ALL(z):[z e y <=> z = x]
This can help to show one direction, for example that
indiscernibility implies extensionality:
/* indiscernibility */
ALL(y):[a e y <=> b e y] =>
/* extensionality */
ALL(y):[y e a <=> y e b]
Proof: Sketch, if we have Singleton we can use:
y = {a} in ALL(y):[a e y <=> b e y] and therefore:
a e {a} <=> b e {a}
And therefore:
a=a <=> b=a
And therefore
b=a
And therefore, trivially:
ALL(y):[y e a <=> y e b]
Q.E.D.
But Singletons are Missing in DC Proof. So what then?
Julio Di Egidio
Sep 4, 2023, 7:25:56 PM9/4/23
to
On Tuesday, 5 September 2023 at 01:23:08 UTC+2, Mild Shock wrote:
> Well its up to you that what Alonzo Church did can be
> also done with indiscernibility.
Stop posting bullshit.
> Well its up to you that what Alonzo Church did can be
> also done with indiscernibility.
*Plonk*
Julio
Mild Shock
Sep 4, 2023, 7:40:37 PM9/4/23
to
Here is a proof in DC Proof, that indiscernibility implies
extensionality, when Singletons are around. In set theory
the argument order is different, in predicate logic its P(x),
in set theory its x e P, so watch out to not confuse the two:
/* Singletons Axiom */
1 ALL(x):EXIST(y):ALL(z):[z @ y <=> z=x]
Axiom
/* Theorem Indiscernibility implies Extensionality */
36 ALL(a):ALL(b):[ALL(y):[a @ y <=> b @ y] => ALL(y):[y @ a <=> y @ b]]
4 Conclusion, 2
-------------------------- begin proof ------------------------------------
1 ALL(x):EXIST(y):ALL(z):[z @ y <=> z=x]
Axiom
2 ALL(y):[a @ y <=> b @ y]
Premise
3 EXIST(y):ALL(z):[z @ y <=> z=a]
U Spec, 1
4 ALL(z):[z @ u <=> z=a]
E Spec, 3
5 a @ u <=> b @ u
U Spec, 2
6 a @ u <=> a=a
U Spec, 4
7 [a @ u => b @ u] & [b @ u => a @ u]
Iff-And, 5
8 [a @ u => a=a] & [a=a => a @ u]
Iff-And, 6
9 a @ u => a=a
Split, 8
10 a=a => a @ u
Split, 8
11 a=a
Reflex
12 a @ u
Detach, 10, 11
13 a @ u => b @ u
Split, 7
14 b @ u => a @ u
Split, 7
15 b @ u
Detach, 13, 12
16 b @ u <=> b=a
U Spec, 4
17 [b @ u => b=a] & [b=a => b @ u]
Iff-And, 16
18 b @ u => b=a
Split, 17
19 b=a => b @ u
Split, 17
20 b=a
Detach, 18, 15
21 ~ALL(y):[y @ a <=> y @ a]
Premise
22 ~~EXIST(y):~[y @ a <=> y @ a]
Quant, 21
23 EXIST(y):~[y @ a <=> y @ a]
Rem DNeg, 22
24 ~[v @ a <=> v @ a]
E Spec, 23
25 v @ a | ~v @ a
Or Not
26 ~v @ a => ~v @ a
Imply-Or, 25
27 ~~v @ a => ~~v @ a
Contra, 26
28 v @ a => ~~v @ a
Rem DNeg, 27
29 v @ a => v @ a
Rem DNeg, 28
30 [v @ a => v @ a] & [v @ a => v @ a]
Join, 29, 29
31 v @ a <=> v @ a
Iff-And, 30
32 [v @ a <=> v @ a] & ~[v @ a <=> v @ a]
Join, 31, 24
33 ~~ALL(y):[y @ a <=> y @ a]
4 Conclusion, 21
34 ALL(y):[y @ a <=> y @ a]
Rem DNeg, 33
35 ALL(y):[y @ a <=> y @ b]
Substitute, 20, 34
36 ALL(a):ALL(b):[ALL(y):[a @ y <=> b @ y] => ALL(y):[y @ a <=> y @ b]]
4 Conclusion, 2
-------------------------- end proof ------------------------------------
extensionality, when Singletons are around. In set theory
the argument order is different, in predicate logic its P(x),
in set theory its x e P, so watch out to not confuse the two:
/* Singletons Axiom */
1 ALL(x):EXIST(y):ALL(z):[z @ y <=> z=x]
Axiom
/* Theorem Indiscernibility implies Extensionality */
36 ALL(a):ALL(b):[ALL(y):[a @ y <=> b @ y] => ALL(y):[y @ a <=> y @ b]]
4 Conclusion, 2
-------------------------- begin proof ------------------------------------
1 ALL(x):EXIST(y):ALL(z):[z @ y <=> z=x]
Axiom
2 ALL(y):[a @ y <=> b @ y]
Premise
3 EXIST(y):ALL(z):[z @ y <=> z=a]
U Spec, 1
4 ALL(z):[z @ u <=> z=a]
E Spec, 3
5 a @ u <=> b @ u
U Spec, 2
6 a @ u <=> a=a
U Spec, 4
7 [a @ u => b @ u] & [b @ u => a @ u]
Iff-And, 5
8 [a @ u => a=a] & [a=a => a @ u]
Iff-And, 6
9 a @ u => a=a
Split, 8
10 a=a => a @ u
Split, 8
11 a=a
Reflex
12 a @ u
Detach, 10, 11
13 a @ u => b @ u
Split, 7
14 b @ u => a @ u
Split, 7
15 b @ u
Detach, 13, 12
16 b @ u <=> b=a
U Spec, 4
17 [b @ u => b=a] & [b=a => b @ u]
Iff-And, 16
18 b @ u => b=a
Split, 17
19 b=a => b @ u
Split, 17
20 b=a
Detach, 18, 15
21 ~ALL(y):[y @ a <=> y @ a]
Premise
22 ~~EXIST(y):~[y @ a <=> y @ a]
Quant, 21
23 EXIST(y):~[y @ a <=> y @ a]
Rem DNeg, 22
24 ~[v @ a <=> v @ a]
E Spec, 23
25 v @ a | ~v @ a
Or Not
26 ~v @ a => ~v @ a
Imply-Or, 25
27 ~~v @ a => ~~v @ a
Contra, 26
28 v @ a => ~~v @ a
Rem DNeg, 27
29 v @ a => v @ a
Rem DNeg, 28
30 [v @ a => v @ a] & [v @ a => v @ a]
Join, 29, 29
31 v @ a <=> v @ a
Iff-And, 30
32 [v @ a <=> v @ a] & ~[v @ a <=> v @ a]
Join, 31, 24
33 ~~ALL(y):[y @ a <=> y @ a]
4 Conclusion, 21
34 ALL(y):[y @ a <=> y @ a]
Rem DNeg, 33
35 ALL(y):[y @ a <=> y @ b]
Substitute, 20, 34
36 ALL(a):ALL(b):[ALL(y):[a @ y <=> b @ y] => ALL(y):[y @ a <=> y @ b]]
4 Conclusion, 2
-------------------------- end proof ------------------------------------
Mild Shock
Sep 4, 2023, 7:43:11 PM9/4/23
to
Maybe you can do the same proof in Coq? That
`leibniz_eq` and `leibniz_eq_prop` are the same you
find all over the place on the internet. Even my
grandmother knows how to do that. But a relationship
between indiscernibility and extensionality, can
you do that in Coq?
`leibniz_eq` and `leibniz_eq_prop` are the same you
find all over the place on the internet. Even my
grandmother knows how to do that. But a relationship
between indiscernibility and extensionality, can
you do that in Coq?
Mild Shock
Sep 4, 2023, 8:02:28 PM9/4/23
to
What about the other direction from extensionality
to indiscernibility? In set theory, this is rather trivial,
especially in FOL with equality and if you can use:
Axiom of extensionality
https://en.wikipedia.org/wiki/Axiom_of_extensionality
The Proof Sketch is very short:
By the extensionallity of set theory,
the assumption ALL(y):[y e a <=> y e b] already implies:
a=b
And therefore, trivially:
to indiscernibility? In set theory, this is rather trivial,
especially in FOL with equality and if you can use:
Axiom of extensionality
https://en.wikipedia.org/wiki/Axiom_of_extensionality
The Proof Sketch is very short:
By the extensionallity of set theory,
the assumption ALL(y):[y e a <=> y e b] already implies:
a=b
And therefore, trivially:
ALL(y):[a e y <=> b e y]
Q.E.D.
Mild Shock
Sep 4, 2023, 8:08:41 PM9/4/23
to
DC Proof is a little picky, it wants also Set(_) declarations.
Just imagine for ZFC, we don't need them. Here is a proof:
/* Theorem Extensionality implies Indiscernibility */
28 ALL(y):[y @ a <=> y @ b] => ALL(y):[a @ y <=> b @ y]
4 Conclusion, 8
------------------------------- begin proof ----------------------------------
1 Set(a)
Axiom
2 Set(b)
Axiom
3 ALL(a):ALL(b):[Set(a) & Set(b) => [a=b <=> ALL(c):[c @ a <=> c @ b]]]
Set Equality
4 ALL(b):[Set(a) & Set(b) => [a=b <=> ALL(c):[c @ a <=> c @ b]]]
U Spec, 3
5 Set(a) & Set(b) => [a=b <=> ALL(c):[c @ a <=> c @ b]]
U Spec, 4
6 Set(a) & Set(b)
Join, 1, 2
7 a=b <=> ALL(c):[c @ a <=> c @ b]
Detach, 5, 6
8 ALL(y):[y @ a <=> y @ b]
Premise
9 [a=b => ALL(c):[c @ a <=> c @ b]]
& [ALL(c):[c @ a <=> c @ b] => a=b]
Iff-And, 7
10 a=b => ALL(c):[c @ a <=> c @ b]
Split, 9
11 ALL(c):[c @ a <=> c @ b] => a=b
Split, 9
12 a=b
Detach, 11, 8
13 ~ALL(y):[a @ y <=> a @ y]
Premise
14 ~~EXIST(y):~[a @ y <=> a @ y]
Quant, 13
15 EXIST(y):~[a @ y <=> a @ y]
Rem DNeg, 14
16 ~[a @ u <=> a @ u]
E Spec, 15
17 a @ u | ~a @ u
Or Not
18 ~a @ u => ~a @ u
Imply-Or, 17
19 ~~a @ u => ~~a @ u
Contra, 18
20 ~~a @ u => a @ u
Rem DNeg, 19
21 a @ u => a @ u
Rem DNeg, 20
22 [a @ u => a @ u] & [a @ u => a @ u]
Join, 21, 21
23 a @ u <=> a @ u
Iff-And, 22
24 [a @ u <=> a @ u] & ~[a @ u <=> a @ u]
Join, 23, 16
25 ~~ALL(y):[a @ y <=> a @ y]
4 Conclusion, 13
26 ALL(y):[a @ y <=> a @ y]
Rem DNeg, 25
27 ALL(y):[a @ y <=> b @ y]
Substitute, 12, 26
28 ALL(y):[y @ a <=> y @ b] => ALL(y):[a @ y <=> b @ y]
4 Conclusion, 8
------------------------------- end proof ----------------------------------
Just imagine for ZFC, we don't need them. Here is a proof:
/* Theorem Extensionality implies Indiscernibility */
28 ALL(y):[y @ a <=> y @ b] => ALL(y):[a @ y <=> b @ y]
4 Conclusion, 8
------------------------------- begin proof ----------------------------------
1 Set(a)
Axiom
2 Set(b)
Axiom
3 ALL(a):ALL(b):[Set(a) & Set(b) => [a=b <=> ALL(c):[c @ a <=> c @ b]]]
Set Equality
4 ALL(b):[Set(a) & Set(b) => [a=b <=> ALL(c):[c @ a <=> c @ b]]]
U Spec, 3
5 Set(a) & Set(b) => [a=b <=> ALL(c):[c @ a <=> c @ b]]
U Spec, 4
6 Set(a) & Set(b)
Join, 1, 2
7 a=b <=> ALL(c):[c @ a <=> c @ b]
Detach, 5, 6
8 ALL(y):[y @ a <=> y @ b]
Premise
9 [a=b => ALL(c):[c @ a <=> c @ b]]
& [ALL(c):[c @ a <=> c @ b] => a=b]
Iff-And, 7
10 a=b => ALL(c):[c @ a <=> c @ b]
Split, 9
11 ALL(c):[c @ a <=> c @ b] => a=b
Split, 9
12 a=b
Detach, 11, 8
13 ~ALL(y):[a @ y <=> a @ y]
Premise
14 ~~EXIST(y):~[a @ y <=> a @ y]
Quant, 13
15 EXIST(y):~[a @ y <=> a @ y]
Rem DNeg, 14
16 ~[a @ u <=> a @ u]
E Spec, 15
17 a @ u | ~a @ u
Or Not
18 ~a @ u => ~a @ u
Imply-Or, 17
19 ~~a @ u => ~~a @ u
Contra, 18
20 ~~a @ u => a @ u
Rem DNeg, 19
21 a @ u => a @ u
Rem DNeg, 20
22 [a @ u => a @ u] & [a @ u => a @ u]
Join, 21, 21
23 a @ u <=> a @ u
Iff-And, 22
24 [a @ u <=> a @ u] & ~[a @ u <=> a @ u]
Join, 23, 16
25 ~~ALL(y):[a @ y <=> a @ y]
4 Conclusion, 13
26 ALL(y):[a @ y <=> a @ y]
Rem DNeg, 25
27 ALL(y):[a @ y <=> b @ y]
Substitute, 12, 26
28 ALL(y):[y @ a <=> y @ b] => ALL(y):[a @ y <=> b @ y]
4 Conclusion, 8
------------------------------- end proof ----------------------------------
Julio Di Egidio
Sep 6, 2023, 10:22:15 AM9/6/23
to
On Monday, 4 September 2023 at 23:03:06 UTC+2, Julio Di Egidio wrote:
> Here is something I am trying to get my head around:
>
> ```coq
> Definition leibniz_eq {U : Type} (x y : U) : Prop :=
> forall (V : Type) (p : U -> V), p x = p y.
>
> Theorem leibniz_eq_equiv_eq {U : Type} (x y : U) :
> leibniz_eq x y <-> x = y.
> Proof. (* relatively easy: left as an exercise *) Admitted.
>
> Definition leibniz_eq_prop {U : Type} (x y : U) : Prop :=
> forall (p : U -> Prop), p x <-> p y.
>
> Theorem leibniz_eq_prop_equiv_eq {U : Type} (x y : U) :
> leibniz_eq_prop x y <-> x = y.
> Proof. (* relatively easy: left as an exercise *) Admitted.
>
> Lemma leibniz_eq_prop_equiv_leibniz_eq {U : Type} (x y : U) :
> leibniz_eq_prop x y <-> leibniz_eq x y.
> Proof. (* relatively easy: left as an exercise *) Admitted.
> ```
>
> I find quite puzzling that `leibniz_eq` and `leibniz_eq_prop`
> come up equivalent, despite the latter is (almost) only a
> special case of the former...
That's a doubt, but an even more stringent one now is this:
> Here is something I am trying to get my head around:
>
> ```coq
> Definition leibniz_eq {U : Type} (x y : U) : Prop :=
> forall (V : Type) (p : U -> V), p x = p y.
>
> Theorem leibniz_eq_equiv_eq {U : Type} (x y : U) :
> leibniz_eq x y <-> x = y.
> Proof. (* relatively easy: left as an exercise *) Admitted.
>
> Definition leibniz_eq_prop {U : Type} (x y : U) : Prop :=
> forall (p : U -> Prop), p x <-> p y.
>
> Theorem leibniz_eq_prop_equiv_eq {U : Type} (x y : U) :
> leibniz_eq_prop x y <-> x = y.
> Proof. (* relatively easy: left as an exercise *) Admitted.
>
> Lemma leibniz_eq_prop_equiv_leibniz_eq {U : Type} (x y : U) :
> leibniz_eq_prop x y <-> leibniz_eq x y.
> Proof. (* relatively easy: left as an exercise *) Admitted.
> ```
>
> I find quite puzzling that `leibniz_eq` and `leibniz_eq_prop`
> come up equivalent, despite the latter is (almost) only a
> special case of the former...
how does it come that leibniz_eq (whichever form), which is
an *extensional* equality, comes out equivalent to equality in
Coq, given (*) that equality in Coq is definitional equality, i.e.
purely syntactic (as in terms of "convertibility") and, as such,
purely *intensional*?? -- Am I just messing up somewhere?
(*) Not (yet?) really given, but closing this point is along the
lines of the same what-is-what as above...
Julio
Ross Finlayson
Sep 7, 2023, 1:43:14 AM9/7/23
to
Whether they remain sound, valid, well-formed under usual forms, ...,
is rather immaterial when any contradiction emits "material conditional"
any stipulation.
Now, if you add a certain amount of boilerplate like the relevance logic,
and make it so that only contrapositive makes direct implication, it would
seem a well-advised addition to such a usual logic, to prevent usual fallacies.
I'm trying to figure out for Quine, that there's a notion how to help interpret
Quine's various writings and derivations of logic, and about his opinion in
the real numbers as before or after the rationals, then about getting equality back
up front, and addressing where he does class/set distinction at the beginning, to
make a fuller formal logic, rich as it would be underneath, instead of running out
a simple, quickly simple logic, that's later less usually tractable, in what are say,
usually bounded resources (and especially in usually bounded resources, where it's
expected that always half the problems are hard and half the problems are easy,
not all easy).
I.e., it results then that later syllogisms are just part of as Kant put it, the analytic,
where the conditions are always making a context for them, establishing they're TND,
from the mutable grounds where they aren't.
It's not much more a complicated logic to make it first-class analytic.
Ross Finlayson
Sep 7, 2023, 2:37:24 AM9/7/23
to
See, it's easy to organize and reorganize things in fundamental logic. They still have to fit, ....
Then the challenge is "there exists a first-order logic, provide one", with the usual approach
to make low-order things a smooth "middling order".
Logic is small and light enough that you can usually attach a bespoke logic to any given set
of conditions. It's just like a usual data structure and a usual distribution. If you know the
distribution, then you can provide a provably optimal algorithm, of the data structure's
accessors and mutators. Similarly with logic, is for relating whatever related terms in
small local tableau, bringing the logic along, then providing first-class adapters to the logic
over that, what is usually called theorems. (In a world of models, models of theorems,
and altogether little theories.)
Julio Di Egidio
Sep 7, 2023, 1:35:19 PM9/7/23
to
On Thursday, 7 September 2023 at 08:37:24 UTC+2, Ross Finlayson wrote:
> On Wednesday, September 6, 2023 at 10:43:14 PM UTC-7, Ross Finlayson wrote:
> > It's not much more a complicated logic to make it first-class analytic.
I have explained in another thread how Syllogisms are not simply
> On Wednesday, September 6, 2023 at 10:43:14 PM UTC-7, Ross Finlayson wrote:
> > It's not much more a complicated logic to make it first-class analytic.
conditionals, though you can translate them to conditionals and
then they are tautologies... some of which need classical logic,
but never mind indeed.
> How about this, just having a universal quantifier, and demote the
> existential to a predicate.
is not primitive but inductively defined (i.e. it's a carrier of
evidence): from universal quantification the former, from the
underlying unification (as "convertibility" in CIC) mechanism
the latter. But what is primitive in Coq as in functional languages
generally, is "convertibility" which is definitional equality, and that
is an integral and primitive part of such languages... so yes, that
can be done, and apparently it is as powerful as to *prove* Leibniz
equality: and then I start speculating...
> Logic is small and light enough that you can usually attach a bespoke logic
> to any given set of conditions.
all interesting things, good and bad, actually happen, whence a
"simple" theory is *never enough*.
Julio
Ross Finlayson
Sep 7, 2023, 11:57:38 PM9/7/23
to
I coined the phrase "inductive impasse" because that's what
it is, where deduction brings back something that induction
doesn't carry out, through the limit. I'm not sure a given
existing name but maybe "analytic/synthetic divide" would suffice,
or as of a "deductive inductive divide".
Then, it seems like there are conditions for the limit where
what's so for the point at infinity is so for each, and those where
it's the opposite.
Hmm... if that's so maybe I picked it up when I scanned
the, "command", list. (Where what stuck out was "auto".)
But, mostly it's because of studying quantifier disambiguation.
(I.e., attaching the boundary/limit properties to the quantifier.)
Julio Di Egidio
Sep 8, 2023, 8:44:45 AM9/8/23
to
On Friday, 8 September 2023 at 05:57:38 UTC+2, Ross Finlayson wrote:
> Huh. Thanks, I think I learned something.
Did you really?
> Huh. Thanks, I think I learned something.
> I coined the phrase "inductive impasse" because that's what
> it is, where deduction brings back something that induction
> doesn't carry out, through the limit.
There is simply no point anymore...
*Plonk*
Julio
Julio Di Egidio
Sep 9, 2023, 3:59:37 AM9/9/23
to
On 25/08/2023 13:56, Julio Di Egidio wrote:
> ...a binary relation `phi` (formalized as a
> total propositional function)...
Indeed, together with a notion of *functional extensionality*
(represented by 'peq'), that 'phi' is a *total function* seems
all it takes for the "paradox" to apply.
```coq
Parameter U : Set.
Parameter phi : U -> U -> Prop.
Definition peq (p q : U -> Prop) : Prop :=
forall (x : U), p x <-> q x.
```
Conversely, the only way I have found to close the system is
by extending the domain with a non-standard element standing
for 'het', but extending 'phi' only partially:
```coq
Inductive W : Set :=
| W_f : U -> W
| W_i : W. (* a single non-standard element *)
(* [psi] is (as) a partial function on [W*W]. *)
Definition psi (w : W) (u : U) : Prop :=
match w with
| W_f u' => phi u' u
| W_i => het u
end.
```
Which seems to work, i.e. no "revenge" that I can guess, but
remains also only partly satisfactory: 'het' is now represented
in the system and can be "applied" to standard elements, still
standard elements cannot be "applied" to it...
The complete code can be found here:
<https://gist.github.com/jp-diegidio/0898b3eb0719ec9e48df87971693e4b6>
Julio
> ...a binary relation `phi` (formalized as a
> total propositional function)...
Indeed, together with a notion of *functional extensionality*
(represented by 'peq'), that 'phi' is a *total function* seems
all it takes for the "paradox" to apply.
```coq
Parameter U : Set.
Parameter phi : U -> U -> Prop.
Definition peq (p q : U -> Prop) : Prop :=
forall (x : U), p x <-> q x.
```
Conversely, the only way I have found to close the system is
by extending the domain with a non-standard element standing
for 'het', but extending 'phi' only partially:
```coq
Inductive W : Set :=
| W_f : U -> W
| W_i : W. (* a single non-standard element *)
(* [psi] is (as) a partial function on [W*W]. *)
Definition psi (w : W) (u : U) : Prop :=
match w with
| W_f u' => phi u' u
| W_i => het u
end.
```
Which seems to work, i.e. no "revenge" that I can guess, but
remains also only partly satisfactory: 'het' is now represented
in the system and can be "applied" to standard elements, still
standard elements cannot be "applied" to it...
The complete code can be found here:
<https://gist.github.com/jp-diegidio/0898b3eb0719ec9e48df87971693e4b6>
Julio
Mild Shock
Sep 10, 2023, 9:15:46 PM9/10/23
to
Did you just steal my proof that use extensionality,
in another thread? Cannot judge. Coq is as usual cryptic
unreadable tactic nonsense, not some nice proof trees.
Anyway, concerning your other idea. Can you maintain:
Definition aut (w : W) : Prop := phi w w.
Definition het (w : W) : Prop := not (aut w).
If you base aut on "psi" instead of "phi",
and if "psi" has the signature: (w : W) (u : U),
how do you want to form "psi w w"?
Do you have:
W ⊆ U?
By your definition W must satisfy, shorthand
exponentiation W^U for function space U -> W,
and + for disjoint sum:
W = W^U + W
Counter example U = ∅, there is a single empty
function, so W^U + W acts like a zero plus successor, and
a Peano structure W = ω satisfies that, but we dont have:
ω ⊆ ∅
in another thread? Cannot judge. Coq is as usual cryptic
unreadable tactic nonsense, not some nice proof trees.
Anyway, concerning your other idea. Can you maintain:
Definition aut (w : W) : Prop := phi w w.
Definition het (w : W) : Prop := not (aut w).
If you base aut on "psi" instead of "phi",
and if "psi" has the signature: (w : W) (u : U),
how do you want to form "psi w w"?
Do you have:
W ⊆ U?
By your definition W must satisfy, shorthand
exponentiation W^U for function space U -> W,
and + for disjoint sum:
W = W^U + W
Counter example U = ∅, there is a single empty
function, so W^U + W acts like a zero plus successor, and
a Peano structure W = ω satisfies that, but we dont have:
ω ⊆ ∅
Mild Shock
Sep 10, 2023, 9:27:52 PM9/10/23
to
Oops, I made an error. You don't have:
W = f(U) + i
I guess W ⊆ U is possible?
Again something like ω.
And therefore we have found a revenge!
Proof: Set U = { f^n(i) | n e N }, claim W = U.
We then have f(U) = { f^n+1(i) | n e N }, and we then have
W = f(U) + i = { f^n+1(i) | n e N } u {f^0(i)} = { f^n(i) | n e N } = U.
Q.E.D.
W = W^U + W
Its rather:
W = f(U) + i
I guess W ⊆ U is possible?
Again something like ω.
And therefore we have found a revenge!
Proof: Set U = { f^n(i) | n e N }, claim W = U.
We then have f(U) = { f^n+1(i) | n e N }, and we then have
W = f(U) + i = { f^n+1(i) | n e N } u {f^0(i)} = { f^n(i) | n e N } = U.
Q.E.D.
Julio Di Egidio
Sep 11, 2023, 12:28:20 PM9/11/23
to
On Monday, 11 September 2023 at 03:27:52 UTC+2, Mild Shock wrote:
> Oops, I made an error. You don't have:
> W = W^U + W
> Its rather:
> W = f(U) + i
Yes, it's an inductive definition, where 'f' and 'i'
> Oops, I made an error. You don't have:
> W = W^U + W
> Its rather:
> W = f(U) + i
are constructors. Here it is again for reference:
```coq
Inductive W : Set :=
| W_f : U -> W
| W_i : W. (* a single non-standard element *)
Here is the definition of `nat` for comparison:
```coq
Inductive nat : Set :=
| O : W (* zero *)
| S : U -> W. (* succ *)
```
> I guess W ⊆ U is possible?
see, and prove, that every term of U is coercible
to a term of W, but not the other way round.
Julio
Julio Di Egidio
Sep 11, 2023, 12:32:28 PM9/11/23
to
On Monday, 11 September 2023 at 18:28:20 UTC+2, Julio Di Egidio wrote:
> Here is the definition of `nat` for comparison:
>
> ```coq
> Inductive nat : Set :=
> | O : W (* zero *)
> | S : U -> W. (* succ *)
> ```
Eh, that should be:
> Here is the definition of `nat` for comparison:
>
> ```coq
> Inductive nat : Set :=
> | O : W (* zero *)
> | S : U -> W. (* succ *)
> ```
```coq
Inductive nat : Set :=
| S : nat -> nat. (* succ *)
```
where the point just was that
`S` too is a unary function.
Julio
Mild Shock
Sep 11, 2023, 12:50:08 PM9/11/23
to
Coq doesn't disallow a model instance where W ⊆ U ?
Is there a postulate that types, declared as : Set,
is disjoint from any other type. What if we want to do:
ℚ : Set /* Rational Numbers */
ℝ : Set /* Real Numbers */
We might want ℚ ⊆ ℝ.
The idea of a "Revenge Paradox" is to show the "possibility"
of a "Revenge", not the "necessesity" of a "Revenge".
So there is nothing wrong in probing, whether W ⊆ U
is possible. We don't need to prove that W ⊆ U necessarely holds.
Is there a postulate that types, declared as : Set,
is disjoint from any other type. What if we want to do:
ℚ : Set /* Rational Numbers */
ℝ : Set /* Real Numbers */
We might want ℚ ⊆ ℝ.
The idea of a "Revenge Paradox" is to show the "possibility"
of a "Revenge", not the "necessesity" of a "Revenge".
So there is nothing wrong in probing, whether W ⊆ U
is possible. We don't need to prove that W ⊆ U necessarely holds.
Mild Shock
Sep 11, 2023, 12:58:05 PM9/11/23
to
The possibility is often realized by:
i) Modifying the sentence slightly, like going from:
L : This sentences is not true.
To this sentence, which uses the vocabulary that the "resolution" proposes:
R : This sentences is not true and not indeterminate.
ii) What else, in what category falls W ⊆ U?
i) Modifying the sentence slightly, like going from:
L : This sentences is not true.
To this sentence, which uses the vocabulary that the "resolution" proposes:
R : This sentences is not true and not indeterminate.
ii) What else, in what category falls W ⊆ U?
Julio Di Egidio
Sep 11, 2023, 1:46:23 PM9/11/23
to
On Monday, 11 September 2023 at 18:50:08 UTC+2, Mild Shock wrote:
> Coq doesn't disallow a model instance where W ⊆ U ?
As I said, it is easy to *prove* that U *strict*
> Coq doesn't disallow a model instance where W ⊆ U ?
"subset" of W. Hint: given the definition of W...
You spamming imbecile. I'll add systematic use of
non-ascii characters to the list of your nefarious practices.
(STFU.)
Julio
Mild Shock
Sep 11, 2023, 3:45:14 PM9/11/23
to
I don't think its provable. Because you are not allowed
to confuse u and W_f u. The former is an element of
U and the later is an element of W. You cannot prove
in Coq that this here holds:
u = W_f u
to confuse u and W_f u. The former is an element of
U and the later is an element of W. You cannot prove
in Coq that this here holds:
u = W_f u
Mild Shock
Sep 11, 2023, 4:01:01 PM9/11/23
to
So why would it be a possibility and not a necessesity a
"Revenge Paradox" ? I don't know, its just a gut feeling.
Maybe Soul Kripke could formalize this gut feeling better.
Here is an example, which just came to my mind, which would
reduce the possibilities, and just by this move, create a
revenge paradox, namely:
C : This sentences is not true and nothing is indeterminate
Thats kind of a cheating (C) revenge paradox.
Bye
Its also an Antinomy:
∀x(Fx ∧ (Tx ∧ Ux)), ∀x¬(Fx ∧ Tx), ∀x¬(Fx ∧ Ux), ∀x¬(Tx ∧ Ux)
entails ∀x¬(Tx ↔ (Fx ∧ ∀y(Fy ∨ Ty))).
https://www.umsu.de/trees/#~6x(Fx~1Tx~1Ux),~6x(~3(Fx~1Tx)),~6x(~3(Fx~1Ux)),~6x(~3(Tx~1Ux))|=~6x~3((Tx~4Fx~1~6y(Fy~2Ty)))
Julio Di Egidio
Sep 15, 2023, 1:56:41 PM9/15/23
to
On 09/09/2023 09:59, Julio Di Egidio wrote:
<snip>
no such thing as diagonalizing psi, W and U are just
not the same type; moreover, for any given phi, there
are in fact infinitely many possible anti-diagonals,
not just one.
I am now trying to count how many exactly...
Julio
<snip>
> Conversely, the only way I have found to close the system is
> by extending the domain with a non-standard element standing
> for 'het', but extending 'phi' only partially:
>
>
> ```coq
> Inductive W : Set :=
> | W_f : U -> W
> | W_i : W. (* a single non-standard element *)
>
> (* [psi] is (as) a partial function on [W*W]. *)
> Definition psi (w : W) (u : U) : Prop :=
> match w with
> | W_f u' => phi u' u
> | W_i => het u
> end.
> ```
But that's doubly unsatisfactory: because there is
> by extending the domain with a non-standard element standing
> for 'het', but extending 'phi' only partially:
>
>
> ```coq
> Inductive W : Set :=
> | W_f : U -> W
> | W_i : W. (* a single non-standard element *)
>
> (* [psi] is (as) a partial function on [W*W]. *)
> Definition psi (w : W) (u : U) : Prop :=
> match w with
> | W_f u' => phi u' u
> | W_i => het u
> end.
> ```
no such thing as diagonalizing psi, W and U are just
not the same type; moreover, for any given phi, there
are in fact infinitely many possible anti-diagonals,
not just one.
I am now trying to count how many exactly...
Julio
Julio Di Egidio
Sep 15, 2023, 2:16:28 PM9/15/23
to
sequences that are provably different in at least
one place from every sequence in the given list.
Julio
Julio Di Egidio
Sep 15, 2023, 3:19:51 PM9/15/23
to
0 => 1
---
1 => 2^1 - 1 = 1.
00
01 => 2
---
10
11 => 2^2 - 2 = 2.
000
001
010 => 3
---
011
100
101
110
111 => 2^3 - 3 = 5.
and so on.
Generalizing: |AD(n)| = 2^n - n ~~> O(2^n)
where AD(n) is the set of "anti-diagonals" at level n.
So, in fact, nothing new to see here.
(I was hoping not to find as many, but I had in mind
a wrong definition of "ad", a too strict one: the
definition I have given above is the correct/intended
one, and, as seen here, it does not lead to anything
new. -- Luckily, that didn't take very long.;))
Julio
Mild Shock
Sep 15, 2023, 4:59:34 PM9/15/23
to
You can define diagonals relative to X in Y as,
where Δ is the symmetric difference:
diag(X,Y) := { x e Y | ∀y(y e X => x Δ y = {} }
You can use it to find Liar Paradoxs. For example
the Liar Paradox that Dan Christensen is using, is:
A <-> B
it is relatively easy to find: Use 0 to encode A,
and 1 to encode B, then X = {{0}, {1}} is classical
logic, and Y = {{}, {0}, {1}, {0, 1}} is Belnap FOUR,
diag(X,Y) = {{}, {0,1}}
which is the same as A <-> B. The diagonal is
automatically an Antinomy in X, but satisfiable
in Y. Anything between X and Y, excluding X and
including Y does also satisfy it, and in Dan Christensens
terminology consists a "resolution":
1) { {}, {0}, {1}}: 3-valued Logic with bottom, the solution proposed
by Dan Christense, is a resolution
2) { {0}, {1}, {0,1}: 3-valued Logic with top, sometimes called
Logic of Paradox, would be also a resolution
3) { {}, {0}, {1}, {0,1}: 4-valued Logic with bottom and top, called
Belnap FOUR, would be also a resolution
Have Fun!
where Δ is the symmetric difference:
diag(X,Y) := { x e Y | ∀y(y e X => x Δ y = {} }
You can use it to find Liar Paradoxs. For example
the Liar Paradox that Dan Christensen is using, is:
A <-> B
it is relatively easy to find: Use 0 to encode A,
and 1 to encode B, then X = {{0}, {1}} is classical
logic, and Y = {{}, {0}, {1}, {0, 1}} is Belnap FOUR,
diag(X,Y) = {{}, {0,1}}
which is the same as A <-> B. The diagonal is
automatically an Antinomy in X, but satisfiable
in Y. Anything between X and Y, excluding X and
including Y does also satisfy it, and in Dan Christensens
terminology consists a "resolution":
1) { {}, {0}, {1}}: 3-valued Logic with bottom, the solution proposed
by Dan Christense, is a resolution
2) { {0}, {1}, {0,1}: 3-valued Logic with top, sometimes called
Logic of Paradox, would be also a resolution
3) { {}, {0}, {1}, {0,1}: 4-valued Logic with bottom and top, called
Belnap FOUR, would be also a resolution
Have Fun!
Ross Finlayson
Feb 21, 2024, 12:18:17 AMFeb 21
to
You'll find in lots of theorem-proving machinery
such notions as "programmer's intent", as with
regards to the, "whatever", type.
It's not great, but, it's what it's for.
It's not considered "thoroughly conscientious".
such notions as "programmer's intent", as with
regards to the, "whatever", type.
It's not great, but, it's what it's for.
It's not considered "thoroughly conscientious".
Ross Finlayson
Feb 21, 2024, 1:05:28 PMFeb 21
to
The usual concept here is "GIGO".
There's another usual concept that "formal systems shouldn't allow
garbage or nor garbage out", the above basically refers to the "bilge".
There's another usual concept that "formal systems shouldn't allow
garbage or nor garbage out", the above basically refers to the "bilge".
0 new messages