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.