Can a second-order theory that contains the first-order theory of the structure (N,+,x,1) have a decidable axiomatization?

Question

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

Answer 1

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.