I am looking for a closed statement (i.e. not depending on any parameter objects) which is true in the internal logic of the topos of simplicial sets, but is not an intuitionistic tautology. Ideally, I would like it to be a simple universal statement of propositional logic (e.g. "for all propositions P, Q, and R, blah blah", like LEM or de Morgan's law).


(To clarify: this has nothing to do with higher topoi or homotopy type theory; it's purely a question about ordinary 1-categorical 1-topos theory.)



Internal logic of the topos of simplicial sets
Short answer: the Kreisel-Putnam axiom $(\lnot p \to (q \lor r)) \to ((\lnot p \to q) \lor (\lnot p \to r))$ is not an intuitionistic tautology but it is valid for any subobjects of an object in the topos of simplicial sets.


The longer answer relies on an interesting characterization of the subobject classifier $\Omega$ of the topos of simplicial sets. (Thanks to Zhen Lin for helping me explain this characterization.) Sieves on $[n]$ in $\Delta$ can be identified with (possibly empty) abstract simplicial complexes $A$ with vertices drawn from $[n] = \{0,\ldots,n\}$. The sieve corresponding to $A$ consists of all order preserving maps $f:[m]\to[n]$ such that $\{f(0),\dots,f(m)\} \in A$. So, for each $n$, $\Omega(n)$ can be identified with the set of all such abstract simplicial complexes and for $g:[m]\to[n]$, $\Omega(g):\Omega(n)\to\Omega(m)$ takes each $A \in \Omega(n)$ to $B = \{x \subseteq [m] : \{g(i) \mid i \in x\} \in A\}$.


Interestingly, the lattice of abstract simplicial complexes on $[n]$ (with intersection and union) is the free distributive lattice $D\_{n+1}$ on $n+1$ generators with a free top element (but no free bottom element though it still has a bottom element). Every finite bounded distributive lattice is a Heyting algebra by defining implication via $$(p \to q) \equiv \bigvee \{r \mid p \land r \leq q\},$$ where the big join makes sense since there are only finitely many possibilities for $r$. The logical operators $\land,\lor,\to:\Omega\times\Omega\to\Omega$ can be computed pointwise using the Heyting algebra structure of $D\_{n+1}$. In other words, ${\land}(n):\Omega(n)\times\Omega(n)\to\Omega(n)$ takes each pair of abstract simplicial complexes $A\_n,B\_n$ on $[n]$ to $A\_n \cap B\_n$, and similarly for $\lor$ and $\to$. Thus any propositional formula which is true in $D\_{n+1}$ for every $n$ will be valid for generalized truth values in the topos of simplicial sets. I don't know a simple characterization of this logic but it at least satisfies the Kreisel-Putnam axiom.


To verify the Kreisel-Putnam axiom in $D\_{n+1}$, suppose $P$, $Q$, $R$ are abstract simplicial complexes over $[n]$. Note that $\lnot P$ consists of all nonempty $x \subseteq [n]$ that are disjoint from every element of $P$. If nonempty, which is the interesting case, this simplicial complex has a maximal element that I will denote $z$. Now $\lnot P \to (Q \lor R)$ consists of all $x \subseteq [n]$ such that $x \cap z \in Q \cup R$. Since $\lnot P \to Q$ (resp. $\lnot P \to R$) similarly consist of all $x \subseteq [n]$ such that $x \cap z \in Q$ (resp. $x \cap z \in R$), we see that $\lnot P \to (Q \lor R)$ and $(\lnot P \to Q) \lor (\lnot P \to R)$ correspond to the same abstract simplicial complexes.


