FOM: Restricted Provability

[Harvey Friedman]

One of the main themes of f.o.m. is the study of significant restricted
notions of provability. The most well studied of these are represented by
the various standard formal systems of arithmetic, second order arithmetic,
and set theory, formulated in the usual first order predicate calculus
(classical logic). These include weak fragments of Peano arithmetic, Peano
arithmetic, various fragments of second order arithmetic as in reverse
mathematics, second order arithmetic, higher order arithmetic, Zermelo set
theory, Zermelo set theory augmented with various levels of the cumulative
hierarchy, ZF(C), and ZFC with various large cardinal axioms. There is an
impressive web of robust relationships involving interpretability,
conservativity, relative consistency, independence results, and various
informal distinctions among actual mathematical proofs.

Another source of significant restricted notions of provability are
represented by various standard formal systems of arithmetic, theories of
functions, theories of functionals, second order arithmetic with sets
(species) and sometimes functions, and set theory. These are less well
developed, with weaker connections with actual mathematical proofs, and
with less robustness. Nevertheless, the web of interconnections and
robustness is clearly sufficient to firmaly establish their significance,
although much more should be, can be, and will be, and is being done. E.g.,
intuitionistic propositional calculus, predicate calculus, and arithmetic,
are much richer than classical propositional calculus, predicate calculus,
and arithmetic. In particular, we have only scratched the surface in a
systematic study of the relationship between intuitionsitic and classical
arithmetic (HA and PA).

A third restricted notion of provability is to simply restrict the number
of symbols. Obviously any actual mathematical proof (without use of
computers) is going to be severely limited in length. Even if computers are
used, there are serious limitations in length. There are a number of
results that involve such a restriction. E.g., specific interesting
sentences (typically Sigma-0-1) which can be proved in a few pages using a
relatively strong system of axioms, but where any proof using somewhat less
must be ridiculously large.

The point of this posting is to ask whether there are any further
significant restricted notions of provability.

In particular, one can propose to weaken the logic below full
intuitionistic logic. Or perhaps weaken the logic below full classical
logic in such a way that it is not a fragment of intuitionistic logic. But
I do not know of any body of results for such weakenings of the logic that
indicate its significance as a restricted notion of provability for actual
mathematics.

Let me throw out one commonly considered restriction of intuitionistic
logic: minimal logic. I will give a standard sequent calculus version. We
use therexists, forall, and, or, implies, absurdity. Sequents are of the
form

Gamma arrows A

where A is a formula, and Gamma is a finite set (possibly empty) of formulas.

AXIOMS

Gamma arrows A

where A is an element of Gamma.

PROPOSITIONAL RULES

Gamma arrows A   Gamma arrows B
_________________________
Gamma arrows A & B


Gamma union {A} arrows C
_____________________
Gamma union {A & B} arrows C


Gamma union {B} arrows C
_____________________
Gamma union {A & B} arrows C


Gamma arrows A
______________
Gamma arrows A v B


Gamma arrows B
______________
Gamma arrows A v B


Gamma union {A} arrows C   Gamma union {B} arrows C
_______________________________________
Gamma union {A v B} arrows C


Gamma union {A} arrows B
___________________
Gamma arrows A implies B


Gamma arrows A   Gamma union {B} arrows C
________________________________
Gamma union {A implies B} arrows C


QUANTIFIER RULES

Gamma arrows A
____________________      where x is not free in Gamma
Gamma arrows (forallx)(A)


Gamma union {A[x/t]} arrows B
_________________________        where t is substitutable for x in A
Gamma union {(forallx)(A)} arrows B


Gamma arrows A[x/t]
__________________                 where t is substitutable for x in A
Gamma arrows (therexistsx)(A)


Gamma union {A} arrows B
______________________________     where x is not free in Gamma, B
Gamma union {(therexistsx)(A)} arrows B


CUT RULE


Gamma arrows A   Gamma union {A} arrows B
______________________________
Gamma arrows B

END

Now suppose we have a set of proper axioms; i.e., a set of formulas. A
proof in minimal logic of a formula B from this set is a proof in minimal
logic of a sequent Gamma arrows B, where Gamma consists entirely of zero or
more universal closures of the proper axioms.

Full intuitionistic logic is obtained from the above by adding the rule

Gamma arrows absurdity
_________________
Gamma arrows A

Let MA = minimal arithmetic consist of minimal logic together with the
following proper axioms in the language =,S,+,x.

EQUALITY AXIOMS

x = x
x = y arrows (phi arrows psi), where phi,psi are atomic formulas and psi is
obtained from phi by replacing zero or more occurrences of x by y.

SUCCESSOR AXIOMS

Sx = Sy implies x = y
Sx = 0 implies absurdity

EQUATIONS

x + 0 = x
x + Sy = S(x + y)
x dot 0 = 0
x dot Sy = (x dot y) + x

INDUCTION

(phi[x/0] & (forallx)(phi implies phi[x/Sx])) implies (forallx)(phi), where
phi is any formula in the language of MA.

END

THEOREM (well known). Any sequent without absurdity that is provable in
intutionistic logic is provable in minimal logic, even without the use of
absurdity. If a sentence is provable in HA, then the sentence obtained by
replacing absurdity with 1 = 0 is provable in MA.

QUESTION: Is there a basic mathematical theorem whose natural formalization
is provable in HA but not in MA? In the natural formalization, "notA" is
taken to be an abbreviation for "A implies absurdity". And if there is,
then is the restriction to MA mathematically significant? Or is it just a
haphazard restriction which does not correspond to any clear mathematical
intuition?

Minimal logic is just the first of a number of logics based on the idea of
"relevance". There are many other subsequent logics that are held in higher
repute in the philosophical community. We ask the same QUESTION for these
as well.

By the way, the status of HA for actual mathematics is still in a cloudy
state and is quite interesting.

There are now quite a number of important, celebrated, Pi-0-3 theorems
whose proofs seriously use classical logic, and for which it is considered
a very important problem to prove that you can obtain the existential
quantifier effectively from the front universal quantifier. I duscussed
this matter in my posting

Effective Bounds in Core Mathematics, Thu, 22 Jun 2000 19:04

mentioning these examples:

Mordell-Weil Theorem
The group of rational points on an abelian variety is finitely generated.

Roth's Theorem
There are only finitely many rational numbers alpha in K that approximate a
given irrational number beta to within H_K(alpha)^-2+epsilon.

Siegel's Theorem
A curve of genus at least 1 has only finitely many S-integral points.

Faltings' Theorem
A curve of genus at least 2 has only finitely many rational points.

and the book

Marc Hindry, Joseph Silverman, Diophantine Geometry, Graduate Texts in
Mathematics, Springer, 2000.

Such an effective bound would follow from very well known metatheorems from
the existence of a proof in HA. Presumably the theorems can be proved in PA.

But what about a real theorem that we KNOW can be proved in PA but not in HA?

The best example that I know is this:

EVERY MULTIVARIATE POLYNOMIAL WITH INTEGER COEFFICIENTS ASSUMES A VALUE OF
LEAST MAGNITUDE.

This is definitely provable in PA but not in HA.

The best example I know of of a really simple mathematical theorem that is
provable in PA but we have no idea how to prove it in HA is the following:

(e + pi) is irrational or (e - pi) is irrational.

Suppose not. Then by subtraction, 2e is rational, contradiction.