In article <email@example.com>, Dan Christensen <Dan_Christensen@sympatico.ca> wrote:
> 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.