The finite model property and recursive bounds on the size of countermodels (Q1063587)

\textit{R. Harrop} [J. Symb. Logic 30, 271-292 (1965; Zbl 0188.314)] asked whether every finitely axiomatized propositional calculus L which has the finite model property (i.e. every nontheorem is refutable in a finite model) also has the following property: There exists a recursive function f such that for each wff \(\alpha\), \(\vdash_ L\alpha\) if and only if \(\alpha\) is valid in each finite model of L with at most f(\(| \alpha |)\) elements. The author [''Answer to a question raised by Harrop'', Bull. Sect. Logic, Pol. Acad. Sci. 11, 140-141 (1982)] showed that Harrop's question has an affirmative answer. In this paper he extends that result to the case in which L has a recursively enumerable set of theorems. He also constructs an L with the finite model property which does not have Harrop's property.