Functional Completeness in CPL via Correspondence Analysis
DOI:
https://doi.org/10.18778/0138-0680.48.1.04Keywords:
correspondence analysis, invertible rules, classical propositional logic, functional completeness, sequent calculus, automated deduction, automated rules generationAbstract
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.
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.
N. D. Belnap, How a computer should think, Contemporary Aspects of Philosophy, ed. by G. Rule. Stockseld: Oriel Press (1977), pp. 30–56.
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.
K. Došen, Logical constants as punctuation marks, Notre Dame Journal of Formal Logic, vol. 30, no. 3 (1989), pp. 362–381.
J. M. Dunn, Intuitive semantics for first-degree entailment and coupled trees, Philosophical Studies, vol. 29, no. 3 (1976), pp. 149–168.
M. Fitting, First-Order Logic and Automated Theorem Proving, New York: Springer-Verlag, 1990.
S. Halldén, The Logic of Nonsense. Lundequista Bokhandeln, Uppsala, 1949.
A. Indrzejczak, Rule-Generation Theorem and Its Applications, Bulletin of the Section of Logic, vol. 47, no. 4 (2018), pp. 265–281.
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.
S. C. Kleene, On a notation for ordinal numbers, The Journal of Symbolic Logic, vol. 3, no. 1 (1938), pp. 150–155.
S. C. Kleene, Introduction to metamathematics, Sixth Reprint, Wolters-Noordhoof Publishing and North-Holland Publishing Company, 1971.
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.
E. Kubyshkina, D. V. Zaitsev, Rational agency from a truth-functional perspective, Logic and Logical Philosophy, vol. 25, no. 4 (2016), pp. 499–520.
S. Negri, J. von Plato, Structural Proof Theory, Cambridge: Cambridge University Press, 2001.
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.
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.
Y. Petrukhin, V. Shangin, Natural three-valued logics characterised by natural deduction, Logique et Analyse, vol. 244 (2018), pp. 407–427.
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.
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.
Y. Petrukhin, Correspondence analysis for first degree entailment, Logical Investigations, vol. 22, no. 1 (2016), pp. 108–124.
Y. Petrukhin, Generalized Correspondence Analysis for Three-Valued Logics, Logica Universalis, vol. 12, no. 3-4 (2018), pp. 423–460.
Y. Petrukhin, Correspondence analysis for logic of rational agent, Chelyabinsk Physical and Mathematical Journal, vol. 2, no. 3 (2017), pp. 329–337.
G. Priest, The logic of paradox, Journal of Philosophical Logic, vol. 8, no. 1 (1979), pp. 219–241.
K. Segerberg, Arbitrary truth-value functions and natural deduction, Mathematical Logic Quarterly, vol. 29, no. 11 (1983), pp. 557–564.
A. Tamminga, Correspondence analysis for strong three-valued logic, Logical Investigations, vol. 20 (2014), pp. 255–268.
N. E. Tomova, A lattice of implicative extensions of regular Kleene's logics, Reports on Mathematical Logic, vol. 47 (2012), pp. 173–182.
A. S. Troelstra, H. Schwichtenberg, Basic Proof Theory, second edition, Cambridge: Cambridge University Press, 2000.
W. Wernick, Complete sets of logical functions, Transactions of the American Mathematical Society, vol. 51 (1942), pp. 117–132.
Downloads
Published
Issue
Section
License
Copyright (c) 2019 Bulletin of the Section of Logic
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
How to Cite
