# Does Gödel's theorem rule out derivations from all possible logical systems or just first-order logic?

Gödel's first incompleteness theorem excludes the possibility of formulating a consistent and decidable set of first order sentences which are true in standard arithmetic from which the truth/falsehood of every possible first order statement can be derived.

But Peano's axioms include a second order statement. I know that second order logic is incomplete so that we can't derive the truth or falsehood of all second order statements, but since peano's axioms (with the second order induction axiom rather than the first order scheme) characterize arithmetic up to isomorphism, it seems possible that we could derive at least all first order statements using the second order axiom.

My question is essentially about the meaning of Gödel's theorem: does it merely exclude the possibility of using first order logic to derive all first order statements, or does it exclude the possibility of proving the truth/falsehood of all first order statements, no matter what additional extensions we add to the logical system (such as infinite disjunction, second-order formula's, statements about countability, etc)?

EDIT: My question hasn't been answered yet, so let me clarify:

Here is ONE possible way to think about my question:

• We cannot have a set of first order axioms for arithmetic from which all first order sentences can be proven or disproven (first incompletness theorem)

• We cannot prove for all second order sentences all their second order implications. (incompleteness of second order logic)

• But can we have a set of second order axioms for arithmetic, from which we can prove or disprove all first-order sentences? (or is this ruled out by godel's theorem as well?)

• en.wikipedia.org/wiki/First-order_logic section "Completeness and undecidability" – Peter Apr 1 '18 at 6:44
• @Peter, I don't see what completeness and undecidability have to do with this? completeness of FO-logic is no longer relevant when we extend it with additional expressions, and undecidability refers to valid FO sentences, but if we extend the language, then we may be able to make derivations that cannot be reduced to a valid FO sentence, since they contain e.g. second order quantifiers. – user56834 Apr 1 '18 at 8:13

• Sorry, that statement is indeed wrong. I forgot to add that the sentences have to be $S^{arithmetic}$ sentences that are true in the standard structure of arithmetic. Surely then the statement is correct? – user56834 Apr 1 '18 at 9:21