Finite semantics for fragments of intuitionistic logic

TL;DR

This paper investigates whether finite semantics can be established for various fragments of intuitionistic logic, providing insights into their logical structure with minimal algebraic prerequisites.

Contribution

It systematically examines all fragments of intuitionistic logic to determine the existence of finite semantics, filling a gap in the understanding of their logical properties.

Findings

Some fragments admit finite semantics

Most fragments do not admit finite semantics

Provides a comprehensive classification of fragments

Abstract

In 1932, G\"odel proved that there is no finite semantics for intuitionistic logic. We consider all fragments of intuitionistic logic and check in each case whether a finite semantics exists. We may fulfill a didactic goal, as little logic and algebra are presupposed.

Equations

$$\phi \dot{\vee }\psi =(\phi \to \psi )\to \psi .$$

$$([([(p_3\to p_2)\to (p_3\to p_1)]\to (p_3\to p_1))\to (p_2\to p_1)]\to (p_2\to p_1)).$$

$$(p_3\to p_2)\to (p_3\to p_1)\to (p_3\to p_1)\to (p_2\to p_1)\to (p_2\to p_1).$$

$${\alpha }_n=\underset{1\le i<j\le n+1}{\text{∨˙}}{p}_j\to p_i.$$

$$\text{(C) }\Gamma {⊢}_F\phi \text{iff}\Gamma {\models }_{{\mathfrak{A}}_F,D}\phi .$$

$$\bar{w}({\alpha }_n)$$

$$=\underset{1\le i<j\le n+1}{\text{∨˙}}\bar{w}{p}_i,\text{(as}\bar{w}{p}_i<w{p}_j\text{, using Lemma refLid(i)),}$$

$$=\bar{w}{p}_1\dot{\vee }\bar{w}{p}_1\dot{\vee }\cdots \dot{\vee }w{p}_2\dot{\vee }w{p}_2\cdots \dot{\vee }w{p}_n,$$

$$=\bar{w}{p}_1\dot{\vee }\bar{w}{p}_2\dot{\vee }\cdots \dot{\vee }w{p}_n\text{, (by Lemma refLid(ii)),}$$

$$=\bar{w}{p}_n\text{, (by Lemma refLid(ii)),}$$

$$=n,$$

$$\ne n+1.$$

$${\alpha }_n=\underset{1\le i<j\le n+1}{\bigvee }\neg \neg (\neg p_i\vee p_j).$$

$$\text{(C) }\Gamma {⊢}_F\phi \text{iff}\Gamma {\models }_{{\mathfrak{A}}_F,D}\phi .$$

Full text

1 Introduction

As is well known, classical logic has a finite semantics. In the beginning of the twenties of the twentieth century, mathematicians like Kolmogorov, Glivenko, and Heyting began to study intuitionistic logic, at that time sometimes called “the logic of M. Brouwer” (see [12], [4], and [10], respectively). The natural question arises whether also intuitionistic logic has a finite semantics. In 1932, Gödel proved that there is no finite semantics for intuitionistic logic. In his words, he wrote that intuitionistic logic has no Realisierung mit endlich vielen Elementen (see [6]). In fact, Gödel’s argument also holds for positive logic, that is, the conjunction-disjunction-conditional fragment of intuitionistic logic. That is, there is no finite semantics for the mentioned fragment. Shortly afterwards, in 1933, Gödel himself proved that the conjunction-negation fragments of intuitionistic and classical logic coincide (see [7]). This implies that the conjunction-negation fragment of intuitionistic logic does have a finite semantics. However, Gödel result does not hold when also considering premisses (just note that the Double Negation Law holds in classical logic, but not in intuitionistic logic). In particular, in this note we will want to know whether the conjunction-negation fragment has a finite semantics also when having premisses. In general, it is also natural to ask the same question regarding every fragment of intuitionistic logic, including the fragment with no connectives, which will be notated $\varnothing$. This we do in the present note. All fragments appear pictorially in Figure 1.

The set $\mathfrak{F}$ of formulas is obtained in the usual way from the set of (propositional) letters $\Pi$, applying the connectives $\land,\lor,\to$, and $\neg$. Any subset of the connectives will be called a fragment (of intuitionistic logic). Let $F$ be a fragment. Then, $\mathfrak{F}_{F}$ denotes the formulas where only the connectives in $F$ are applied. Note that in intuitionistic logic the given connectives are independent.

As regards syntactic matters, it is possible to use the corresponding axioms of the Frege-style axiomatization of intuitionistic logic in the case of fragments with the conditional. For one version of the mentioned axiomatization see [2, Section 11.1]. In the case of fragments without the conditional, it is possible to use Gentzen’s Natural Deduction. However, as we do not have $\perp$, we need to use something like the following two rules in the case of negation, for introduction and elimination, respectively,

[$\mathfrak{A}$]

$\mathfrak{B}$

     

[$\mathfrak{A}$]

$\mathfrak{\neg B}$

$\mathfrak{\neg A}$

and

$\mathfrak{A}$         $\mathfrak{\neg A}$

.

$\mathfrak{B}$

Gentzen’s Natural Deduction rules for the other connectives may be found in [3, p. 186]. Alternatively, for fragments without the conditional, one may also proceed using the following rules, where $\Gamma\cup\{\varphi\}\subseteq\mathfrak{F}$:

(R∈) If $\varphi\in\Gamma$, then $\Gamma\vdash_{i}\varphi$,

(Rm) If $\Gamma\vdash_{i}\varphi$ then $\Gamma,\psi\vdash_{i}\varphi$ (monotonicity),

(Rt) If $\Gamma\vdash_{i}\varphi$ and $\Delta,\varphi\vdash_{i}\psi$, then $\Gamma,\Delta\vdash_{i}\psi$ (cut rule),

(R∧) $\Gamma\vdash_{i}\varphi\land\psi$ iff $\Gamma\vdash_{i}\varphi$ and $\Gamma\vdash_{i}\varphi$,

(R∨) $\Gamma,\varphi\lor\psi\vdash_{i}\chi$ iff $\Gamma,\varphi\vdash_{i}\chi$ and $\Gamma,\psi\vdash_{i}\chi$,

(R→) $\Gamma\vdash_{i}\varphi\to\psi$ iff $\Gamma,\varphi\vdash_{i}\psi$,

(R*¬I*) If $\Gamma,\varphi\vdash_{i}\psi$ and $\Gamma,\varphi\vdash_{i}\neg\psi$, then $\Gamma\vdash_{i}\neg\varphi$,

(R*¬E*) If $\Gamma\vdash_{i}\varphi$ and $\Gamma\vdash_{i}\neg\varphi$, then $\Gamma\vdash_{i}\psi$.

When we write $\vdash_{F}$, for $F$ a fragment, we mean that only the rules of the connectives in $F$ are applied.

Now , let us define semantic consequence for a given algebra.

Definition 1**.**

Let $F$ be a fragment, let $\Gamma\cup\{\varphi\}\subseteq\mathfrak{F}_{F}$, let $\mathfrak{A}_{F}$ be an algebra with universe $V$ and an operation for every connective in $F$, and let $D\subseteq V$. Then, we say that $\varphi$ is a semantic consequence of $\Gamma$ in $\mathfrak{A}_{F}$ with $D$ (and use the notation $\Gamma\vDash_{\mathfrak{A}_{F},D}\varphi$) iff for every assingment $v:\Pi\to V$, the unique homomorphism $\bar{v}:\mathfrak{F}_{F}\to V$, satisfies that if $\bar{v}\psi\in D$, for all $\psi\in\Gamma$, then $\bar{v}\varphi\in D$.

We will use the same symbols for both the connectives and the corresponding algebraic operations. This ambiguity should not cause any problem.

Under “having a finite semantics” we will understand the same as Gödel, that is, we will use the following definition.

Definition 2**.**

The fragment $F$ has a finite semantics iff there exists an algebra $\mathfrak{A}_{F}$ with finite universe $V$ and $D\subseteq V$ such that for every $\Gamma\cup\{\varphi\}\in\mathfrak{F}_{F}$ it holds that $\Gamma\vdash_{F}\varphi$ iff $\Gamma\vDash_{\mathfrak{A}_{F},D}\varphi$.

It should be clear that, for each fragment, we will be looking for one algebra (not for a class of algebras) and, moreover, for a finite one.

In Section 2, we will use Gödel’s argument in order to prove that any fragment having the conditional, in particular positive and intuitionistic logics, do not have a finite semantics. There will only be eight fragments left to consider.

In Section 3, we will see that the conjunction-disjunction fragments and the fragments contained in it, do have a finite semantics.

In Section 4, we will consider the case of the disjunction-negation fragment.

Funally, in Section 5, we consider the negation and conjunction-negation fragments.

When referring to the conditional fragment, we will say $\{\to\}$-fragment. Analogously, in the case of other fragments.

We think this note may fulfill a didactic goal, as little knowledge of logic and algebra are presupposed.

2 Fragments with the conditional

Lemma 1**.**

Let $F$ be a fragment with $\to$. Then, (i) $\varphi\vdash_{F}\varphi$, (ii) $\vdash_{F}\varphi\to\varphi$, and (iii) $\varphi,\varphi\to\psi\vdash_{F}\psi$ (modus ponens).

Proof.

(i) follows just using (R∈) and (ii) follows from (i) using (R→). In order to prove (iii), use (i) to obtain $\varphi\to\psi\vdash_{F}\varphi\to\psi$ and then apply (R→) with $\Gamma=\{\varphi\to\psi\}$. ∎

In what follows we will use Gödel’s argument with formulas of a different form. In order to do that, we will use the following abbreviation:

[TABLE]

For example, the formula $[(p_{3}\to p_{2})\dot{\vee}(p_{3}\to p_{1})]\dot{\vee}(p_{2}\to p_{1})$ denotes the formula

[TABLE]

Note that $\dot{\vee}$ is neither commutative nor associative. We will omit parentheses supposing associativity to the left. So, instead of the given formula, we may as well write

[TABLE]

We will use the following lemma.

Lemma 2**.**

Let $F$ be a fragment with $\to$ and $\varphi\in\mathfrak{F}_{F}$ such that $\vdash_{F}\varphi$. Then (i) $\vdash_{F}\varphi\dot{\vee}\psi$, (ii) $\vdash_{F}\psi\dot{\vee}\varphi$, for any formula $\psi\in\mathfrak{F}_{F}$, and (iii) If $\psi=\cdots\dot{\lor}\ \varphi\ \dot{\lor}\cdots$, where the given dots may be empty at the beginning or the end, then $\vdash_{F}\psi$.

Proof.

(i) By (mp) we have $\varphi,\varphi\to\psi\vdash_{F}\psi$. Then, using (R→), it follows that $\varphi\vdash_{F}(\varphi\to\psi)\to\psi$. As we have $\vdash_{F}\varphi$, using the cut rule it follows that $\vdash_{F}(\varphi\to\psi)\to\psi$. (ii) As we have $\vdash_{F}\varphi$, by (Rm) it follows that $\psi\to\varphi\vdash_{F}\varphi$. Then, by (R→) it follows that $\vdash_{F}(\psi\to\varphi)\to\varphi$. Part (iii) follows using (i) and (ii). ∎

We will also use the following algebraic facts, using the $\dot{\vee}$ notation in a way analogous to the logical case.

Lemma 3**.**

Let $\mathbf{A}$ be a Heyting algebra with universe $A$. Let $a,b\in A$. Then, (i) If $\mathbf{A}$ is a chain and $a<b$, then $b\to a=a$ and (ii) if $a\leq b$, then $a\dot{\lor}b=b$.

Proof.

(i) It is clear that (1) $b\wedge a\leq a$. Now, let us suppose that $b\wedge c\leq a$, for any $c\in A$. Then, as $A$ is a chain, then either $b\wedge c=b$ or $b\wedge c=c$. Now, as $a<b$, it cannot be the case that $b\wedge c=b$. So, $b\wedge c=c$. Then $c\leq a$. So, we have that, (2) for any $c\in A$, if $b\wedge c\leq a$, then $c\leq a$. From (1) and (2) it follows that $b\to a=a$.

(ii) Let us suppose that $a\leq b$. So, $a\to b$ is top. So, $(a\to b)\to b\leq b$. It is also the case that $b\leq(a\to b)\to b$. ∎

Next come two propositions.

Proposition 1**.**

Let $F$ be a fragment with $\to$ such that $F$ has a finite semantics, say with $n\geq 1$ values. Then, the formulas of the following form are derivable in $F$:

[TABLE]

Proof.

Let us suppose that $F$ is a fragment with $\to$ that has a semantics with $n$ values, that is, there exists an algebra with universe $|V|=n$ and $D\subseteq V$ such that for every $\Gamma\cup\{\varphi\}\in\mathfrak{F}_{F}$ it holds that

[TABLE]

Let us take a valuation $w:\mathfrak{F}_{F}\to V$ and let us consider $w(\alpha_{n})$. As there are $n+1$ propositional letters in $\alpha_{n}$, but only $n$ values, there must be letters $p_{i}$, $p_{j}$ such that $w(p_{i})=w(p_{j})$. Now, let us consider the formula $\beta_{n}=\alpha_{n}[p_{i}/p_{j}]$. It should be clear that $w(\beta_{n})=w(\alpha_{n})$. Now, $\beta_{n}=\cdots\dot{\lor}(p_{j}\to p_{j})\dot{\lor}\cdots$, where the given dots may be empty at the beginning or the end. Now, using Lemma 1 (ii), it holds that $\vdash_{F}p_{j}\to p_{j}$ and then, using Lemma 2 (iii), $\vdash_{F}\beta_{n}$. Then, by (C), $\vDash_{\mathfrak{A}_{F},D}\beta_{n}$. So, $\vDash_{\mathfrak{A}_{F},D}\alpha_{n}$. So, using (C) in the other direction, $\vdash_{F}\alpha_{n}$. ∎

Proposition 2**.**

Let $\alpha_{n}$ be a formula as in Proposition 1. Then, $\nvdash_{i}\alpha_{n}$, for any natural number $n\geq 1$.

Proof.

Let us consider the $n+1$-element chain of the first $n+1$ natural numbers with the usual order. Defining meet, join, relative meet complement and meet complement as usual, the given chain is a Heyting algebra. Let us consider any assignment $w$ such that $w(p_{i})=i$, for $1\leq i\leq n+1$. Then,

[TABLE]

Using soundness, it follows that $\nvdash_{i}\alpha_{n}$. ∎

Theorem 1**.**

Fragments containing $\to$ do not have a finite semantics.

Proof.

Applying Proposition 1, the formulas $\alpha_{n}$ would be derivable in the fragment, which cannot be the case, as by Proposition 2, $\nvdash_{i}\alpha_{n}$. ∎

3 Subfragments of $\{\land,\lor\}$

Due to the results of the previous section, the remaining fragments to be considered are the ones appearing in Figure 2.

In this section, $\mathbf{2}$ stands for any algebra of the form $\langle\{0,1\};F\rangle$, where $F\subseteq\{\wedge,\vee\}$ and $\land$ and $\lor$ stand for the usual meet and join in a lattice or semilattice. In all cases, $D=\{1\}$. It will be clear in the context which is the relevant $F$, which may be the empty set.

Proposition 3**.**

Let $\Gamma\cup\{\varphi\}\subseteq\mathfrak{F}_{\{\land\}}$. Then, $\Gamma\vdash_{\{\land\}}\varphi$ iff $\Gamma\vDash_{\mathbf{2}}\varphi$.

Proof.

If $\Gamma\vdash_{\{\land\}}\varphi$, then $\Gamma\vdash_{i}\varphi$. Using soundness of intuitionistic logic, it follows that $\Gamma\vDash_{\mathbf{2}}\varphi$. On the other hand, suppose $\Gamma\nvdash_{\{\land\}}\varphi$, that is, $\Gamma\nvdash_{\{\land\}}p_{1}\land p_{2}\land\cdots\land p_{n}$. Then, by (R∧), there is a letter $p_{i}$ such that $\Gamma\nvdash_{\{\land\}}p_{i}$. So, again by (R∧), $p_{i}$ is not a subformula of any formula in $\Gamma$. Then, there exists the valuation $w$ such that $wp_{i}=0$ and $wp=1$ for letters $p$ other that $p_{i}$. So, $\Gamma\nvDash_{\mathbf{2}}\varphi$. ∎

Corollary 1**.**

Let $\Gamma\cup\{\varphi\}\subseteq\mathfrak{F}_{\varnothing}$. Then, $\Gamma\vdash_{\varnothing}\varphi$ iff $\Gamma\models_{\mathbf{2}}\varphi$.

Proposition 4**.**

Let $\Gamma\cup\{\varphi\}\subseteq\mathfrak{F}_{\{\land,\lor\}}$. Then, $\Gamma\vdash_{\{\land,\lor\}}\varphi$ iff $\Gamma\vDash_{\mathbf{2}}\varphi$.

Proof.

If $\Gamma\vdash_{\{\land,\lor\}}\varphi$, then $\Gamma\vdash_{i}\varphi$. Using soundness of intuitionistic logic, it follows that $\Gamma\vDash_{\mathbf{2}}\varphi$. On the other hand, suppose $\Gamma\nvdash_{\{\land,\lor\}}\varphi$. Then using the conjunctive normal form theorem, it follows that $\varphi$ and every formula in $\Gamma$ may be seen as a conjunction of disjunction of letters. Then, by (R∧), $\Gamma\nvdash_{\{\land,\lor\}}\chi$, where $\chi=q_{1}\lor\cdots\lor q_{n}$. Also, as every formula in $\Gamma$ is a conjunction (of disjunctions), and to have formulas $\alpha$ and $\beta$ as different premisses is equivalent to having $\alpha\land\beta$ as only premiss, then we might as well consider $\Gamma$ to be a set of disjunctions and call it $\Delta$. Now, by (R∨), it follows that every disjunction in $\Delta$ has a letter that does not belong to the set $\{q_{1},\dots q_{n}\}$. Consequently, there exists the valuation $w$ such that $wq_{i}=0$, for all $1\leq i\leq n$ and $wp=1$ for letters $p$ other than the $q_{i}$. So, every formula in $\Delta$ will have value $1$. So, $\Gamma\nvDash_{2}\varphi$. ∎

Corollary 2**.**

Let $\Gamma\cup\{\varphi\}\subseteq\mathfrak{F}_{\{\lor\}}$. Then, $\Gamma\vdash_{\{\lor\}}\varphi$ iff $\Gamma\vDash_{\mathbf{2}}\varphi$.

Proof.

The proof for the fragment $\{\land,\lor\}$ was reduced to having only disjunctions. ∎

4 The disjunction-negation fragment

Due to the results of the previous sections, the remaining fragments to be considered are the ones appearing in Figure 3.

We will use the following lemmas.

Lemma 4**.**

Let $F$ be a fragment with $\lor$. Then, $\varphi\vdash_{F}\varphi\lor\psi$ and $\psi\vdash_{F}\varphi\lor\psi$.

Proof.

Using (R∈), we get $\varphi\vee\psi\vdash_{F}\varphi\vee\psi$. Then, using (R∨) with $\Gamma=\varnothing$, we get both $\varphi\vdash_{F}\varphi\lor\psi$ and $\psi\vdash_{F}\varphi\lor\psi$. ∎

Lemma 5**.**

Let $F$ be a fragment with $\lor$ and $\neg$. Then, (i) if $\varphi\vdash_{F}\psi$, then $\neg\psi\vdash_{F}\neg\varphi$ and (ii) $\vdash_{F}\neg\neg(\varphi\vee\neg\varphi)$.

Proof.

(i) Suppose $\varphi\vdash_{F}\psi$. Then, by monotonicity, we have $\varphi,\neg\psi\vdash_{F}\psi$. By (R∈) we also have $\varphi,\neg\psi\vdash_{F}\neg\psi$. Then, using (R*¬I*), it follows that $\neg\psi\vdash_{F}\neg\varphi$. (ii) Using Lemma 4, we have $\varphi\vdash_{F}\varphi\vee\neg\varphi$. Then, by part (i), $\neg(\varphi\vee\neg\varphi)\vdash_{F}\neg\varphi$. Using Lemma 4 again, we have $\neg\varphi\vdash_{F}\varphi\vee\neg\varphi$. So, using the cut rule, $\neg(\varphi\vee\neg\varphi)\vdash_{F}\varphi\vee\neg\varphi$. Now, by (R∈), we also have $\neg(\varphi\vee\neg\varphi)\vdash_{F}\neg(\varphi\vee\neg\varphi)$. Finally, using (R*¬I*), we get $\vdash_{F}\neg\neg(\varphi\vee\neg\varphi)$. ∎

Remark 1**.**

Recall that Tertium non datur does not hold in intuitionistic logic. However, as seen in part (ii) of the last Lemma, its double negation holds in any fragment with $\vee$ and $\neg$.

On the other hand, intuitionistic logic enjoys the Disjunction Property, which does not hold for classical logic.

Lemma 6**.**

Let $\varphi,\psi\in\mathfrak{F}$. If $\vdash_{i}\varphi\vee\psi$, then $\vdash_{i}\varphi$ or $\vdash_{i}\psi$.

Proof.

An algebraic proof runs as follows. If neither $\vdash_{i}\varphi$ nor $\vdash_{i}\psi$ hold, then there are Heyting algebras $\mathbf{H_{1}}$, $\mathbf{H_{2}}$ and valuations $v_{1}$, $v_{2}$ such that $v_{1}\varphi\neq 1_{\mathbf{H_{1}}}$ and $v_{2}\psi\neq 1_{\mathbf{H_{2}}}$. Now, take the direct product $\mathbf{H_{1}}\times\mathbf{H_{2}}$ and add an element which is greater than any element of the universe of the given product. Then, the resulting algebra with the natural valuation will prove that it is not the case that $\vdash_{i}\varphi\vee\psi$. For details, the reader may see [13]. For other proofs, see [14, Exercise 2.6.7 or sections 5.6 to 5.10]. ∎

Proposition 5**.**

Let $F$ be such that {$\lor,\neg\}\subseteq F$. Let us suppose that $F$ has a finite semantics, say with $n\geq 1$ values. Then, the formulas of the following form are derivable in $F$:

[TABLE]

Proof.

Let us suppose that $F$ is a fragment with $\lor$ and $\neg$ that has a semantics with $n$ values, that is, there exists an algebra with universe $V$ such that $|V|=n$ and $D\subseteq V$ such that for every $\Gamma\cup\{\varphi\}\in\mathfrak{F}_{F}$ it holds that

[TABLE]

Let us take a valuation $w:\mathfrak{F}_{F}\to V$ and let us consider $w(\alpha_{n})$. As there are $n+1$ propositional letters in $\alpha_{n}$, but only $n$ values, there must be letters $p_{i}$, $p_{j}$ such that $w(p_{i})=w(p_{j})$. Now, let us consider the formula $\beta_{n}=\alpha_{n}[p_{i}/p_{j}]$. It should be clear that $w(\beta_{n})=w(\alpha_{n})$. Now, it holds that $\vdash_{F}\neg\neg(\neg p_{j}\lor p_{j})$. Consequently, $\vdash_{F}\beta_{n}$. Then, by (C), $\vDash_{\mathfrak{A}_{F},D}\beta_{n}$. So, $\vDash_{\mathfrak{A}_{F},D}\alpha_{n}$. So, using (C) in the other direction, $\vdash_{F}\alpha_{n}$. ∎

Proposition 6**.**

The formulas of the form given in Proposition 5 are not intuitionistically derivable.

Proof.

For every $i$, $j$, $i\neq j$, $\neg\neg(\neg p_{i}\lor p_{j})$ is not even classically derivable. So, by Lemma 6, it follows that $\nvdash_{i}\alpha_{n}$. ∎

Theorem 2**.**

Fragments containing $\lor$ and $\neg$ do not have a finite semantics.

Proof.

Applying Proposition 5, the formulas of the given form would be derivable in the fragment, which cannot be the case, as they are not intuitionistically derivable, as stated in Proposition 6. ∎

5 The negation and conjunction-negation fragments

We only need to consider fragments $\{\neg\}$ and $\{\land,\neg\}$. In the Introduction we stated that Gödel proved that the set of derivable formulas of the conjunction-negation fragment of intuitionistic logic coincides with the set of classically derivable formulas. This is also stated and proved in detail in [11] (see Corollary to (a2) in p. 493). This implies that the conjunction-negation fragment has a finite semantics with respect to derivable formulas, that is, two-valued classical semantics. The natural question arises whether we also have a finite semantics when having premisses as well. This we solve in this section.

As regards syntactics, in this section we will use the following version of the celebrated Glivenko Theorem and also the given Corollary. Glivenko Theorem was originally proved for intuitionistic logic in [5]. Before stating those facts, we say that a set of formulas $\Gamma\in\mathfrak{F_{\land,\neg}}$ is classically (respectively $\{\land,\neg\}$-) consistent iff from $\Gamma$ we may not arrive to a contradiction in classical logic (respectively in the $\{\land,\neg\}$-fragment of intuitionistic logic), where by a contradiction we mean a pair $\varphi,\neg\varphi$ of formulas.

Theorem 3**.**

Let $\Gamma\cup\{\varphi\}\subseteq\mathfrak{F_{\land,\neg}}$. Then, if $\Gamma\vdash_{c}\neg\varphi$, then $\Gamma\vdash_{\{\land,\neg\}}\neg\varphi$.

Corollary 3**.**

Let $\Gamma\subseteq\mathfrak{F_{\land,\neg}}$. If $\Gamma$ is $\{\land,\neg\}$-consistent, then $\Gamma$ is classically consistent.

Regarding semantics, we will use the concepts of subalgabra and congruence, which we now state (for details or examples the reader may see [1]).

Definition 3**.**

Given two algebras $\mathbf{A}$ and $\mathbf{B}$ of the same type, we say that $\mathbf{B}$ is a subalgebra of $\mathbf{A}$ iff the universe of $\mathbf{B}$ is included in the universe of $\mathbf{A}$ and every fundamental operation of $\mathbf{B}$ is the restriction to the universe of $\mathbf{B}$ of the corresponding operation of $\mathbf{A}$.

Definition 4**.**

Given an algebra $\mathbf{A}=\langle A;F\rangle$, a congruence on $\mathbf{A}$ is an equivalence relation $E$ on $A$ such that for every n-ary operation $f$ in $F$ and elements $a_{i},b_{i}$ in $A$,

if $a_{i}Eb_{i}$, for all $i,1\leq i\leq n$, then $f(a_{1},\dots,a_{n})Ef(b_{1},\dots,b_{n})$.

The diagonal relation and the all relation are the only trivial congruences.

In this section, $\mathbf{3}$ will stand for the algebra $\langle\{0,\,^{1}\!/_{2},1\};F\rangle$, where $F$ is either $\{\wedge,\neg\}$ or $\{\neg\}$. and $\land$ and $\neg$ stand for the usual meet and meet complement in a Heyting algebra (we might as well say that $a\wedge b=$ min $\{a,b\}$, for any $a,b$ in the universe of $\mathbf{3}$, $\neg 0=1$, and $\neg^{1}\!/_{2}=\neg 1=0$). In all cases, $D=\{1\}$. It will be clear in the context which is the relevant $F$. The algebra $\mathbf{3}$ appears in Figure 4 together with the only non-trivial congruence given by the ellipses. Note, also, that $\langle\{0,1\};\wedge,\neg\rangle$, where $\wedge$ and $\neg$ are the usual meet and meet complement, is a subalgebra of $\mathbf{3}$.

Let us now consider the fragment $\{\land,\neg\}$.

Proposition 7**.**

Let $\Gamma\cup\{\varphi\}\subseteq\mathfrak{F}_{\{\land,\neg\}}$. Then, $\Gamma\vdash_{\{\land,\neg\}}\varphi$ iff $\Gamma\vdash_{\bf{3}}\varphi$.

Proof.

If $\Gamma\vdash_{\{\land,\neg\}}\varphi$, then $\Gamma\vdash_{i}\varphi$. Using soundness of intuitionistic logic, it follows that $\Gamma\models_{\bf{3}}\varphi$. On the other hand, suppose $\Gamma\nvdash_{\{\land,\neg\}}\varphi$. There are three cases: (i) $\varphi=\varphi_{1}\land\varphi_{2}\land\cdots\land\varphi_{n}$, where each $\varphi_{i}$ is a either a negation or a letter, (ii) $\varphi=\neg\psi$, for some formula $\psi$, or (iii) $\varphi=p$, for some letter $p$. In case (i), by (R∧), $\Gamma\nvdash_{\{\land,\neg\}}\varphi_{1}\land\varphi_{2}\land\cdots\land\varphi_{n}$ iff there is at least an $i$ such that $\Gamma\nvdash_{\{\land,\neg\}}\varphi_{i}$ such that $\varphi_{i}$ is either a negation or a letter. So, this case reduces to either case (ii) or case (iii). In case (ii), using Theorem 3, we have that $\Gamma\nvdash_{c}\neg\psi$. Then, there is a valuation $v$ in the two element Boolean algebra such that $v\psi=1$ for all $\psi\in\Gamma$ and $v\neg\varphi=0$. Then, as the Boolean algebra of two elements with fundamental operations $\land$ and $\neg$ is a subalgebra of $\mathbf{3}$, it follows, using the same valuation $v$, that $\Gamma\nvDash_{\bf{3}}\varphi$. Finally, case (iii) means that we have $\Gamma\nvdash_{\{\land,\neg\}}p$. Then, $\Gamma$ is $\{\land,\neg\}$-consistent. Then, using Corollary 3, it follows that $\Gamma$ is classically consistent. Then, there exists a assignment $v$ such that in the two-element Boolean algebra we have that $\bar{v}\psi=1$ for all $\psi\in\Gamma$. Now, let us define an assignment $w:\Pi\to\mathbf{3}$ such that $wp_{i}=vp_{i}$, for all $p_{i}\in\Pi$. Then, as the given Boolean algebra is a subalgebra of $\mathbf{3}$, $\bar{w}\psi=1$ for all $\psi\in\Gamma$. If $\bar{w}p=0$, then we are done. In case $\bar{w}p=1$, let us define $w^{\prime}$ like $w$ except for $w^{\prime}p=\,^{1}\!/_{2}$. Now, as $\Gamma\nvdash_{\{\land,\neg\}}p$, then, due to (R∈) and (R∧), $p$ can only appear as subfomula of a formula $\psi$ in $\Gamma$ if it appears in the scope of a negation, and the value of $\psi$ will not change, as $\langle(1,1),(1,^{1}\!/_{2}),(^{1}\!/_{2},^{1}\!/_{2}),(^{1}\!/_{2},1),(0,0)\rangle$ is a congruence relation. ∎

Now we can easily deal with the negation fragment.

Proposition 8**.**

Let $\Gamma\cup\{\varphi\}\subseteq\mathfrak{F}_{\{\neg\}}$. Then, $\Gamma\vdash_{\{\neg\}}\varphi$ iff $\Gamma\models_{\bf{3}}\varphi$.

Proof.

The left to right direction is the same as in the previous proof. For the other direction, just consider cases (ii) and (iii) in the previous proof. ∎

It is clear, then, due to propositions 7 and 8, that the fragments $\{\land,\neg\}$ and $\{\neg\}$ have finite semantics.

A final remark. We have seen that we do not have finite semantics for many fragments of intuitionistic logic. However, the Finite Model Property (FMP) holds for intuitionistic logic (so, also, for any of its fragments). The difference may be understood as the difference between the quantifications $\exists\forall$ and $\forall\exists$, that is, we do not have a finite semantics for all cases. Now, given any particular case that does not hold, we may find a finite interpretation (for example, a Heyting algebra) that proves that it is not the case. The reader interested in a proof of the FMP for intuitionistic logic may see [2, Section 11.9 ].