0
$\begingroup$

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.

  • 0
    It all relies on the representability of a certain kind of functions, and it actually takes a lot of work to prove that a statement such as $Con(PA)$ as a first-order sentence. Fact 1 is correct, and conjecture 3 is wrong: $Con(PA)$ only tells you that there are no codes of proofs of $0=1$ in $PA$, it also gives you the ability to enumerate $PA$'s axioms but it doesn't contain them2017-12-06

1 Answers 1

4

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

  • 1
    We aren't oracles and we don't have access to any oracles. We can execute algorithms, however.2011-10-19