Georgi Guninski
2011-06-25 12:18:41 UTC
Is the Daniel Schepler's inconsistency real?
Daniel Schepler proved [1][2] both T and ~T using only a plausible axiom and I couldn't find any cheating in his proof (I admit I am dumb).
Possibly due to a coq ``anomaly'' (read a bug) coq gives strange error when using both T and ~T (well maybe coded on purpose)
In his code T and ~T are [uat_maximal_card] and [uat_not_maximal_card].
Assuming excluded middle, does it mean one of T and ~T is necessarily true so it can be taken as an axiom?
According to my tests if I take as an axiom one of them, in *both* cases I can prove False using exactly his approach.
One of the proofs will have axiom False (genuinely proved by him but unusable due to a bug),
but the other must be real inconsistency.
For testing I just replaced [Lemma] by [Axiom] and commented out the
proof (leaving the proof for the contrary).
Is this correct?
[1] https://sympa-roc.inria.fr/wws/arc/coq-club/2011-06/msg00099.html?checked_cas=2
[2] https://sympa-roc.inria.fr/wws/arc/coq-club/2011-06/msg00100.html?checked_cas=2
Daniel Schepler proved [1][2] both T and ~T using only a plausible axiom and I couldn't find any cheating in his proof (I admit I am dumb).
Possibly due to a coq ``anomaly'' (read a bug) coq gives strange error when using both T and ~T (well maybe coded on purpose)
In his code T and ~T are [uat_maximal_card] and [uat_not_maximal_card].
Assuming excluded middle, does it mean one of T and ~T is necessarily true so it can be taken as an axiom?
According to my tests if I take as an axiom one of them, in *both* cases I can prove False using exactly his approach.
One of the proofs will have axiom False (genuinely proved by him but unusable due to a bug),
but the other must be real inconsistency.
For testing I just replaced [Lemma] by [Axiom] and commented out the
proof (leaving the proof for the contrary).
Is this correct?
[1] https://sympa-roc.inria.fr/wws/arc/coq-club/2011-06/msg00099.html?checked_cas=2
[2] https://sympa-roc.inria.fr/wws/arc/coq-club/2011-06/msg00100.html?checked_cas=2