A Gentzen Calculus for Nothing but the Truth

S. Wintein, Reinhard Muskens

Research output: Contribution to journalArticleScientificpeer-review

Abstract

In their paper Nothing but the Truth Andreas Pietz and Umberto Rivieccio present Exactly True Logic, an interesting variation upon the four-valued logic for first-degree entailment FDE that was given by Belnap and Dunn in the 1970s. Pietz & Rivieccio provide this logic with a Hilbert-style axiomatisation and write that finding a nice sequent calculus for the logic will presumably not be easy. But a sequent calculus can be given and in this paper we will show that a calculus for the Belnap-Dunn logic we have defined earlier can in fact be reused for the purpose of characterising ETL, provided a small alteration is made—initial assignments of signs to the sentences of a sequent to be proved must be different from those used for characterising FDE. While Pietz & Rivieccio define ETL on the language of classical propositional logic we also study its consequence relation on an extension of this language that is functionally complete for the underlying four truth values. On this extension the calculus gets a multiple-tree character—two proof trees may be needed to establish one proof.
Original languageEnglish
Pages (from-to)1-15
Number of pages15
JournalJournal of philosophical logic
Publication statusPublished - 2015

Fingerprint

Gentzen
Calculi
Logic
Belnap
Language
Sequent Calculus
Axiomatization
Alteration
Propositional Logic
1970s
Truth Value
David Hilbert
Consequence Relation
Assignment
Entailment

Keywords

  • Belnap-Dunn logic
  • Gentzen calculi
  • Multiple tree calculi
  • Exactly true logic

Cite this

@article{4032feb3c71449c5952a64f3f168753c,
title = "A Gentzen Calculus for Nothing but the Truth",
abstract = "In their paper Nothing but the Truth Andreas Pietz and Umberto Rivieccio present Exactly True Logic, an interesting variation upon the four-valued logic for first-degree entailment FDE that was given by Belnap and Dunn in the 1970s. Pietz & Rivieccio provide this logic with a Hilbert-style axiomatisation and write that finding a nice sequent calculus for the logic will presumably not be easy. But a sequent calculus can be given and in this paper we will show that a calculus for the Belnap-Dunn logic we have defined earlier can in fact be reused for the purpose of characterising ETL, provided a small alteration is made—initial assignments of signs to the sentences of a sequent to be proved must be different from those used for characterising FDE. While Pietz & Rivieccio define ETL on the language of classical propositional logic we also study its consequence relation on an extension of this language that is functionally complete for the underlying four truth values. On this extension the calculus gets a multiple-tree character—two proof trees may be needed to establish one proof.",
keywords = "Belnap-Dunn logic, Gentzen calculi, Multiple tree calculi, Exactly true logic",
author = "S. Wintein and Reinhard Muskens",
note = "Online first",
year = "2015",
language = "English",
pages = "1--15",
journal = "Journal of philosophical logic",
issn = "0022-3611",
publisher = "Springer Netherlands",

}

A Gentzen Calculus for Nothing but the Truth. / Wintein, S.; Muskens, Reinhard.

In: Journal of philosophical logic, 2015, p. 1-15.

Research output: Contribution to journalArticleScientificpeer-review

TY - JOUR

T1 - A Gentzen Calculus for Nothing but the Truth

AU - Wintein, S.

AU - Muskens, Reinhard

N1 - Online first

PY - 2015

Y1 - 2015

N2 - In their paper Nothing but the Truth Andreas Pietz and Umberto Rivieccio present Exactly True Logic, an interesting variation upon the four-valued logic for first-degree entailment FDE that was given by Belnap and Dunn in the 1970s. Pietz & Rivieccio provide this logic with a Hilbert-style axiomatisation and write that finding a nice sequent calculus for the logic will presumably not be easy. But a sequent calculus can be given and in this paper we will show that a calculus for the Belnap-Dunn logic we have defined earlier can in fact be reused for the purpose of characterising ETL, provided a small alteration is made—initial assignments of signs to the sentences of a sequent to be proved must be different from those used for characterising FDE. While Pietz & Rivieccio define ETL on the language of classical propositional logic we also study its consequence relation on an extension of this language that is functionally complete for the underlying four truth values. On this extension the calculus gets a multiple-tree character—two proof trees may be needed to establish one proof.

AB - In their paper Nothing but the Truth Andreas Pietz and Umberto Rivieccio present Exactly True Logic, an interesting variation upon the four-valued logic for first-degree entailment FDE that was given by Belnap and Dunn in the 1970s. Pietz & Rivieccio provide this logic with a Hilbert-style axiomatisation and write that finding a nice sequent calculus for the logic will presumably not be easy. But a sequent calculus can be given and in this paper we will show that a calculus for the Belnap-Dunn logic we have defined earlier can in fact be reused for the purpose of characterising ETL, provided a small alteration is made—initial assignments of signs to the sentences of a sequent to be proved must be different from those used for characterising FDE. While Pietz & Rivieccio define ETL on the language of classical propositional logic we also study its consequence relation on an extension of this language that is functionally complete for the underlying four truth values. On this extension the calculus gets a multiple-tree character—two proof trees may be needed to establish one proof.

KW - Belnap-Dunn logic

KW - Gentzen calculi

KW - Multiple tree calculi

KW - Exactly true logic

M3 - Article

SP - 1

EP - 15

JO - Journal of philosophical logic

JF - Journal of philosophical logic

SN - 0022-3611

ER -