FOM: Restricted Provability

[Harvey Friedman]

This is a followup to the posting Restricted Provability, 5/6/01, 2:13PM.

Firstly, I should have said at the beginning of the second paragraph, that
I was talking about systems based on intuitionistic logic in the second
paragraph.

Secondly, there is a very interesting error in my posting. I wrote:

>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.

The first claim is true but the second claim is, interestingly, false. In
fact, I had already essentially published a negative answer. Here is the
story.

R.K. Meyer asked a number of people this question:

is every sentence of PA without absurdity provable in the system PA- = PA
without the axiom

Sx = 0 implies absurdity?

I answered this in the negative by first showing that the field of complex
numbers obeys PA without that axiom. And then showing that there is a
sentence without absurdity which is provable in PA but which fails in the
field of complex numbers.

This was applied to a problem in relevance logic and appeared autonomously
in the paper

(with R.K. Meyer), Wither Relevance Arithmetic?, Journal of Symbolic Logic,
Vol. 57, No. 3, September 1992, pp. 824-831.

But we can apply this result here. First of all, the sentence is in fact
provable in HA. We can let HA- = HA without the axiom

Sx = 0 implies absurdity.

Note that in HA- and PA-, absurdity is allowed to appear in the induction
scheme.

THEOREM. Any sentence without absurdity is provable in MA if and only if it
is provable in HA-. Any sentence without absurdity, provable in MA, is true
in the complex field.

This is because we can interpret absurdity as (therexists x)(Sx = 0)
throughout a given proof in MA. And we can interpret absurdity as 1 = 0
throughout any given proof in HA-.

We now come to the question of consistency proofs. What is the status of
Con(MA)?

Here are several notions of consistency for MA, or any system of arithmetic
based on minimal logic:

1. 1 = 0 is not provable.
2. absurdity is not provable.
3. some sentence without absurdity is not provable.
4. some sentence is not provable.

Note that obviously 2 implies 1 implies 3 implies 4.

THEOREM. EFA proves that MA does not prove absurdity. EFA proves that HA-
is consistent. Godel showed that PA is consistent if and only if HA is
consistent within EFA, and that PA does not prove the consistency of HA.

NOTE: This kind of thing may cause you to want to avoid negation entirely.
This can easily be done as follows. Simply ban negation and absurdity from
the language, and instead use 1 = 0 for absurdity. Then the usual axioms
and rules without negation or absurdity allow one to derive every formula
(without negation or absurdity) from 1 = 0.

More generally, in a finite language, we can always avoid negation and
absurdity by using the sentence that asserts that all atomic formulas with
no function symbols or constants hold universally. We can use this as the
synthetic absurdity.

QUESTION: Is MA a significant system in terms of mathematical practice?
When is a sentence provable in MA?