A Completeness Proof for a Regular Predicate Logic with Undefined Truth Value

Antti Valmari, Lauri Hella

Tutkimustuotos: ArtikkeliScientificvertaisarvioitu

Abstrakti

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 precisely explain, in terms of logic, typical informal methods of reasoning in such applications.

AlkuperäiskieliEnglanti
Sivut61-93
Sivumäärä33
JulkaisuNOTRE DAME JOURNAL OF FORMAL LOGIC
Vuosikerta64
Numero1
DOI - pysyväislinkit
TilaJulkaistu - 2023
OKM-julkaisutyyppiA1 Alkuperäisartikkeli tieteellisessä aikakauslehdessä

Julkaisufoorumi-taso

  • Jufo-taso 2

!!ASJC Scopus subject areas

  • Logic

Sormenjälki

Sukella tutkimusaiheisiin 'A Completeness Proof for a Regular Predicate Logic with Undefined Truth Value'. Ne muodostavat yhdessä ainutlaatuisen sormenjäljen.

Siteeraa tätä