For which subsystems T of 2nd order arithmetic is there a model of T + $\neg$Con(T)?

Question

A theory T might have the following property: there is a model of T + $\neg$Con(T)

1st order PA has this property, but full 2nd order PA doesn't.

Among subsystems of 2nd order arithmetic, which ones have this property and which ones don't?

With respect to consistency strength, what is the strongest subsystem that has the property, and what is the weakest subsystem that doesn't have the property?

Since some subsystems are incomparable I'm not sure there is a unique strongest with (or weakest without) the property.

Answer 1

Any subsystem of 2nd order arithmetic $T$ in the usual sense (i.e. theory of the sort discussed in Simpson's book or a cousin) is a recursively axiomatized two-sorted first-order theory which includes PA.

Hence Gödel's second incompleteness theorem applies, and $T \not\vdash Con(T)$.

Therefore $T + \neg Con(T)$ is consistent, and hence has a model by Gödel's completeness theorem.

Answer 2

As the question points out, second-order PA with full semantics is categorical, and its only model is the standard model. But the set of axioms for that theory is extremely small: finite, with 9 axioms in one common axiomatization. In particular, there is only one induction axiom: $$ (\forall X)[0 \in X \land (\forall n)[n \in X \to Sn \in X] \to (\forall n)[n \in X]]$$ and there are no comprehension (set-existence) axioms at all (these are often taken as logical axioms in full semantics, like the axioms for equality).

So it makes little sense to look at subsystems of that theory - which of the 9 axioms would you omit?

When we talk about subsystems, we move to Henkin semantics. The difference is that we no longer insist that the second-order part of each model must be the powerset of the first-order part. Now we have to include set-existence axioms (as a scheme) in our theory, because otherwise the second-order part of a model might be empty. This extended set of axioms, whose syntactic consequences give a theory known as $Z_2$, is the theory we use for forming subsystems of second-order arithmetic. Each of these subsystems, $S$, has a model of $S + \lnot \text{Con}(S)$, as long as it meets the hypotheses of the second incompleteness theorem (effectiveness and sufficient strength).