Functional Completeness in CPL via Correspondence Analysis

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

Bulletin of the Section of Logic (2019)

  • Volume: 48, Issue: 1
  • ISSN: 0138-0680

Abstract

top
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.

How to cite

top

Dorota Leszczyńska-Jasion, et al. "Functional Completeness in CPL via Correspondence Analysis." Bulletin of the Section of Logic 48.1 (2019): null. <http://eudml.org/doc/295543>.

@article{DorotaLeszczyńska2019,
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.},
author = {Dorota Leszczyńska-Jasion, Yaroslav Petrukhin, Vasilyi Shangin, Marcin Jukiewicz},
journal = {Bulletin of the Section of Logic},
keywords = {correspondence analysis; invertible rules; classical propositional logic; functional completeness; sequent calculus; automated deduction; automated rules generation},
language = {eng},
number = {1},
pages = {null},
title = {Functional Completeness in CPL via Correspondence Analysis},
url = {http://eudml.org/doc/295543},
volume = {48},
year = {2019},
}

TY - JOUR
AU - Dorota Leszczyńska-Jasion
AU - Yaroslav Petrukhin
AU - Vasilyi Shangin
AU - Marcin Jukiewicz
TI - Functional Completeness in CPL via Correspondence Analysis
JO - Bulletin of the Section of Logic
PY - 2019
VL - 48
IS - 1
SP - null
AB - 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.
LA - eng
KW - correspondence analysis; invertible rules; classical propositional logic; functional completeness; sequent calculus; automated deduction; automated rules generation
UR - http://eudml.org/doc/295543
ER -

References

top
  1. F. G. Asenjo, A calculus of antinomies, Notre Dame Journal of Formal Logic, vol. 7, no. 1 (1966), pp. 103–105. 
  2. 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. 
  3. N. D. Belnap, How a computer should think, Contemporary Aspects of Philosophy, ed. by G. Rule. Stockseld: Oriel Press (1977), pp. 30–56. 
  4. 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. 
  5. K. Došen, Logical constants as punctuation marks, Notre Dame Journal of Formal Logic, vol. 30, no. 3 (1989), pp. 362–381. 
  6. J. M. Dunn, Intuitive semantics for first-degree entailment and coupled trees, Philosophical Studies, vol. 29, no. 3 (1976), pp. 149–168. 
  7. M. Fitting, First-Order Logic and Automated Theorem Proving, New York: Springer-Verlag, 1990. 
  8. S. Halldén, The Logic of Nonsense. Lundequista Bokhandeln, Uppsala, 1949. 
  9. A. Indrzejczak, Rule-Generation Theorem and Its Applications, Bulletin of the Section of Logic, vol. 47, no. 4 (2018), pp. 265–281. 
  10. 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. 
  11. S. C. Kleene, On a notation for ordinal numbers, The Journal of Symbolic Logic, vol. 3, no. 1 (1938), pp. 150–155. 
  12. S. C. Kleene, Introduction to metamathematics, Sixth Reprint, Wolters-Noordhoof Publishing and North-Holland Publishing Company, 1971. 
  13. 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. 
  14. E. Kubyshkina, D. V. Zaitsev, Rational agency from a truth-functional perspective, Logic and Logical Philosophy, vol. 25, no. 4 (2016), pp. 499–520. 
  15. S. Negri, J. von Plato, Structural Proof Theory, Cambridge: Cambridge University Press, 2001. 
  16. 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. 
  17. 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. 
  18. Y. Petrukhin, V. Shangin, Natural three-valued logics characterised by natural deduction, Logique et Analyse, vol. 244 (2018), pp. 407–427. 
  19. 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. 
  20. 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. 
  21. Y. Petrukhin, Correspondence analysis for first degree entailment, Logical Investigations, vol. 22, no. 1 (2016), pp. 108–124. 
  22. Y. Petrukhin, Generalized Correspondence Analysis for Three-Valued Logics, Logica Universalis, vol. 12, no. 3-4 (2018), pp. 423–460. 
  23. Y. Petrukhin, Correspondence analysis for logic of rational agent, Chelyabinsk Physical and Mathematical Journal, vol. 2, no. 3 (2017), pp. 329–337. 
  24. G. Priest, The logic of paradox, Journal of Philosophical Logic, vol. 8, no. 1 (1979), pp. 219–241. 
  25. K. Segerberg, Arbitrary truth-value functions and natural deduction, Mathematical Logic Quarterly, vol. 29, no. 11 (1983), pp. 557–564. 
  26. A. Tamminga, Correspondence analysis for strong three-valued logic, Logical Investigations, vol. 20 (2014), pp. 255–268. 
  27. N. E. Tomova, A lattice of implicative extensions of regular Kleene's logics, Reports on Mathematical Logic, vol. 47 (2012), pp. 173–182. 
  28. A. S. Troelstra, H. Schwichtenberg, Basic Proof Theory, second edition, Cambridge: Cambridge University Press, 2000. 
  29. W. Wernick, Complete sets of logical functions, Transactions of the American Mathematical Society, vol. 51 (1942), pp. 117–132. 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.