Re: all the incompleteness proofs are worthless untill...

On 2008-03-24, in sci.logic, Marshall wrote:
It is possible that I have given the wrong impression. I do not
propose that formalization is supposed to *replace* understanding,
or that formalization is *necessary* for understanding. However I do
feel that while mathematics is a quite mature field, formalization
is quite immature, (and by that standard, computation is in its
infancy.)

I wouldn't say that computation is in its infancy, but serious actual
use of formal systems, as opposed to their mathematical study,
certainly is. It seems we now agree that we can have sober and clear
understanding of this and that that does not consist in formal
calculi, in which case I'm somewhat unsure of just what our original
disagreement was about.

My background may be contributing to a perspective that is so
merely pragmatic as to be obscure if not actually unpleasant
to actual mathematicians or logicians. Most of my interest in
logic is in mechanizing it, and for that, a formalism is required.

Indeed. What is it that you want to mechanise logic for?

My mention of the brain was only to dispel any arguments against
the *possibility* of mechanization.

That was never the issue. Let's assume that we're entirely mechanical
and that there is no obstacle to mechanising this and that. It still
does not follow that a sober and clear understanding should result in
a formal theory, which was my sole point.

As to your larger question: I don't entirely know. What lies
beyond the next unexplored horizon?

Who knows? It's quite a mystery. If we are, however, to make sense of
what would follow from our being able to do this and that, we must be
very clear on just what we mean by this and that. For, in case of
future contingencies, there are real ambiguities, and not just the
purely imaginary sort philosophers like to carp on. A perfect example
of such ambiguity is "the brain is a formal system" which, as said,
has no apparent meaning -- any number of things could be meant by it,
and if we are to make something of what follows or does not follow
from it further explanations are required. Often with stuff that is
not just a matter of speculation about the future no such elaborate
explanations are required since it's clear what is meant, and in such
instances I wouldn't dream of chiming in with irrelevant "But just
what do you mean by that?"s.

Who is better equipped to find the next exciting theorem? I cannot
help but feel that the person with the sophisticated theorem prover
as an assistant is in a better position than the person without. The
more of what we understand, via "informal rigor", can be captured by
this logic assistant, the better it can assist the person.

Certainly. But informal rigour is informal precisely because there's
no obvious way of formalising it. What follows or does not follow from
this or that informal principle is an indeterminate matter, and
modelling our reasoning in this regard in, say, a computer program
would require teaching computers all the vagueness, waffling,
uncertainty, ambiguities, and so on, that goes to our natural language
reasoning. This might or might not be possible in reality, but we're
nowhere near that point as things currently stand.

An an ice-cream cone is a formal system. It is a formal system
because it is a physical object, and it is entirely
epistemologically valid to look upon its melting slowly in the
spring air as a computation in thermodynamics.

What is the formal language of an ice-cream cone, what are its axiom,
its rules of inference? We can of course view anything as anything,
but in this case the view seems somewhat pointless. We were talking
about the brain being a formal system. In the sense you wish to view
the ice-cream cone as a formal system we could view the brain as
carrying out computations in Newtonian mechanics, as we drop it from
the seventh floor, breathlessly witnessing the splash it makes hitting
the ground. I now recall your sage advice, that I should, instead of
just taking cheap pot-shots at people, explain more clearly what I see
as the correct alternative. The point is simply what I explained
before: that in order to make some sense of ice-cream cones or brains
being formal systems we need more than the bald assertion "the brain
is a formal system"; an explanation of just what is meant by
this. This need is not a theoretical philosophical need but a
practical one: it makes no obvious sense to say of either brains or
ice-cream cones that they are formal systems and thus nothing can be
said of what follows or does not follow from such an assumption.

(As an abstraction of computation it is probably not very good;
better instead simply to consider it a tasty treat, perhaps as an
alternative to a deep-fried banana.)

Indeed!

--
Aatu Koskensilta (aatu.koskensilta@xxxxxxxxx)

"Wovon man nicht sprechen kann, daruber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
.

Relevant Pages

  • Re: all the incompleteness proofs are worthless untill...
    ... or that formalization is *necessary* for understanding. ... At the end of the preface of Pierce's "Types and Programming ... The whole brain/ice cream cone subdiscussion came about over ...
    (sci.logic)
  • Re: The Asymmetry of Identity
    ... meanings of named things are stipulated. ... Formalization is the process of modelling a system ... This is not to say that appending commentary (stipulating meanings) to ... a program (formal system) is a pointless exercise. ...
    (sci.logic)
  • Re: Formal statement of godels 1.incompleteness theorem
    ... |which formal system) IS IT STATED. ... arithmetization of syntax and coding of proof etc., ... formaly stated without formalization of metamathematics, ... hence by contradiction and using the consistency ...
    (sci.logic)
  • Re: Formal statement of godels 1.incompleteness theorem
    ... this is a stronger result due to Robinson. ... |which formal system) IS IT STATED. ... arithmetization of syntax and coding of proof etc., ... formaly stated without formalization of metamathematics, ...
    (sci.logic)
  • Re: Formal statement of godels 1.incompleteness theorem
    ... this is a stronger result due to Robinson. ... |which formal system) IS IT STATED. ... arithmetization of syntax and coding of proof etc., ... formaly stated without formalization of metamathematics, ...
    (sci.logic)
Quantcast