A consistent prepositional logic without any finite models

Some propositional logics (e.g. the classical system) can be characterized by a finite model, while others (e.g. Heyting's) which have the finite model property (FMP) can be characterized by an infinite set of finite models. Still others (e.g. certain extensions of Heyting's logic) which lack the FMP can only be characterized by a set of models, at least one of which is infinite. Yet all these logics admit finite models even though they may not be characterized by them. (For example, they all admit the 2-element Boolean algebra as a model in the sense that all their theorems are valid on that algebra when the propositional connectives are interpreted in the usual manner.) The object of the present paper is to give a (not too artificial) example of a propositional logic which is consistent and which admits only infinite models. It therefore lacks the FMP in a very strong sense. Such a propositional logic, I shall call hyperinfinite. The existence of hyperinfinite logics was already plausible from a result in abstract algebra which says that there are varieties of algebras of which the only finite element is the trivial algebra (see [3]).I wish to thank Professor A. S. Troelstra, Amsterdam, for comments on an early version of this paper. The constructive criticism of two anonymous referees has also been useful.The hyperinfinite propositional logic to be described is obtained from Positive Logic—the negative-free part of Heyting's logic—by adjoining certain axioms which govern the use of a unary modal connective.