[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
_______________________________________________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>
More information about the FOM
mailing list