In article <email@example.com>, Dan Christensen <Dan_Christensen@sympatico.ca> wrote:
> On Friday, May 2, 2014 3:56:22 PM UTC-4, Virgil wrote: > > > > So, get busy, WM! Start by fully understanding what a formal proof is. > > > > > Imagine that a computer, without any knowledge of the outside world is > > > > > checking your proof against a pre-determined list of rules and axioms. > > > Every > > > > > line must be justified by citing exactly one of them. My software may > > > help > > > > > you help you get into the right mindset. > > > > > > > > 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. > > Dan > Download my DC Proof 2.0 software at http://www.dcproof.com > Visit my new Math Blog at http://www.dcproof.wordpress.com --