Functional Completeness in CPL via Correspondence Analysis

Dorota Leszczyńska-Jasion; Yaroslav Petrukhin; Vasilyi Shangin; Marcin Jukiewicz

doi:10.18778/0138-0680.48.1.04

Authors

Dorota Leszczyńska-Jasion Department of Logic and Cognitive Science, Adam Mickiewicz University, Poznań, Poland
Yaroslav Petrukhin Department of Logic, Faculty of Philosophy, Lomonosov Moscow State University, Moscow, Russia
Vasilyi Shangin Department of Logic, Faculty of Philosophy, Lomonosov Moscow State University, Moscow, Russia
Marcin Jukiewicz Department of Logic and Cognitive Science, Adam Mickiewicz University, Poznan, Poland

DOI:

https://doi.org/10.18778/0138-0680.48.1.04

Keywords:

correspondence analysis, invertible rules, classical propositional logic, functional completeness, sequent calculus, automated deduction, automated rules generation

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 (sets) of rules characterizing a two-argument Boolean function(s) 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.

References

F. G. Asenjo, A calculus of antinomies, Notre Dame Journal of Formal Logic, vol. 7, no. 1 (1966), pp. 103–105.
Google Scholar

N. D. Belnap, A useful four-valued logic, Modern Uses of Multiple-Valued Logic, ed. by J.M. Dunn, G. Epstein. Boston: Reidel Publishing Company (1977), pp. 7–37.
Google Scholar

N. D. Belnap, How a computer should think, Contemporary Aspects of Philosophy, ed. by G. Rule. Stockseld: Oriel Press (1977), pp. 30–56.
Google Scholar

S. Bonzio, J. Gil-Férez, F. Paoli, L. Peruzzi, On Paraconsistent Weak Kleene Logic: Axiomatisation and Algebraic Analysis, Studia Logica, vol. 105, no. 2 (2017), pp. 253–297.
Google Scholar

K. Došen, Logical constants as punctuation marks, Notre Dame Journal of Formal Logic, vol. 30, no. 3 (1989), pp. 362–381.
Google Scholar

J. M. Dunn, Intuitive semantics for first-degree entailment and coupled trees, Philosophical Studies, vol. 29, no. 3 (1976), pp. 149–168.
Google Scholar

M. Fitting, First-Order Logic and Automated Theorem Proving, New York: Springer-Verlag, 1990.
Google Scholar

S. Halldén, The Logic of Nonsense. Lundequista Bokhandeln, Uppsala, 1949.
Google Scholar

A. Indrzejczak, Rule-Generation Theorem and Its Applications, Bulletin of the Section of Logic, vol. 47, no. 4 (2018), pp. 265–281.
Google Scholar

A. Karpenko, N. Tomova, Bochvar's three-valued logic and literal paralogics: Their lattice and functional equivalence, Logic and Logical Philosophy, vol. 26, no. 2 (2017), pp. 207–235.
Google Scholar

S. C. Kleene, On a notation for ordinal numbers, The Journal of Symbolic Logic, vol. 3, no. 1 (1938), pp. 150–155.
Google Scholar

S. C. Kleene, Introduction to metamathematics, Sixth Reprint, Wolters-Noordhoof Publishing and North-Holland Publishing Company, 1971.
Google Scholar

B. Kooi, A. Tamminga, Completeness via correspondence for extensions of the logic of paradox, The Review of Symbolic Logic, vol. 5, no. 4 (2012), pp. 720–730.
Google Scholar

E. Kubyshkina, D. V. Zaitsev, Rational agency from a truth-functional perspective, Logic and Logical Philosophy, vol. 25, no. 4 (2016), pp. 499–520.
Google Scholar

S. Negri, J. von Plato, Structural Proof Theory, Cambridge: Cambridge University Press, 2001.
Google Scholar

Y. Petrukhin, V. Shangin, Automated correspondence analysis for the binary extensions of the logic of paradox, The Review of Symbolic Logic, vol. 10, no. 4 (2017), pp. 756–781.
Google Scholar

Y. Petrukhin, V. Shangin, Automated proof searching for strong Kleene logic and its binary extensions via correspondence analysis, Logic and Logical Philosophy, vol. 28, no. 2 (2019), pp. 223–257.
Google Scholar

Y. Petrukhin, V. Shangin, Natural three-valued logics characterised by natural deduction, Logique et Analyse, vol. 244 (2018), pp. 407–427.
Google Scholar

Y. Petrukhin, V. Shangin, Completeness via correspondence for extensions of paraconsistent weak Kleene logic, The Proceedings of the 10th Smirnov Readings in Logic (2017), pp. 114–115.
Google Scholar

Y. Petrukhin, V. Shangin, Correspondence Analysis and Automated Proof-searching for First Degree Entailment, European Journal of Mathematics, online first article, DOI: 10.1007/s40879-019-00344-5.
Google Scholar

Y. Petrukhin, Correspondence analysis for first degree entailment, Logical Investigations, vol. 22, no. 1 (2016), pp. 108–124.
Google Scholar

Y. Petrukhin, Generalized Correspondence Analysis for Three-Valued Logics, Logica Universalis, vol. 12, no. 3-4 (2018), pp. 423–460.
Google Scholar

Y. Petrukhin, Correspondence analysis for logic of rational agent, Chelyabinsk Physical and Mathematical Journal, vol. 2, no. 3 (2017), pp. 329–337.
Google Scholar

G. Priest, The logic of paradox, Journal of Philosophical Logic, vol. 8, no. 1 (1979), pp. 219–241.
Google Scholar

K. Segerberg, Arbitrary truth-value functions and natural deduction, Mathematical Logic Quarterly, vol. 29, no. 11 (1983), pp. 557–564.
Google Scholar

A. Tamminga, Correspondence analysis for strong three-valued logic, Logical Investigations, vol. 20 (2014), pp. 255–268.
Google Scholar

N. E. Tomova, A lattice of implicative extensions of regular Kleene's logics, Reports on Mathematical Logic, vol. 47 (2012), pp. 173–182.
Google Scholar

A. S. Troelstra, H. Schwichtenberg, Basic Proof Theory, second edition, Cambridge: Cambridge University Press, 2000.
Google Scholar

W. Wernick, Complete sets of logical functions, Transactions of the American Mathematical Society, vol. 51 (1942), pp. 117–132.
Google Scholar