Take the 2-minute tour ×

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

share|improve this question
This all sounds rather circular... –  Harry Gindi May 16 '10 at 10:29
I'm trying to find the best linear approximation :) –  Colin Tan May 16 '10 at 10:36

3 Answers 3

up vote 10 down vote accepted

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 RCA0. It is well known that Goedel's incompleteness theorems can be formalized in PRA, and so they can also be formalized in RCA0.

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

The underlying reason that WKL0 is needed is that RCA0 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, RCA0 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 RCA0.

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

share|improve this answer

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

share|improve this answer

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.


share|improve this answer
I'm glad you pointed out the distinction between strength and expressiveness. The fact that PA is able to handle all the purely syntactic aspects of finite formulas is an essentially complete response to the "expressiveness" question. Finite syntax can also be managed in much weaker systems such as PRA, of course, so PA is much stronger than necessary. –  Carl Mummert May 16 '10 at 13:13
What I'm interested in is how much mathematics is needed to express first-order logic –  Colin Tan May 16 '10 at 15:12
Not what can I express with first order logic. –  Colin Tan May 16 '10 at 15:12
Well, you can encode the sentences as Gödel-numbers. You can argue that such encoding is not readable anymore. To keep some structure, you need something like a pair. Then the sentences can be expressed while keeping most of the original structure. Then, the sentences that are part of the logic, is a Turing-halting problem. You can have a discussion about the most natural way to describe Turing-halting problems. Personally I prefer a system that has non-deterministic properties, because that is often more natural. So, I don't see what your question actually is. –  Lucas K. May 16 '10 at 16:26
@Colin: The issue Lucas raised is that "express" is really just a property of the language you have and its standard model. What you almost certainly want is a theory that can not only express something like "$n$ is a code for a formula" but can also perform elementary syntactical manipulations. Such as: given a code for a formula $\phi$, one of its free variables $x$, and some other formula $y$, produce the substitution instance $\phi(y)$. The ability to perform this type of manipulation requires some logical strength, not just expressiveness. The theory PRA is certainly strong enough. –  Carl Mummert May 17 '10 at 11:25

Your Answer


