An unsolvable problem concerning implicational calculi.
Ralph Calvin Applebee, Biswambhar Pahi · Notre Dame Journal of Formal Logic · 1970
Propositional calculi are assumed to be defined as in Harrop [2].A propositional calculus is called implicational if it has exactly one connective and that a binary one.Algebraic structures called finite models of a propositional calculus P in Harrop [2] will be called here finite rulemodels of P.An algebraic structure of the appropriate kind is called a model of P if every theorem of P is valid in it.We note that every finite rule-model of P is a finite model of P, but the converse need not hold.It is proved in Harrop [2] (lemma 3.1, pp.5-6) that there is an effective method for deciding whether or not a finite algebraic structure is a finite rule-model of a propositional calculus P. We prove here the following: