0

Hedman in his "A First Course in Logic" (2004) says, in p.359,

"... we now demonstrate a second-order theory containing $T_N$ that does have a decidable axiomatization." where $T_N$ is the first-order theory of arithmetic of the structure $N=\(N|+,x,1)$.

But after a few paragraphs later he says,

"It follows from proposition 8.1 that second-order logic does not have completeness.That is, we cannot hope to define second-order analogues for first-order resolution and formal proofs. By Gödel’s First Theorem, there is no such algorithm."

My question is: Do not these two quotes contradict each other? Because the former says of a theory that it is decidable, while the latter says that it is not.

Thank you

Ozgur Demir
  • 3

1 Answers1

0

Perhaps Hedman is not perfectly clear here, but I think the claims are these.

There is a set of second-order axioms $2A$ such that the semantic consequences of those axioms include all the first-order truths $T_N$. And (i) it is effectively decidable what's an axiom in $2A$.

But (ii) it is not effectively decidable whether a given sentence of first-order arithmetic, a candidate member of $T_N$, is indeed a semantic consequence of $2A$.

(i) and (ii) are consistent.

Peter Smith
  • 54,743
  • Thank you very much Sir. I thought that a decidable axiomatization refers to a set of sentences such that, given any sentence, it can be determined by an algorithm that whether the sentence is derivable from the set of sentences. But I now understand that a decidable axiomatization is a set of sentences such that, given any sentence, it can be determined whether this sentence belongs to this set of sentences or not. – Ozgur Demir Jan 17 '24 at 20:16