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



What is the reverse mathematics of first-order logic and propositional logic?
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. 


