lo.logictopos-theory
Is the consistency of classical third-order arithmetic provable in the logic of a topos with natural numbers?
(My guess would be yes, but I haven't seen this anywhere.)
Edit: in the original version I used the name PA$_3$ as an abbreviation for classical third-order arithmetic, and comments have followed suit, but I've since learnt that this name refers to a different theory (the classical theory of third order functions).
IIRC, the calculus of inductive constructions is equi-interpretable with ZFC plus countably many inaccessibles -- see Benjamin Werner's "Sets in Types, Types in Sets". (This is because of the presence of a universe hierarchy in the CIC.)
As I understand it, the homotopy type theory project does not need (or want?) the full consistency strength of Coq; they make use of it simply because it is one of the better implementations of type theory. Instead, what makes this work interesting is not its consistency strength, but its focus on a wholly new dimension of logical complexity: the complexity of equality (which, utterly amazingly, they relate to homotopy type). It puts me in mind of a famous quotation of Rota:
“What can you prove with exterior algebra that you cannot prove without it?” Whenever you hear this question raised about some new piece of mathematics, be assured that you are likely to be in the presence of something important. In my time, I have heard it repeated for random variables, Laurent Schwartz’ theory of distributions, ideles and Grothendieck’s schemes, to mention only a few. A proper retort might be: “You are right. There is nothing in yesterday’s mathematics that could not also be proved without it. Exterior algebra is not meant to prove old facts, it is meant to disclose a new world. Disclosing new worlds is as worthwhile a mathematical enterprise as proving old conjectures.” (Indiscrete Thoughts, 48)
(This is not meant as criticism of your question, but just as a caution not to let old battles cause us to lose sight of the new innovations brought to us.)
That said, as a sometime constructivist, I do not find consistency to be a primary philosophical notion. If PA is consistent, so is PA+$\lnot$Con(PA). That is, systems can lie despite being consistent, and so I hesitate to build my foundations on consistency. Instead, I prefer a proof-theoretic justification for logical systems, such as Gentzen's proof of cut-elimination. This guarantees that a system is not merely consistent, but that theorems actually have proper proofs. For a good introduction to these ideas, you can hardly do better than Per Martin-Lof's Siena lectures, "On the Meaning of the Logical Constants and the Justification of the Logical Laws".
I should be clear that these are more stringent conditions than consistency, and hence offer no way at all of avoiding the obstacles that the halting/incompleteness theorems pose. Heyting and Peano arithmetic are equi-consistent: there is no reason to trust constructivism more, if consistency strength is all that you are interested in. It is other logical qualities that make constructivism attractive.
The consistency of ZFC + IC is perhaps a little bit too much to ask, but I believe the next best thing is true:
Conjecture. Every boolean topos1 with dependent choice in which every set of reals is Lebesgue measurable contains a well-founded model of ZFC. In fact, every real is contained in a well-founded model of ZFC.
The proof that Con(ZF + DC + LM) implies Con(ZFC + IC) shows that in any model $V$ of ZF + DC + LM, $\aleph_1$ (of $V$) is an inaccessible cardinal in the constructible universe $L$ and therefore the inner model $L$ satisfies ZFC + IC. In fact, it shows that $\aleph_1$ is inaccessible in $L[a]$ for every real $a$ and therefore $L_{\aleph_1}[a]$ is a well-founded model of ZFC that contains $a$. I will now argue that we can still make sense of "$L_{\aleph_1}[a]$ is a well-founded model of ZFC that contains $a$" in a boolean topos with dependent choice and I will explain why I believe why this is true in a boolean topos with dependent choice in which all sets of reals are Lebesgue measurable.
Since there are no actual material sets around, we must first find a substitute. A boolean topos can still make sense of HC, the collection of all hereditarily countable sets, by amalgamating all countable well-founded extensional structures $(\mathbb{N},E)$. More precisely, one can show that any two such structures have at most one transitive embedding between them and that any two of them can be amalgamated into a third. (All that is needed for this is arithmetic transfinite recursion.) Then the limit of this directed system of countable well-founded extensional structures under transitive embeddings is the required HC.
Once we have HC, we can do a bit of set theory in there, thinking of its elements as actual material sets. In fact, assuming dependent choice, HC is a very nice model: it satisfies comprehension, replacement, choice and the basic combinatorial axioms but it doesn't have powersets, of course, since every set is countable. The ordinals of HC form a well-ordering that we will call $\aleph_1$. Working in HC, one can construct $L_\eta[a]$ for every $\eta \in \aleph_1$ and every $a \subseteq \omega$. Therefore, one can make sense of the substructure $L_{\aleph_1}[a]$ of HC, which is a well-founded model of a fragment of ZFC + $V = L[a]$ and the question whether $L_{\aleph_1}[a]$ is a model of ZFC makes sense.
The key ingredient that connects these ideas with Lebesgue measurability is the following theorem of Raisonnier:
Theorem. Assume ZF + DC. If there is an uncountable well-orderable subset of $\mathbb{R}$ then there is a non-measurable set of reals.
I don't know whether this goes through in a boolean topos with dependent choice. However, since this is a theorem of "ordinary mathematics," I conjecture that it does! The theorem does use some "fancy objects" such as rapid ultrafilters but these do make sense in a boolean topos and, in the presence of dependent choice, so does Lebesgue measure. I could be wrong, but I can't see any immediate obstructions to Raisonnier's Theorem in a boolean topos with dependent choice.
Now, the $a$-constructible reals $\mathbb{R}^{L[a]} = \mathbb{R}\cap L_{\aleph_1}[a]$ form a well-orderable set of reals since $L_{\aleph_1}[a]$ has a definable wellordering. Therefore, assuming that Raisonnier's Theorem goes through, in any boolean topos with dependent choice where all sets of reals are Lebesgue measurable, it must be the case that $\mathbb{R}^{L[a]}$ is countable for every $a \subseteq \omega$. Then, the usual argument that shows that $\aleph_1$ is inaccessible in $L[a]$ goes through to show that $L_{\aleph_1}[a]$ is a model of ZFC.
To summarize, at Alex's request, the above sketches a proof of the following:
Theorem. In a boolean topos with dependent choice where all well-orderable sets of reals are countable, every real is contained in a well-founded model of ZFC.
So the truth of the initial conjecture rests only on the truth of Raisonnier's Theorem in a boolean topos with dependent choice. Note that the conclusion is rather strong. Since the models are well-founded, all $\Sigma^1_2$ statements that are true in such models are also true in the ambient topos. In particular, every such topos proves that ZFC is not only consistent but also $\Sigma^1_2$-sound.
To get the relative consistency of ZFC+IC as in Shelah's Theorem, we would need to continue the construction of $L$ past $\aleph_1$ and show that this leads to a model of ZFC in the limit. It is unlikely that this is possible without some kind of additional completeness assumptions on the topos.
1For the sake of brevity, by "topos" I always mean "topos with a natural number object."
Best Answer
Let $\Omega_{\neg\neg} = \{p \in \Omega \mid \neg\neg p \Rightarrow p\}$ be the object of $\neg\neg$-stable truth values, and let us write $P_{\neg\neg}(A) = {\Omega_{\neg\neg}}^A$ for the object of $\neg\neg$-stable subobjects of $A$. Observe that $\Omega_{\neg\neg}$ is a complete Boolean algebra, and this fact can be shown in the internal logic of a topos.
Now, it seems to me that one can build a model of $\mathsf{PA}_n$ for each $n$, by interpreting its logic in $\Omega_{\neg\neg}$, and the (higher-order) predicates as elements of the iterates of the $\neg\neg$-powersets ${P_{\neg\neg}}^k(\mathbb{N})$.
Supplemental: I initially claimed we can have a model of $\mathsf{PA}_\infty$, but Paul pointed out I was overstating the case. Indeed, to have a model of $\mathsf{PA}_\infty$ we would need a single object that encompasses all finite iterates $\neg\neg$-powersets ${P_{\neg\neg}}^k(\mathbb{N})$ at once, says something like $\coprod_{n \in \mathbb{N}} {P_{\neg\neg}}^k(\mathbb{N})$. However, in an elementary topos such an object need not exist. A counter-model is the set $V_{\omega + \omega}$ of sets of rank below $\omega + \omega$.