[FOM] Absolute truth vs. relative meaning and formal nature of mathematics

[Vladimir Sazonov]

Quoting Harvey Friedman <friedman at math.ohio-state.edu> Wed, 08 Feb 2006:

>> For example, I ASSERT, not as a mere speculation, that there is a
>> simple, but rather unusual FORMAL system of axioms and proof
>> rules in which a (semi)set of natural numbers 0,1,2,... < 1000
>> is FORMALLY definable which is PROVABLY closed under successor
>> and is also upper bounded by the number 1000. Quite intuitive
>> informal examples of such semisets from our real world are well
>> known (e.g. presented by P. Vopenka).
>
> If this formal system is reasonably simple, I would like to see it presented
> here on the FOM. If it is complicated, I would rather not.

It is technically quite simple, but some comments are necessary.
(See more details in http://www.csc.liv.ac.uk/~sazonov/papers/lcc.ps;
Sect. 4, etc.)

>
> It would seem to have to be inconsistent in the strong sense that you can
> easily produce an actual electronic file of the inconsistency.

No, this is physically impossible: the shortest contradiction
proof should contain at least 2^1000 symbols.


This theory is based on the LANGUAGE of first order logic with
equality and with non-logical symbols 0,1, +, log (base two
logarithm) and <. Let us also agree that negation is defined
formally as the implication to falsity, the latter being
considered as the primitive symbol. Everything else is as usual.

AXIOMS: a small list of universal closures of quantifier-free
formulas like the ordinary axioms on 0,1, +, log, and <.
For example, log 1 = 0, x <= log y implies x+1 <= log (y+y)
(<= means `less or equal'), etc. There is nothing peculiar
in the exact list, thus it is omitted. In particular, these
axioms postulate that successor (x+1) generates an infinite
(never ending) row of natural numbers, just as usual in PA.
(No induction axiom is postulated, however we could take some
weak form of it.)

But there is also one additional and unusual (also universal) axiom:

forall y log log y < 10.

Informally, variables range over feasible natural numbers
which should evidently satisfy all the above axioms (there
is, of course no last feasible number for which x+1 is
non-feasible), including the double logarithm axiom saying
that all feasible numbers are < 2^1024 (= 2^(2^10)). Thus,
these axioms can be considered as "true", but how to make
them to be FORMALLY consistent?


PROOF RULES are those of natural deduction (or of Gentzen
sequent calculus) with one formal restriction: only normal
deductions are allowed (resp., cut rule should be
excluded).

There is also "restriction" on the length of formulas,
terms and proofs: everything should have a feasible length
(physically written symbol-by-symbol, say, in computer
memory or in any other physically sufficiently "rigid" way).
All real mathematical proofs satisfy this restriction, except
they are usually semi-formal. Any formal theory, like the
above, is considered feasibly consistent if we have some
guarantee, or even only some strong belief that a feasible
proof of the formula "false" (the contradiction) is
impossible. (Note, that it is postulated that falsity implies
everything, what makes any contradictory theory formally
trivial, and vice versa. It follows that any feasibly
consistent theory is non-trivial - not everything is provable.)


THE ABOVE THEORY IS FEASIBLY CONSISTENT
(use Herbrand theorem to show that any proof of contradiction
must contain a formal term of the length > 2^1000).


Now, DEFINE

F(x) iff x=x (all feasible numbers),

M(x) iff "x is a middle (or medium? or non-large) number"
     iff exists y (x < log y),

All other (feasible) numbers in F minus M can be called large.
Define also

S(x) iff "x is a small number"
     iff exists y (x < log log y)


---------------------------------

DERIVABLE FACTS:

Then we can derive formally (with all the postulated
restrictions) by using the basic properties of logarithm:

M(0), M(1), not M(1024)
M(x) implies M(x+1),
M(x) implies x < 1024.

This is quite evident. Note that modus ponens (cut) rule
cannot be used freely to derive the apparent contradiction
with not M(1024) by showing with modus ponens M(2),
M(3),...,M(1024). We could try to eliminate the cut rule
from such deductions, but would only succeed in initial
steps. So, M(1024) is not possible to derive in this way without
using cut rule.

Thus, so defined (semi)set M of numbers is infinite,
but upperbounded by 1024.

---------------



This demonstrates what was announced, but this is not the full seory.
Let us also consider the following "surprising" fact which was not
anticipated when these considerations were first done.
Despite the above facts derived for M, we can derive formally that

M has the biggest number (some < 1024), or that

NOT forall x (M(x) implies M(x+1)).


(*) Thus, both not forall x (M(x) implies M(x+1)), and
    forall x (M(x) implies M(x+1)) are formally derivable.

Is this a contradiction? Formally, not. Contradiction means
derivation of the formula `false'. The negation in not A
is actually understood as A implies false. We could apply
modus ponens (cut) rule to derive from (*) the contradiction,
but this is not allowed formally. We could try to eliminate
the cut rule from this derivation, but this is physically
impossible - the cut elimination algorithm will never halt
in our (real) world. The intermediate results would
be so huge that there will be no place in our world
where to write down them. So, according to our criteria
this is not a contradiction.

--------------


Consider some more features of this formalism.

We can also formally derive that the semiset of small numbers
S is upper bounded by 10 (this is trivial) and, moreover,

there exists is a maximal small number (in our framework this is
not so self-evident)

The exact value of this number is, however, unknown (something
like 4 or 5; the logic is still classical - non-constructive).


Note that the above "normality" restriction on derivations
can be somewhat relaxed and reformulated to be intuitively
more plausible: ABBREVIATIONS OF TERMS ARE NOT ALLOWED
(I omit the details of argumentation). So, in principle,
we could avoid the (explicit) reference to cut rule in
our restriction on the form of derivations.

For example, abbreviating x+x as 2*x (or introducing new
function symbol for multiplication by two with the axiom
forall x (2*x=x+x)) will (evidently) make the theory
feasibly contradictory. This is an unusual feature, but
the idea of feasibility is so unusual that we should pay
something like that for its formalisation.


Vladimir Sazonov

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