[FOM] An attempt of a constructive proof for Takeuti Conjecture

Sandro Skansi skansi.sandro at gmail.com
Sat Mar 1 08:35:36 EST 2014

The system I used (SO^\triangle), should be classical, not intuitionistic,
and as far as I have checked it is based oh the system G3c (i.e. its second
order expansion with the modification of using sets rather than multisets)
of Troelstra and Schwichtenberg (in their book Basic Proof Theory). As such
it admits a proof of (A \implies absurdity) \implies absurdity |- A
(provable in classical logic):

_______________Axiom(for formula F)
A |- absurdity, A
______________________R\implies      ______________Axiom(for absurdity)
|- (A \implies absurdity), A                      absurdity |- A
         ((A \implies absurdity) \implies absurdity) |- A

[I hope the "ASCII-proofs" I made display correctly]
I agree if it were intuitionistic it should not prove this sequent, but as
it does, it is not intuitionistic. The fact that it proves this, as well as
A|- ((A \implies absurdity) \implies absurdity):

______________Axiom(for formula F)       _____________________Axiom(for
A |- A, absurdity                                      absurdity, A |-
               A, (A\implies absurdity) |- absurdity
           A|- ((A \implies absurdity) \implies absurdity)

Makes it a system of classical logic, just as G3c is. The modifications I
made (rules for second order \forall, sets instead of multisets), do not
alter this.

Best regards,
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20140301/27bb9b88/attachment.html>

More information about the FOM mailing list