On the Ja\'skowski Models for Intuitionistic Propositional Logic
R. D. Arthan

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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Multi-Agent Systems and Negotiation · Semantic Web and Ontologies
