Intuitionistic Logic

Finite Satisfiability Gap#

See Degree of Classicality for more.

Definition. Given a first-order language \(\mathcal{L}\) and a finite \(\mathcal{L}\)-structure \(M\), and an \(\mathcal{L}\)-formula \(\phi(x_1,\ldots,x_n)\) with arity \(n\). The degree of satisfiability \(\mathsf{ds}_M(\phi)\) of the formula \(\phi\) in the structure \(M\) is the quantity
 

\[\frac{ | \{ (a_1, \dots, a_n) \in M^n \mid \varphi(a_1, \dots, a_n)  \} | }{ | M | ^n }.\]

One says that a formula \(\phi\) has finite satisfiability gap \(\epsilon\) for \(\phi\in (0,1)\) if for all \(M\) either \(\mathsf{ds}_M(\phi = 1)\) or \(\mathsf{ds}_M(\phi) \leq 1-\epsilon\) (here we can vary \(M\)).

Now the following results are standard:

1. A propositional formula \(\phi\) is provable in classical logic precisely if for every Boolean algebra \(B\), one has \(B\vDash (\phi = \top)\).
2. A propositional formula \(\phi\) is provable in intuitionistic logic precisely if for every Heyting algebra \(H\), one has \(H\vDash (\phi = \top)\).

A result is:

Theorem. For any Heyting algebra \(H\), either \(H\) is Boolean, or one has that \(\mathsf{ds}_H(x\vee \neg x = \top)\leq 2/3\).

This means that if tertium non datur is not universally true in a Heyting algebra, then it is false for at least \(⅔\) of the choice of elements.

Curiously, the double negation elimination \(\neg\neg x = x\) does not have a finite satisfiability gap. 

1. In intuitionistic logic we can prove that \((x\vee \neg x)\to (\neg \neg x \to x)\), but cannot prove the converse \((\neg \neg p \to p)\to (p\vee\neg p)\), only \((\neg \neg p \to p)\to \neg\neg(\neg\neg p\vee\neg p)\).