Functional Completeness in CPL via Correspondence Analysis

Bulletin of the Section of Logic 48 (1) (2019)
  Copy   BIBTEX


Kooi and Tamminga's correspondence analysis is a technique for designing proof systems, mostly, natural deduction and sequent systems. In this paper it is used to generate sequent calculi with invertible rules, whose only branching rule is the rule of cut. The calculi pertain to classical propositional logic and any of its fragments that may be obtained from adding a set of rules characterizing a two-argument Boolean function to the negation fragment of classical propositional logic. The properties of soundness and completeness of the calculi are demonstrated. The proof of completeness is conducted by Kalmár's method. Most of the presented sequent-calculus rules have been obtained automatically, by a rule-generating algorithm implemented in Python. Correctness of the algorithm is demonstrated. This automated approach allowed us to analyse thousands of possible rules' schemes, hundreds of rules corresponding to Boolean functions, and to nd dozens of those invertible. Interestingly, the analysis revealed that the presented proof-theoretic framework provides a syntactic characteristics of such an important semantic property as functional completeness.



    Upload a copy of this work     Papers currently archived: 91,271

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Proofs and Countermodels in Non-Classical Logics.Sara Negri - 2014 - Logica Universalis 8 (1):25-60.
Partial and paraconsistent three-valued logics.Vincent Degauquier - 2016 - Logic and Logical Philosophy 25 (2):143-171.
Labeled sequent calculus for justification logics.Meghdad Ghari - 2017 - Annals of Pure and Applied Logic 168 (1):72-111.
Stoic Sequent Logic and Proof Theory.Susanne Bobzien - 2019 - History and Philosophy of Logic 40 (3):234-265.
An approach to infinitary temporal proof theory.Stefano Baratella & Andrea Masini - 2004 - Archive for Mathematical Logic 43 (8):965-990.
Reasoning About Collectively Accepted Group Beliefs.Raul Hakli & Sara Negri - 2011 - Journal of Philosophical Logic 40 (4):531-555.
Propositional proof compressions and DNF logic.L. Gordeev, E. Haeusler & L. Pereira - 2011 - Logic Journal of the IGPL 19 (1):62-86.
Sequent Calculi for Visser's Propositional Logics.Kentaro Kikuchi & Ryo Kashima - 2001 - Notre Dame Journal of Formal Logic 42 (1):1-22.


Added to PP

22 (#684,548)

6 months
6 (#506,019)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Yaroslav Petrukhin
Moscow State University

Citations of this work

Non-transitive Correspondence Analysis.Yaroslav Petrukhin & Vasily Shangin - 2023 - Journal of Logic, Language and Information 32 (2):247-273.
Two-sided Sequent Calculi for FDE-like Four-valued Logics.Barteld Kooi & Allard Tamminga - 2023 - Journal of Philosophical Logic 52 (2):495-518.

Add more citations

References found in this work

The logic of paradox.Graham Priest - 1979 - Journal of Philosophical Logic 8 (1):219 - 241.
A useful four-valued logic.N. D. Belnap - 1977 - In J. M. Dunn & G. Epstein (eds.), Modern Uses of Multiple-Valued Logic. D. Reidel.
How a computer should think.Nuel Belnap - 1977 - In Gilbert Ryle (ed.), Contemporary aspects of philosophy. Boston: Oriel Press.
On notation for ordinal numbers.S. C. Kleene - 1938 - Journal of Symbolic Logic 3 (4):150-155.
Logical constants as punctuation marks.Kosta Došen - 1989 - Notre Dame Journal of Formal Logic 30 (3):362-381.

View all 10 references / Add more references