# Does the fragment of intuitionistic propositional calculus with just $\to$ have a finitely-valued semantics?

Intuitionistic propositional calculus (IPC) has a topological semantics. IPC also does not have a sound and complete semantics with finitely many truth values.

I'm curious whether the fragment of IPC with only the connective $$\to$$ and no truth value constants has a finitely-valued semantics.

I'm also curious what sort of techniques in general are available for establishing whether a logic (given as a set of inference rules) has a finitely-valued semantics or not.

Let $$a^o$$ represent the interior of $$a$$. Let $$[a]$$ be the interpretation of $$a$$.

IPC has the following topological semantics. The topology in question is the standard topology over the reals $$\mathbb{R}$$.

$$[a \land b] = [a] \cap [b]$$ $$[a \lor b] = [a] \cup [b]$$ $$[a \to b] = ([a]^c \cup [b])^o$$ $$[\bot] = \varnothing$$ $$[\lnot a] = [a \to \bot]$$

I had a silly idea to try replacing $$(\mathbb{R}, \tau)$$ with the Sierpiński space and see how many connectives I need to remove from the language of IPC to make the Sierpiński space a correct interpretation.

I started off with $$\to$$ and $$\lor$$.

However, the statement $$(a \to b) \lor (b \to a)$$ is "Sierpiński-valid", but is not true for intuitionistic logic. As proof, consider $$a = (0, \infty)$$ and $$b = (-\infty, 0)$$. $$0$$ is not an element of $$[(a \to b) \lor (b \to a)]$$.

So, then I considered removing $$\lor$$.

The classical tautology is $$((a \to b) \to a) \to a$$ is not valid when $$a$$ is $$\{0\}$$ and $$b$$ is $$\varnothing$$, so this three-valued semantics successfully fails to be classical logic, but I'm not sure whether it's equivalent to the $$\to$$-fragment of IPC or not.

The set of equations $$\varphi = \top$$ that hold in the Heyting algebra of the Sierpiński space is a proper superset of the set of tautologies of the $$\rightarrow$$-fragment of the intuitionistic propositional calculus.

You already know that the Sierpiński space satisfies the equation $$(a \rightarrow b) \vee (b \rightarrow a) = \top$$, even though $$(a \rightarrow b) \vee (b \rightarrow a)$$ is not an intuitionistic tautology. You can use the second-order encoding of the intuitionistic connectives to produce the following sentence in the $$\rightarrow$$-fragment:

$$\varphi \equiv ((a \rightarrow b) \rightarrow c) \rightarrow ((b \rightarrow a) \rightarrow c) \rightarrow c$$

An algebra satisfies $$(a \rightarrow b) \vee (b \rightarrow a) = \top$$ for all $$a,b$$ precisely if it validates $$\varphi = \top$$ for all $$a,b,c$$. Hence, the Sierpiński space satisfies $$\varphi = \top$$.

edit: There is no finite universal Heyting algebra (and hence finite topological space) that satisfies only the tautologies of the $$\rightarrow$$-fragment. I don't have a reference off-hand (I'll try to find one), but you can take the Boolean algebra $$B_n$$ with $$n$$ generators, adjoin a new "top element" to it, and get a Heyting algebra with $$n+1$$ elements that satisfies an $$\rightarrow$$-equation (in many variables) that none of the previous algebras do. Regarding your question about "techniques for establishing that a logic has a finite-valued semantics": this usually happens only when every finite model of your algebra is generated by a single finite model. E.g. every finite Boolean algebra is the $$n$$-fold product of the $$2$$-element Boolean algebra, and an equation holds in a product algebra $$A \times B$$ precisely if it holds in both $$A$$ and $$B$$ (this is a fact from universal algebra).

• Thank you. I have two follow-up questions if that's okay. 1) What are the second-order encodings of the connectives? 2) Do you know whether $\to$-IPC has any finite semantics? I'm not sure how the equational technique you're describing (it looks a lot like universal algebra?) generalizes to cases where we have more than one designated truth value. Commented Aug 5, 2021 at 2:24
• @GregoryNisbet I added a paragraph on why the $\rightarrow$-fragment doesn't have a single finite semantics (although it does have the finite model property: if something is not a tautology, you can find a finite model that refutes the corresponding equation). For the second-order encodings: these are the same as Church encodings in System F. See e.g. slides 19 and 21 of Neel Krishnaswami's lecture. Commented Aug 5, 2021 at 2:38
• Regarding "more than one designated truth value": the opens of every topological space constitute a Heyting algebra, and completeness for Heyting semantics says that you can prove $\varphi \vdash \psi$ in intuitionistic logic precisely if the universal closure of the inequality $\varphi \leq \psi$ holds in every Heyting algebra. But said inequality holds precisely if $\varphi \rightarrow \psi = \top$. So it's always enough to consider equations of the form $\upsilon = \top$. Commented Aug 5, 2021 at 4:23