Return to Answer

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 the topos of simplicial sets.

The longer answer relies on an interesting characterization of the subobject classifier of the topos of simplicial sets. (Thanks to Zhen Lin for helping me to explain this characterization.) Sieves on $[n]$ in $\Delta$ can be identified with (possibly empty) abstract simplicial complex $A_n$ with vertices drawn from $[n] = \{0,\ldots,n\}$. The sieve corresponding to $A_n$ consists of all order preserving maps $f:[m]\to[n]$ such that $\{f(0),\dots,f(m)\} \in A_n$. 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_n \in \Omega(n)$ to $A_m = \{x \subseteq [m] : \{g(i) \mid i \in x\} \in A_n\}$.

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). 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.

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 (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.

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.

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 the topos of simplicial sets.

The longer answer relies on an interesting characterization of the subobject classifier of the topos of simplicial sets. (Thanks to Zhen Lin for helping me to explain this characterization.) Sieves on $[n]$ in $\Delta$ can be identified with (possibly empty) abstract simplicial complex $A_n$ with vertices drawn from $[n] = \{0,\ldots,n\}$. The sieve corresponding to $A_n$ consists of all order preserving maps $f:[m]\to[n]$ such that $\{f(0),\dots,f(m)\} \in A_n$. 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_n \in \Omega(n)$ to $A_m = \{x \subseteq [m] : \{g(i) \mid i \in x\} \in A_n\}$.

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. 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.

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 (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.

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 the topos of simplicial sets.

The longer answer relies on an interesting characterization of the subobject classifier of the topos of simplicial sets. (Thanks to Zhen Lin for helping me to explain this characterization.) Sieves on $[n]$ in $\Delta$ can be identified with (possibly empty) abstract simplicial complex $A_n$ with vertices drawn from $[n] = \{0,\ldots,n\}$. The sieve corresponding to $A_n$ consists of all order preserving maps $f:[m]\to[n]$ such that $\{f(0),\dots,f(m)\} \in A_n$. 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_n \in \Omega(n)$ to $A_m = \{x \subseteq [m] : \{g(i) \mid i \in x\} \in A_n\}$.

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). 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.

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 (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.

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 the topos of simplicial sets.

The longer answer relies on an interesting characterization of the subobject classifier of the topos of simplicial sets. (Thanks to Zhen Lin for helping me to explain this characterization.) Sieves on $[n]$ in $\Delta$ can be identified with (possibly empty) abstract simplicial complex $A_n$ with vertices drawn from $[n] = \{0,\ldots,n\}$. The sieve corresponding to $A_n$ consists of all order preserving maps $f:[m]\to[n]$ such that $\{f(0),\dots,f(m)\} \in A_n$. 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_n \in \Omega(n)$ to $A_m = \{x \subseteq [m] : \{g(i) \mid i \in x\} \in A_n\}$.

Interestingly, the lattice of abstract simplicial complexes on $[n]$ (with intersection and union) is the free bounded distributive lattice $D_{n+1}$ on $n+1$ generators. 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.

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 (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.

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 the topos of simplicial sets.

The longer answer relies on an interesting characterization of the subobject classifier of the topos of simplicial sets. (Thanks to Zhen Lin for helping me to explain this characterization.) Sieves on $[n]$ in $\Delta$ can be identified with (possibly empty) abstract simplicial complex $A_n$ with vertices drawn from $[n] = \{0,\ldots,n\}$. The sieve corresponding to $A_n$ consists of all order preserving maps $f:[m]\to[n]$ such that $\{f(0),\dots,f(m)\} \in A_n$. 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_n \in \Omega(n)$ to $A_m = \{x \subseteq [m] : \{g(i) \mid i \in x\} \in A_n\}$.

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. 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.

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 (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.