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

DOI10.1215/00294527-2022-0034zbMATH Open1522.03063arXiv2112.04436OpenAlexW4360612162MaRDI QIDQ6100982FDOQ6100982

Authors: Antti Valmari, Lauri Hella 

Publication date: 31 May 2023

Published in: Notre Dame Journal of Formal Logic (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/2112.04436

Recommendations

• scientific article; zbMATH DE number 4035828
• scientific article; zbMATH DE number 3931008
• An intuitionistic completeness theorem for classical predicate logic
• A completeness theorem for continuous predicate modal logic
• Some Completeness Results for Propositional Conditional Logics
• The completeness of a predicate-functor logic
• A logic for propositions with indefinite truth values
• Completeness theory for propositional logics
• scientific article; zbMATH DE number 2196603
• A proof of the standard completeness for the involutive uninorm logic

zbMATH Keywords

completenesspredicate logicKleene's three-valued logicpartial functionsundefined truth value

Mathematics Subject Classification ID

Many-valued logic (03B50)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• The completeness of the first-order functional calculus
• A typed logic of partial functions reconstructed classically
• Computer science today. Recent trends and developments
• On all strong Kleene generalizations of classical logic
• A logic covering undefinedness in program proofs
• Problems in between words and abelian words: \(k\)-abelian avoidability
• Adapting Calculational Logic to the Undefined
• A first order logic for partial functions
• A set theory with support for partial functions
• A practical approach to partial functions in CVC Lite
• Efficient Well-Definedness Checking
• A fully logical inductive logic
• Strict Fregean free logic
• A more unified approach to free logics
• Title not available (Why is that?)
• Title not available (Why is that?)
• Natural deduction for three-valued regular logics
• Title not available (Why is that?)
• A system of logic for partial functions under existence-dependent kleene equality
• Theorem proving for classical logic with partial functions by reduction to Kleene logic
• Title not available (Why is that?)

Cited In (3)

• A simple Henkin-style completeness proof for Gödel 3-valued logic G3
• A logic covering undefinedness in program proofs
• Title not available (Why is that?)

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)