On Friday, May 2, 2014 5:12:28 PM UTC-4, Virgil wrote:
> > > Is it not possible to have one line involving more than one rule and/or
> > > axiom at a time in your system? >
> > No. That is the nature of formal proof. If you have a formal proof, you know > > > exactly what rules, axioms and assumptions were used. That's why any > > > important foundational issues such as we are discussing here really have to > > > be resolved by formal proof. You don't want hidden assumptions sneaking in. > > > > While it may well be possible, and even idea in some ways, to build a > > proof structures in which each line only applies one rule, most everyday > > proofs do not do so, so the NECESSITY of a "one line, one rule" rule is > > not clearly established. >
Foundational issues in their fields having been settled centuries ago, very few mathematicians work with formal proofs. If you want to try to reformulate the foundations of all of mathematics, as WM seems to want to do, it can only be done with formal proofs on the basis of one line, one rule.