# How to express Con(PA) as a first-order statement?

I read from somewhere that

Fact 1. PA, which refers to the first-order version, is not finitely axiomatizable.

At the same time, the second incompleteness theorem says that there is no proof in PA for Con(PA). This theorem takes for granted that Con(PA) can be expressed as a statement in first-order logic. (Here the language consists of the constant symbol 0, the unary successor function S and the binary functions + and $\times$.) The question is

Question 2. How to express Con(PA) as a first-order sentence?

You have to take care that Fact 1 does not become false as a result of your answer to Question 2. Actually I believe that

Conjecture 3. If you have a way to express Con(PA) as a finite statement, I can turn this into a finite representation of PA, thus violating Fact 1.

Proving or arguing against Conjecture 3 is highly appreciated, besides answering Question 2.

-
Well, while $PA$ isn't finitely axiomatizable, it is recursively axiomatizable. That is, given an arbitrary formula, we can tell if it's an axiom of $PA$. So there exists a formula $Ax(x)$ which is true (in the standard model) if and only if $x$ is the Goedel number of an axiom of $PA$. It's enough to express $Th(x)$ (true if $x$ is the Goedel number of a $PA$ theorem) and so $Con(PA)$.
Wait. How do you define a formula? That is the $P()$ in the induction axiom $[P(0)\land\forall x(P(x)\to P(x+1))]\to\forall xP(x)$. –  Zirui Wang Oct 17 '11 at 13:08