Functional Completeness in CPL via Correspondence Analysis


Authors
Yaroslav Petrukhin
Moscow State University
Abstract
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.
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.18778/0138-0680.48.1.04
Options
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive


Upload a copy of this paper     Check publisher's policy     Papers currently archived: 43,914
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

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.

View all 11 references / Add more references

Citations of this work BETA

Add more citations

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.

Analytics

Added to PP index
2019-09-08

Total views
8 ( #827,416 of 2,266,272 )

Recent downloads (6 months)
8 ( #144,326 of 2,266,272 )

How can I increase my downloads?

Downloads

My notes

Sign in to use this feature