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

[Sandro Skansi]

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
_______________________________________________L\implies
         ((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
absurdity)
A |- A, absurdity                                      absurdity, A |-
absurdity
_________________________________________________________L\implies
               A, (A\implies absurdity) |- absurdity
________________________________________________R\implies
           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,
Sandro
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20140301/27bb9b88/attachment.html>