What is the reverse mathematics of first-order logic and propositional logic?

Question

Suppose one tries to formalize first-order logic. How much "strength" is required to do this?

Strength can mean in various senses:

1. The fragment of ZFC needed to codify first-order logic.
2. Which system of 2nd-order arithmetic is needed to codify first-order logic. (reverse mathematics)
3. The fragment of PA needed to codify first-order logic.
4. Categorial logic?

Codify means be able to (i) represent formulae and sentences, (ii) recognize proofs, (ii) represent structures and models.

(I'm also interested to the answer for this question in the case of propositional logic.)

Answer 1

In general, "reverse mathematics" refers to work with subsystems of second-order arithmetic only; it does not include ZFC. Assuming this is actually what you meant, everything is in Stephen Simpson's book Subsystems of second-order arithmetic.

All the basic syntactics of formulas can be done in a primitive recursive way, and can be directly formalized into RCA₀. It is well known that Goedel's incompleteness theorems can be formalized in PRA, and so they can also be formalized in RCA₀.

The restriction of Goedel's completeness theorem to countable theories is equivalent to WKL₀ over RCA₀, as is the similar restriction of the compactness theorem. The corresponding theorems for propositional logic are also equivalent to WKL₀ over RCA₀.

The underlying reason that WKL₀ is needed is that RCA₀ is not strong enough to prove that the deductive closure of an arbitrary set of sentences exists. If one adds a hypothesis that the input theory is already deductively closed, RCA₀ will do. This is all made precise in Simpson's book.

There has been some interesting work [1] on the reverse mathematics strength of the atomic model theorem of elementary model theory, which turns out to be very weak in the sense of reverse mathematics while still being stronger than RCA₀.

[1] Denis R. Hirschfeldt; Richard A. Shore; Theodore A. Slaman. "The atomic model theorem and type omitting". Trans. Amer. Math. Soc. 361 (2009), 5805-5837.

Answer 2

Just as in any area of mathematics, different parts of the subject have different strengths. The theory of Reverse Mathematics investigates these strengths by determining for a large number of mathematical theorems, including theorems arising in the development of first order logic, the weakest axioms that are able to prove them. In order to do this, one reverses the usual direction of mathematical proof, by proving the axioms from the theorems, over an extremely weak base theory.

The remarkable fact of Reverse Mathematics is that many theorems of classical mathematics fall into five large equivalence classes, consisting of provably equivalent theorems. Many instances of this are listed on the Wikipedia page I link to above.

It appears that all the most trivial parts of logical syntax can be developed in the weak base system $RCA_0$, and this may be the answer to your question. For more powerful parts of the theory, one needs stronger axioms.

• A weak version of the Goedel Incompleteness Theorem (for countable theory, already closed under conseqeunce) is also provable already in the base theory $RCA_0$. (As is the Baire Category theorem and the existence, but not uniqueness, of an algebraic closure for any countable field.)

• The Completeness Theorem for countable languages is equivalent to $WKL_0$. (As is the Heine-Borel theorem, the Jordan curve theorem, and many others.)

• the sequential completeness of the reals and various forms of Ramsey's theorem are equivalent to $ACA_0$.

• Comparability of well-orders and Open Determinacy are equivalent to $ATR_0$.

• the Cantor-Bendixon theorem is equivalent to $\Pi^1_1-CA_0$.

Answer 3

First of all, there is a difference between 'strength' and 'expressiveness'. This is not always unambiguous used in articles and literature.

With 'strength' is usually meant the possibility of a system to proof certain sentences. When comparing two systems for strength, one can limit the comparison to a certain subset of sentences.

Considering your question, I do think that you mean 'expressiveness'.

If you have first order logic + induction scheme + definitions for addition and multiplication, you can express any problem of discrete mathematics.

You need to build a 'pairing' construction and a 'transitive reflexive closure' construction. With those two, you can do anything. With some tricks with addition and multiplication, you can construct both.

You can also opt to start with a pairing operator and closure, and construct addition and multiplication from that.

If you have higher order logic, you don't need the addition and multiplication, because higher order logic allows the construction of pairing and closure in a different way.

So, I think the answer to your question is that you can codify all logics (with finite sentences) with First Order PA (or the question is not clear).

When talking about strength. First order PA + addition + multiplication, can't prove the consistency of itself. You need second order logic, with the ability to have second order formulas as induction hypothesis to prove consistency of first order logic + PA.

Lucas