🚀 go-pugleaf

In article <22791@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:
>In article  <1992Sep23.165809.44902@Cookie.secapl.com> Frank Adams writes:
>]In article <22556@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:
>]>In article  <1992Sep22.161011.116130@Cookie.secapl.com> Frank Adams writes:
>]>]In article <22514@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:
>]>]>  If informal reasoning was good enough
>]>]>to establish the formal system, why is it not good enough to use
>]>]>instead of the formal system?

>]>Second, by "informal reasoning", I do not mean "sloppy", "hand-waving"
>]>or "skipping steps".  I only mean that there is no fixed set of
>]>syntactic (formal) manipulations that lead you from one syntactic
>]>theorem to another.
>]
>]In practice, the reasoning used directly in proofs is "informal" in this
>]sense.  However, new sorts of steps to use in proofs are normally justified
>]by reducing to previously accepted techniques; the exceptions are rare and
>]usually controversial.
>
>That does not make it a formal system.
>
>]And, insofar as the proof techniques are ultimately
>]reducible to formal techniques, the whole structure of techniques is "based
>]on" the formal system.
>
>I hate to bicker about word choices, but there is no relationship
>between "reducible to formal techniques" --in the sense you are using
>it-- and formal systems.  You are using the word "formal" to mean
>something like "rigorous" or even just "mathematical".

No; I mean reducible to the techniques of some formal system.

>  A "formal
>system", as I said before is a set of syntactic rules, a calculus, a
>set of rewrite rules, a formal transformation system, a set of rules
>specified by a type 0 grammar ... stop me if one of these rings a
>bell :-).
>
>Here is a formal system:
>
>  FXY -> X
>  GXYZ -> XYXZ

I think you mean:
   GXYZ -> XY/XZ

And, of course, this is not yet a formal system; it has no syntactic rules,
no calculus.  The casual reader does not even know that F and G are
constants, and X, Y, and Z are variables.

>[Proofs in a formal system are meaningful to a Platonist only when meanings
>are attached to the symbols of the formal system.]

How many times do I have to agree with this before you stop bring it up?

>  And in such a case, all he has
>proven is that the calculus represents a set of valid deductive steps,
>but it does not represent the set of _all_ valid deductive steps.  So
>why should he restrict himself to this particular set?

(1) *No one* is suggesting that mathematicians restrict themselves to the
direct use of the rules in the formal system.  Even logicians working
directly with a formal system take shortcuts with the deductive steps in
that system.

(2) By using rules derivable from a formal system, the degree to which we
are entitled to believe that our results are correct (our confidence) is
increased.

There is, in fact, no reason to restrict oneself to the rules derivable from
a particular formal system.  In fact, when doing mathematics, it is at times
useful to use rules or facts (the distinction blurs, outside a formal
system) which are known to be false: like assuming the existence of
infinitesimal real numbers.  But, when you publish, you had better use
accepted rules (which are reducible to a formal system); or provide good
evidence for the validity of the new rule (which will in practice enable
construction of a new formal system incorporating it -- usually by the
inclusion of a new axiom in an existing system).

Formal systems have, for the Platonist, a useful, if indirect, role to play
in ensuring rigor and the closely related area of understanding and accepting
published proofs.  That is all I am saying.  It *isn't* an especially
glamorous role; it isn't really crucial; but it is useful.