Hostname: page-component-78c5997874-mlc7c Total loading time: 0 Render date: 2024-11-05T03:59:29.141Z Has data issue: false hasContentIssue false

On the existence of finite models and decision procedures for propositional calculi

Published online by Cambridge University Press:  24 October 2008

R. Harrop
Affiliation:
King's CollegeNewcastle upon Tyne

Extract

1. Introduction. In this paper we consider certain general properties of propositional calculi. Two forms of the definition of a finite model of such a calculus are discussed, these forms differing in the manner prescribed for the satisfaction of the rules of the calculus. The methods of definition are shown to be equivalent for the application of the finite model method for the demonstration of the unprovability of formulae in the calculus. It is further proved that, although the decidability of a calculus follows from the existence of a finite model counter-example for each unprovable formula of the calculus, the converse result is not true.

Type
Research Article
Copyright
Copyright © Cambridge Philosophical Society 1958

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

(1)Hilbert, D. and Bernays, P.Grundlagen der Mathematik, vol. I (Berlin, 1934).Google Scholar
(2)Linial, S. and Post, E. L.Recursive unsolvability of the deducibility Tarski's completeness and independence of axioms problems of propositional calculus. Bull. Amer. Math. Soc. 55 (1949), 50.Google Scholar
(3)McKinsey, J. C. C.A solution of the decision problem for the Lewis systems S2 and S4 with an application to topology. J. Symbolic Logic, 6 (1941), 117–34.CrossRefGoogle Scholar
(4)Rosenbloom, P. C.Elements of mathematical logic (New York, 1950).Google Scholar