Intuitionistic First-Order Logic

Definition

Intuitionistic First-Order Logic (IFOL) is the restriction of first-order logic (FOL) to constructive rules, removing the Law of the Excluded Middle ($P\vee \neg P$) and Double Negation Elimination ($\neg \neg P\to P$). It aligns with the Brouwer-Heyting-Kolmogorov (BHK) interpretation, where truth is equated with the existence of a proof/construction.

Semantics

Unlike the Boolean semantics of FOL (truth values in $\{0,1\}$), IFOL semantics are topological or algebraic.

Kripke Semantics

Algebraic Semantics

Truth values form a Heyting Algebra, a bounded Lattice where $x\wedge a\le b⟺x\le (a\to b)$. The complement is pseudo-complementation: $\neg a=(a\to 0)$.

Metatheoretic Divergences

Completeness

• Classical Meta-theory: IFOL is sound and complete with respect to Kripke semantics (Kripke 1965).
• Constructive Meta-theory: Completeness is unprovable. Kreisel (1962) showed that “IFOL is complete for its intended semantics” implies a weak form of excluded middle (Dyson-Kreisel) in the meta-theory.

Structural Properties

IFOL exhibits constructive witnesses, which FOL lacks:

1. Disjunction Property (DP): If $⊢\varphi \vee \psi$, then $⊢\varphi$ or $⊢\psi$ (for closed formulas).
2. Existence Property (EP): If $⊢\exists x.\varphi (x)$, then there exists a term $t$ such that $⊢\varphi (t)$.

Independence of Connectives

In FOL, sets like $\{\neg ,\to \}$ are functionally complete. In IFOL, logical connectives are independent:

• $\exists$ cannot be defined as $\neg \forall \neg$.
• $\vee$ cannot be defined as $\neg (\neg \cdot \wedge \neg \cdot )$.
• All connectives $\{\perp ,\wedge ,\vee ,\to ,\forall ,\exists \}$ must be taken as primitive.

Decidability

While full FOL is undecidable, restrictions behave differently in IFOL:

• Monadic Predicate Logic: Decidable in FOL; undecidable in IFOL (Kripke 1965).
• Propositional Logic: PSPACE-complete (Statman 1979) vs co-NP complete for Classical.

Invalid Principles

The following are classically valid but intuitionistically invalid:

• Law of Excluded Middle: $\forall P,P\vee \neg P$
• Double Negation Elimination: $\forall P,\neg \neg P\to P$
• Peirce’s Law: $((P\to Q)\to P)\to P$
• Drinker Paradox: $\exists x(P(x)\to \forall yP(y))$
• De Morgan’s Law (one direction): $\neg (A\wedge B)\to \neg A\vee \neg B$
• Definability of $\exists$ from $\forall$: $\neg \forall x\neg P(x)\to \exists xP(x)$

Relation to FOL

• Double Negation Translation (Gödel-Gentzen): FOL can be embedded into IFOL. If $\Gamma {⊢}_C\varphi$, then ${\Gamma }^{gg}{⊢}_I{\varphi }^{gg}$. Classical logic is viewed as a “sub-logic” of intuitionistic logic via this embedding (regarding information content).