On the Ja\'skowski Models for Intuitionistic Propositional Logic

TL;DR

This paper revisits Jaśkowski's construction of finite Heyting algebras, providing a modern proof of their role in intuitionistic propositional logic and outlining a decision procedure for IPL.

Contribution

It offers a clear, modern proof of Jaśkowski's result using a normal form similar to his original, and establishes a semantic property enabling an alternative completeness proof.

Findings

Proof of Jaśkowski's result using modern terminology

Semantic property of the normal form for IPL

Outline of a decision procedure for IPL

Abstract

In 1936, Stanislaw Ja\'skowski gave a construction of an interesting sequence of what he called "matrices", which we would today call "finite Heyting Algebras". He then gave a very brief sketch of a proof that if a propositional formula holds in each of these algebras then it is provable in intuitionistic propositional logic (IPL). The sketch just describes a certain normal form for propositional formulas and gives a very terse outline of an inductive argument showing that an unprovable formula in the normal form can be refuted in one of the algebras. Unfortunately, it is far from clear how to recover a complete proof from this sketch. In the early 1950s, Gene F. Rose gave a detailed proof of Ja\'skowski's result, still using the notion of matrix rather than Heyting algebra, based on a normal form that is more restrictive than the one that Ja\'skowski proposed. However, Rose's paper refers to his thesis for additional details, particularly concerning the normal form. This note gives a proof of Ja\'skowski's result using modern terminology and a normal form more like Ja\'skowski's. We also prove a semantic property of the normal form enabling us to give an alternative proof of completeness of IPL for the Heyting algebra semantics. We outline a decision procedure for IPL based on our proofs and illustrate it in action on some simple examples.