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

  • 0
    You see, your Ax() has to work in non-standard models. Yes, "given an arbitrary formula, we can tell if it's an axiom of PA." This assumes that the "arbitrary formula" is standard. But if Ax() is presented with a non-standard element of the model, how does it detect this? Won't this ability imply that we can _define_ what's standard and what's non-standard?2011-10-17
  • 1
    Of course in a nonstandard model Ax() will be true of some nonstandard numbers. But that's just (one of) reason(s) why Con(PA) may fail in these models and isn't provable in PA! When we say, "Ax(x) expresses 'x is the Goedel number of a PA axiom" or "Con(PA) expresses 'PA is consistent'", it is a statement about standard model, and their behavior in nonstandard models is irrelevant.2011-10-17
  • 0
    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)$.2011-10-17
  • 0
    In the normal way. Of course nonstandard numbers are not ever _really_ Goedel numbers of axioms of PA: that's the point.2011-10-17
  • 1
    What is "the normal way"? I find definitions are the most important thing in studying logic, because logicians define things differently in their inexpressive language. Look at Godel's definition of a proof; it's not required to be finite. Yes, it works in the standard model. But the existence of non-standard models (incompleteness, etc) illustrates the badness of their _definitions_ and nothing else.2011-10-18
  • 0
    OK. The 23rd concept in Godel's incompleteness paper defines what a formula is. But this may not be first-order.2011-10-19
  • 0
    By the way, "we can tell" doesn't mean "there is an algorithm". An oracle can tell whether x is in the halting set but no algorithm can do this. So are we oracles or algorithms?2011-10-19
  • 1
    We aren't oracles and we don't have access to any oracles. We can execute algorithms, however.2011-10-19