Virgil
Posts:
8,833
Registered:
1/6/11
|
|
Re: � 488 Who said this?
Posted:
May 2, 2014 7:39 PM
|
|
In article <6de6d38e-aa27-4517-ba4d-8005e6f62cd3@googlegroups.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.
If one wants to do it in any of the various ways WM seems to want to do
it, I don't believe it can be done at all!
>
> Dan
> Download my DC Proof 2.0 software at http://www.dcproof.com
> Visit my new Math Blog at http://www.dcproof.wordpress.com
--
|
|
