[FOM] Formalization Thesis vs Formal nature of mathematics

[Vladimir Sazonov]

William Messing wrote

> I do not understand what is meant here by "Consis_PA as a formula of PA,
> does not adequately express ...."  Is it being asserted that there is
> some meaningful notion of "feasible length" for a proof in PA, or in any
> other branch of mathematics?

Of course, this is problematic notion from mathematical point
of view. But intuitively this means that only mathematical
proofs which can be physically presented are allowed. If
somebody will assure you that he knows a proof of some
theorem and will present some ideas, a lot of hand waving
but will not be able to write down it because it is too long,
even physically impossible to write, will you accept this
as a proof?

If so, can one make explicit an upper
> bound for the length, say in terms of written lines of text, for the
> concept of "feasible length".  Would the Skewes number serve as such an
> upper bound, or 10^{10^{79}} or ...?

I prefer 2^1000 or even 2^100 as such an upper bound for
feasible numbers (or lengths).

Although the "semiset" F of feasible numbers (closed under +, but
upperbounded by 2^1000) is a highly vague set, it can be formalized
in a sense. (Actual infinitesimals in Analysis were eventually
also formalized.) Please see a brief exposition and references in

http://cs.nyu.edu/pipermail/fom/2006-February/009746.html

If, eventually the Riemann
> Hypothesis is proven and the proof is published in the Annals of
> Mathematics in a paper which is 100,000 pages long, would this qualify
> as "feasible length"?

I think computer would be able to check its correctness, if written
formally. I would accept this as feasible. Somebody else not. But,
anyway, feasible is a vague concept! Something is definitely
feasible (1000), something is definitely not (2^1000),
and there is no exact borderline (no last feasible number,
no first non-feasible). Take this as a system of axioms and
try to find out in which (formal and precise) sense it can be
considered as consistent. This exercise is simple, but,
I think, instructive.


> -------------------------------------------------------------------------
>
> Sazonov wrote:
>
> I know that FLT was proved (to be 'true'), and know virtually nothing
> on the proof. This is almost absolutely useless knowledge. It cannot be
> used, unlike the proof and definitions, constructs and algorithms (and
> corresponding intuitions) involved in the proof.
> ------------------------------------------------------------------------
>
>
> I do not understand the "this is almost useless knowledge."

The examples of using "BLACK BOXES" you presented in your
posting seem to me somewhat different from FLT. As I understand,
their formulations are much more complicated and interesting
than FLT. These very formulations (even without proofs) may
serve as something like complicated formal systems. The mere
invention of these formal systems (or formal objects) in
connection with the rich mathematical context (also a formal
system) can give new insights and new (conditionally proved)
theorems. "Opening" these BLACK BOXES makes this proofs
unconditional. These are really very good examples (however
I should admit that I am not a specialist at all).

With FLT whose formulation was known for ages, the existence of
its proof in a BLACK BOX gives essentially nothing. The majority
of consequences from FLT or from its negation were already done
long time ago. Of course the proof of FLT should definitely
contain a lot of very interesting things.


Vladimir Sazonov

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.