A completeness proof for a regular predicate logic with undefined truth value

Abstract: We provide a sound and complete proof system for an extension of Kleene's ternary logic to predicates. The concept of theory is extended with, for each function symbol, a formula that specifies when the function is defined. The notion of "is defined" is extended to terms and formulas via a straightforward recursive algorithm. The "is defined" formulas are constructed so that they themselves are always defined. The completeness proof relies on the Henkin construction. For each formula, precisely one of the formula, its negation, and the negation of its "is defined" formula is true on the constructed model. Many other ternary logics in the literature can be reduced to ours. Partial functions are ubiquitous in computer science and even in (in)equation solving at schools. Our work was motivated by an attempt to explain, precisely in terms of logic, typical informal methods of reasoning in such applications.

Review text

The authors develop semantics for an extension of \textit{S. C. Kleene}'s three-valued logic (see [J. Symb. Log. 3, 150--155 (1938; Zbl 0020.33803; JFM 64.0932.03); Introduction to metamathematics. Amsterdam: North-Holland Publishing Co.; Groningen: P. Noordhoff N. V. (1952; Zbl 0047.00703)]) to first-order predicate language. They prove soundness and completeness theorem, followed by a very good motivation. The completeness proof is based on traditional \textit{L. Henkin}'s construction [J. Symb. Log. 14, 159--166 (1949; Zbl 0034.00602)]. It seems that this approach can be applied to many other three-valued logics.

Recommendations

Cites work

Cited in

(4)

This page was built for publication: A completeness proof for a regular predicate logic with undefined truth value

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6100982)