Two-sided Sequent Calculi for FDE-like Four-valued Logics

Barteld Kooi*, Allard Tamminga

*Corresponding author for this work

Research output: Contribution to journalArticleAcademicpeer-review

1 Citation (Scopus)
8 Downloads (Pure)


We present a method that generates two-sided sequent calculi for four-valued logics like first degree entailment (FDE). (We say that a logic is FDE-like if it has finitely many operators of finite arity, including negation, and if all of its operators are truth-functional over the four truth-values ‘none’, ‘false’, ‘true’, and ‘both’, where ‘true’ and ‘both’ are designated.) First, we show that for every n-ary operator ⋆ every truth table entry f(x1,…,xn) = y can be characterized in terms of a pair of sequent rules. Secondly, we use these sequent rules to build sequent calculi and prove their completeness. With the help of two simplification procedures we then show that the 2 ⋅ 4n sequent rules that characterize an n-ary operator can be systematically reduced to at most four sequent rules. Thirdly, we use our method to investigate the proof-theoretical consequences of including intuitive truth-functional implications in FDE-like logics.

Original languageEnglish
Pages (from-to)495-518
Number of pages24
JournalJournal of Philosophical Logic
Early online date25-Aug-2022
Publication statusPublished - Apr-2023


  • First degree entailment
  • Many-valued logic
  • Proof theory
  • Sequent calculi

Cite this