8
$\begingroup$

Gödel (1932) showed that intuitionistic propositional logic (more precisely, any fragment with implication and disjunction) is not a finitely many-valued logic. What about the pure implicational fragment?

$\endgroup$

2 Answers 2

12
$\begingroup$

The pure implicational fragment of intuitionistic propositional logic is not finite-valued.

Take your favorite $k \in \mathbb{N}$. It's easy to find a disjunction $t_1 \vee t_2 \vee \dots \vee t_n$ of Heyting algebra terms so that each term in $t_1,t_2,\dots,t_n$ consists only of variables and implications, and the universal closure of $t_1 \vee t_2 \vee \dots \vee t_n = \top$ holds in every finite Heyting algebra $(H, \wedge, \vee, \rightarrow, \bot, \top)$ with $|H| = k$, but fails in some Heyting algebra with $|H| > k$. The usual proof of non-finite-valuedness for IPC itself already gives rise to such a disjunction.

We can turn this into a disjunction-free formula with similar properties using the intuitionistic tautology $(A \vee B) \rightarrow ((A \rightarrow C) \rightarrow (B \rightarrow C) \rightarrow C)$.

If we pick a variable $z$ which does not occur in the terms $t_1,\dots,t_n$, then the universal closure of the equality $$(t_1 \rightarrow z) \rightarrow (t_2 \rightarrow z) \rightarrow \dots \rightarrow (t_n \rightarrow z) \rightarrow z = \top$$ holds in the implicational reduct $(H, \rightarrow, \bot, \top)$ of any Heyting algebra with $|H| = k$, by the tautology above. But by construction, the left hand side of this equality belongs to the implicational fragment, and is certainly not an intuitionistic tautology.

Every finite structure $(H, \rightarrow, \bot, \top)$ which obeys the implicational fragment of intuitionistic logic in the sense that the universal closure of $t=\top$ holds if the term $t$ is a tautology of this fragment, arises as a reduct of some Heyting algebra: the solutions to $x \rightarrow y = \top$ uniquely determine the order, and the order induces the structure of a distributive lattice $(H, \wedge, \vee)$.

Thus, no finite $(H, \rightarrow, \bot, \top)$ provides a complete semantics for the implicational fragment of intuitionistic propositional logic.

$\endgroup$
6
$\begingroup$

A related property in which the implicational fragment differs from full intuitionistic logic is that the former is locally finite: for every finite $n$, there are only finitely many inequivalent formulas in $n$ variables. As a consequence, the $n$-variable implicational fragment is determined by a single finite Kripke frame (whose size depends on $n$); as another consequence, the implicational fragment of every superintuitionistic logic has the finite model property. More generally, all this holds also for the $\{\to,\land,\bot\}$-fragment. This is known as Diego's theorem.

$\endgroup$
3
  • $\begingroup$ May I inquire about the source for this? $\endgroup$ Commented Mar 23, 2024 at 13:55
  • $\begingroup$ See e.g. Chagrov and Zakharyaschev, Modal logic. $\endgroup$ Commented Mar 23, 2024 at 17:59
  • $\begingroup$ Thank you for your comment! $\endgroup$ Commented Mar 24, 2024 at 7:38

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.