Skip to main content
SpringerLink
Log in

Correspondence Analysis for Some Fragments of Classical Propositional Logic

  • Published:
Logica Universalis Aims and scope Submit manuscript

Abstract

In the paper, we apply Kooi and Tamminga’s correspondence analysis (that has been previously applied to some notable three- and four-valued logics) to some conventional and functionally incomplete fragments of classical propositional logic. In particular, the paper deals with the implication, disjunction, and negation fragments. Additionally, we consider an application of correspondence analysis to some connectiveless fragment with certain basic properties of the logical consequence relation only. As a result of the application, one obtains a sound and complete natural deduction system for any binary extension of each fragment in question. With the focus on exclusive disjunction we comparatively study the proposed systems. Finally, we discuss Segerberg’s systems for connectiveless and negation fragments and compare them with our systems.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5

Similar content being viewed by others

Notes

  1. We come back to this issue in Sect. 5, where we compare Segerberg’s approach and ours, since Segerberg, as we did, considered classical logic. Let us notice that Kooi and Tamminga do not mention Segerberg’s work.

  2. For the purpose of this paper, we don’t treat conjunction (\( \wedge \)) as a primitive. However, correspondence analysis works with conjunction, too.

  3. Note the inference schemata for \( f_\circ (0,1)=0 \), \( f_\circ (1,0)=0 \), \( f_\circ (1,1)=0 \), and \( f_\circ (1,1)=1 \) are the same as in Theorem 2.1 while the rest ones are different. This fact is essential for the proof of Theorem 4.13 (Completeness) below.

  4. Note case \( f_\circ (0,0)=1 \) below clearly indicates some extensions contain tautologies that isn’t the case for the other correspondence analyses in this paper. It doesn’t imply they don’t contain tautologies (in fact, they do, e.g. the implication fragment contains Peirce’s law; see Sect. 3.1 below). However, correspondence analysis for the disjunction fragment shows the existence of tautologies in some of its extensions explicitely.

  5. The reader will find some similarities with Kalmár’s folklore conditions in the equivalences below. However, the difference is that Kalmár’s conditions are usually expressed via some implicational formulae (see, for example, [17]).

  6. The rule (EEM) is inspired by a formula \( A\vee (A\rightarrow B) \) (see Definition 4.4 which will clarify it) to have been known as the extended law of excluded middle [19, p. 17]. Note by adding \( A\vee (A\rightarrow B) \) or Peirce’s law \( ((A\rightarrow B)\rightarrow A)\rightarrow A \) to intuitionistic logic one obtains classical logic [19, p. 18]. To be sure, there are other formulae which give the same result (for example, it is a folklore about the law of double negation elimination \( \lnot \lnot A\rightarrow A \) and the law of excluded middle \( A\vee \lnot A \)). We stress, however, that despite some laws discussed in this footnote contain disjunction or negation the rules of the natural deduction system for the implication fragment contain implication only.

  7. Though the symbol \( \veebar \) isn’t in the languages of this paper, we will use it for the human-friendliness of the presentation.

  8. This example is a kind of introduction rule for exclusive disjunction and may be viewed as an analogue of one of the well-known introduction rules for inclusive disjunction: \(\frac{p}{p\vee q}\).

  9. We remind the reader that “\( \Rightarrow \)” in Theorem 2.3 turns out to be the usual assertion of a subderivation in the formulation of some rules of this natural deduction system (see the beginning of Sect. 2.2 above).

  10. To be sure, there are deductively equal alternatives to these rules. We pick up this pair of rules as the most convenient for our completeness proof. The rule (EM) is inspired by the law of excluded middle \( A\vee \lnot A\) (see Definition 4.3 which will clarify it) and the rule (EFQ) is Ex Falso Quodlibet.

  11. Note we adapt this Definition to the rule of extended excluded middle (EEM) while Definition 4.3 is adapted to the rule of excluded middle (EM). Since non-trivial theories which are defined in Definition 4.3 are called maximal ones, so non-trivial theories which are defined in Definition 4.4 are said to be extended maximal ones.

  12. We acknowledge, however, that in [8] the authors do not claim that Segerberg’s ideas could not be extended to n-valued logic without their reduction.

References

  1. Asenjo, F.G.: A calculus of antinomies. Notre Dame J. Formal Logic 7, 103–105 (1966)

    Article  MathSciNet  Google Scholar 

  2. Avron, A.: Natural 3-valued logics—characterization and proof theory. J. Symbol. Logic 56, 276–294 (1991)

    Article  MathSciNet  Google Scholar 

  3. Belnap, N.D.: A useful four-valued logic. In: Dunn, J.M., Epstein, G. (eds.) Modern Uses of Multiple-Valued Logic, pp. 7–37. Reidel Publishing Company, Dordrecht (1977)

    Google Scholar 

  4. Belnap, N.D.: How a computer should think. In: Rule, G. (ed.) Contemporary Aspects of Philosophy, pp. 30–56. Oriel Press, Mumbai (1977)

    Google Scholar 

  5. Bolotov, A., Bocharov, V., Gorchakov, A., Shangin, V.: Automated first order natural deduction. In: Proceedings of the 2nd Indian International Conference on Artificial Intelligence, pp. 1292–1311 (2015)

  6. Caleiro, C., Marcos, J.: Classic-like analytic tableaux for finite-valued logics. In: WoLLIC-2009, Selected Papers, Ed. by H. Ono, R. de Queiroz, M. Kanazawa. Lecture Notes in Artificial Intelligence. 5514, Springer pp. 268–280 (2009)

  7. Copi, I.M., Cohen, C., McMahon, K.: Introduction to logic, 14th edn. Routledge, Abingdon-on-Thames (2011)

    Google Scholar 

  8. Englander, C., Haeusler, E.H., Pereira, L.C.: Finitely many-valued logics and natural deduction. Logic J. IGPL 22(2), 333–354 (2013)

    Article  MathSciNet  Google Scholar 

  9. Dunn, J.M.: Intuitive semantics for first-degree entailment and coupled trees. Philos. Stud. 29, 149–168 (1976)

    Article  MathSciNet  Google Scholar 

  10. Heyting, A.: Die Formalen Regeln der intuitionistischen Logik. Sitzungsber. Preussischen Acad. Wiss. Berlin, pp. 42–46 (1930)

  11. Ferrari, M., Fiorentini, C.: Proof-Search in natural deduction calculus for classical propositional logic. Lecture Notes in Comput. Sci. 9323, 237–252 (2015)

    Article  MathSciNet  Google Scholar 

  12. Karpenko, A., Tomova, N.: Bochvar’s three-valued logic and literal paralogics: their lattice and functional equivalence. Logic Log. Philos. 26(2), 207–235 (2017)

    MathSciNet  MATH  Google Scholar 

  13. Kleene, S.C.: On a notation for ordinal numbers. J. Symbol. Logic 3, 150–155 (1938)

    Article  Google Scholar 

  14. Kooi, B., Tamminga, A.: Completeness via correspondence for extensions of the logic of paradox. Rev. Symbol. Logic 5, 720–730 (2012)

    Article  MathSciNet  Google Scholar 

  15. Leszczyńska-Jasion, D., Petrukhin, Y., Shangin, V., Jukiewicz, M.: Functional completeness in CPL via correspondence analysis. Bull. Sect. Logic 48(1), 45–76 (2019)

    MathSciNet  MATH  Google Scholar 

  16. Leszczyńska-Jasion, D., Petrukhin, Y., Shangin, V.: The method of Socratic proofs meets correspondence analysis. Bull. Sect. Logic 48(2), 99–116 (2019)

    Article  MathSciNet  Google Scholar 

  17. Mendelson, E.: Introduction to Mathematical Logic, 4th edn. Chapman & Hall, Boca Raton (1997)

    MATH  Google Scholar 

  18. Negri, S., von Plato, J.: Structural Proof-Theory. Cambridge University Press, Cambridge (2001)

    Book  Google Scholar 

  19. Odintsov, S.P.: Constructive Negations and Paraconsistency. Springer, Berlin (2008)

    Book  Google Scholar 

  20. Osorio, M., Carballido, J.L.: Brief study of \({ G}_3^\prime \) logic. J. Appl. Non-Class. Logic 18(4), 475–499 (2008)

    Article  Google Scholar 

  21. Petrukhin, Y., Shangin, V.: Automated correspondence analysis for the binary extensions of the logic of paradox. Rev. Symbol. Logic 10(4), 756–781 (2017)

    Article  MathSciNet  Google Scholar 

  22. Petrukhin, Y., Shangin, V.: Natural three-valued logics characterised by natural deduction. Log. et Anal. 61(244), 407–427 (2018)

    MathSciNet  MATH  Google Scholar 

  23. Petrukhin, Y., Shangin, V.: Automated proof-searching for strong Kleene logic and its binary extensions via correspondence analysis. Log. Log. Philos. 28(2), 223–257 (2019)

    MathSciNet  MATH  Google Scholar 

  24. Petrukhin, Y., Shangin, V.: Correspondence analysis and automated proof-searching for first degree entailment. Eur. J. Math. 6(4), 1452–1495 (2020)

    Article  MathSciNet  Google Scholar 

  25. Petrukhin, Y.: Generalized correspondence analysis for three-valued logics. Log. Univers. 12(3–4), 423–460 (2018)

    Article  MathSciNet  Google Scholar 

  26. Priest, G.: The logic of paradox. J. Philos. Logic 8, 219–241 (1979)

    Article  MathSciNet  Google Scholar 

  27. Segerberg, K.: Arbitrary truth-value functions and natural deduction. Math. Logic Quart. 29(11), 557–564 (1983)

    Article  MathSciNet  Google Scholar 

  28. Shangin, V.O.: A precise definition of an inference (by the example of natural deduction systems for logics \( I_{\langle \alpha ,\beta \rangle } \)). Log. Investig. 23(1), 83–104 (2017)

    Article  MathSciNet  Google Scholar 

  29. Tamminga, A.: Correspondence analysis for strong three-valued logic. Log. Investig. 20, 255–268 (2014)

    MathSciNet  MATH  Google Scholar 

  30. Tomova, N.E.: A lattice of implicative extensions of regular Kleene’s logics. Rep. Math. Logic 47, 173–182 (2012)

    MathSciNet  MATH  Google Scholar 

Download references

Acknowledgements

We would like to thank the first reviewer for the valuable suggestions. The second author thanks Xenia Shliakhtina for the everlasting inspiration.

Author information

Authors and Affiliations

  1. University of Lodz, Lindleya 3/5, 90-131, Lodz, Poland

    Yaroslav Petrukhin

  2. Lomonosov Moscow State University, Lomonosovsky prospekt 27-4, 119991, Moscow, Russia

    Vasilyi Shangin

Authors
  1. Yaroslav Petrukhin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Vasilyi Shangin
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Yaroslav Petrukhin.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

The first author is supported by Polish National Science Centre, Grant Number DEC-2017/25/B/HS1/01268. The second author is supported by RFBR, Grant Number 20-011-00698 A.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Petrukhin, Y., Shangin, V. Correspondence Analysis for Some Fragments of Classical Propositional Logic. Log. Univers. 15, 67–85 (2021). https://doi.org/10.1007/s11787-021-00267-4

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11787-021-00267-4

Keywords

Mathematics Subject Classification

Search

Navigation