> > > How far should I expect to get? Is there some ceiling that you're > anticipating? >
Yes. Two ceilings: 1) you need a full set of axioms (predicate calculus and a set theory) 2) If you have a constructive logic, you will have to express ideas like: I have a proof in this state and in all subsequent states but not in that one? How do you do that. Girard's original work is here. http://girard.perso.math.cnrs.fr/linear.pdf And his archives deserve to be read. http://girard.perso.math.cnrs.fr/Archives.html The axioms of his predicate calculus is here p. 11. http://girard.perso.math.cnrs.fr/Synsem.pdf Unfortunately it is in the Gentzen's style. -- FL -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/686180a0-360f-428f-b3e5-14c18b2d1cee%40googlegroups.com.
