  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.
