3

Since second order arithmetic is finitely axiomatazible why do not work with it, and insted we prefer first order Peano Axioms that include induction scheme?

George Chailos
  • 87
  • 1
    We do work with the second order axiomatisation. What makes you think we do not? It is still interesting to understand the first order properties too, but that does not mean we exclude the higher order properties. – Ittay Weiss Jun 12 '16 at 05:07
  • For one thing, there's no complete proof procedure for 2nd order arithmetic. – BrianO Jun 12 '16 at 05:19
  • 1
    Thanks a lot BrianO. Also in second order induction we quantify over sets, so most probably we require set existence . Probably this is another disandvantage – George Chailos Jun 12 '16 at 11:41
  • 2
    @BrianO and OP: Careful - "second order arithmetic" is also the name of a first-order theory! (Not, however, a finitely axiomatizable one.) – Noah Schweber Jun 13 '16 at 00:25
  • I meant the second order Peano axioms. Where the first order induction scheme is replaced by a single axiom that quantifies over sets – George Chailos Jun 13 '16 at 06:00

1 Answers1

7

On one hand, we do work with second-order arithmetic in contemporary logic. Many people work in a program called Reverse Mathematics, which is based on the use of second-order arithmetic. This is one of many active areas of contemporary logic.

Second-order logic has two different semantics: "full" semantics and "Henkin" semantics. In the former, the nine Peano axioms describe a unique structure. But there is no complete deductive system for this structure: the set of sentences that are true in it is too complex of a set to be generated by any effective set of axioms. In Henkin semantics, the Peano axioms no longer describe a unique structure, but we have a complete proof procedure, so that a sentence is provable if and only if it is true in all Henkin structures.

In either case, second-order arithmetic is not actually finitely axiomatizable. We just hide the axioms somewhere else when we use full semantics. When write out formal proofs from the Peano axioms, the proofs will include set-existence axioms. For example, the only way to apply the induction axiom from the Peano axioms is to construct a set first. There are an infinite number of these set-existence axioms, and the collection of sentences that we could prove would be much smaller if we only included the nine Peano axioms without also using any set-existence axioms. For example, we would no longer be able to use the induction axiom in any nontrivial way.

The reason that these axioms are not listed in the nine Peano axioms is that, when we use full semantics for second-order logic, the set-existence axioms are viewed as logical axioms rather than as axioms of our particular theory. In full semantics, the set-existence axioms are already true in the unique structure for the natural numbers. When we use Henkin semantics, we do include the set-existence axioms as part of the axioms of our theories, because they no longer come "for free". The latter option is how we treat second-order arithmetic in Reverse Mathematics.

The hidden use of set-existence axioms is one reason that little is done with second-order arithmetic in full semantics. In order to get all the strength of full semantics, we have to look at a theory such as the Peano axioms from the perspective of a set theory that allows us to construct the sets. It is often better to deal with these set-existence axioms explicitly.

Moreover, the collection of sentences that are true in the full model of second-order arithmetic do depend on the background set theory: there are sentences of second-order arithmetic which express facts that are independent of ZFC set theory. So, although the Peano axioms try to determine a unique model of arithmetic, there are still some properties of that model that they don't determine on their own.

Carl Mummert
  • 81,604
  • I appreciate yoypur answer. I am completely covered – George Chailos Jun 13 '16 at 06:01
  • @GeorgeChailos If this answer satisfies you, you can accept it by clicking the check mark to the left of the answer (under the upvote/downvote buttons). Besides giving the answerer a reputation bonus, this also moves the question off the "unanswered" list. – Noah Schweber Sep 05 '18 at 18:02