D-complete Single Axioms for the Equivalential Calculus with the rules D and R

Marcin Czakon

doi:10.18778/0138-0680.2024.15

Authors

Marcin Czakon John Paul II Catholic University of Lublin, Department of Logic https://orcid.org/0000-0001-6217-6640

DOI:

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

Keywords:

equivalential calculus, D-complete, single axiom, condensed detachment

Abstract

Ulrich (2005) showed that most of the known axiomatisations of the classical equivalence calculus (EC) are D-incomplete, that is, they are not complete with the condensed detachment rule (D) as the primary rule of the proof procedure. He proved that the axiomatisation \(\{EEpEqrErEqp, EEEpppp\}\) by Wajsberg (1937) is D-complete and pointed out a number of D-complete single axioms, including one organic single axiom. In this paper we present new single axioms for EC with the condensed detachment and the reversed condensed detachment rules that form D-complete bases and are organic.

References

J. R. Hindley, “BCK and BCI logics, condensed detachment and the 2-property,” Notre Dame Journal of Formal Logic, vol. 34, no. 2, 1993, pp. 231–250, DOI: https://doi.org/10.1305/ndjfl/1093634655
Google Scholar DOI: https://doi.org/10.1305/ndjfl/1093634655

J. R. Hindley, D. Meredith, “Principal Type-Schemes and Condensed Detachment,” The Journal of Symbolic Logic, vol. 55, no. 1, 1990, pp. 90–105, URL: http://www.jstor.org/stable/2274956
Google Scholar DOI: https://doi.org/10.2307/2274956

K. Hodgson, “Shortest Single Axioms for the Equivalential Calculus with CD and RCD,” Journal of Automated Reasoning, vol. 20, 1998, pp. 283–316, DOI: https://doi.org/10.1023/A:1005731217123
Google Scholar DOI: https://doi.org/10.1023/A:1005731217123

J. A. Kalman, “Condensed Detachment as a Rule of Inference,” Studia Logica, vol. 42, no. 4, 1983, pp. 443–451, DOI: https://doi.org/10.1007/bf01371632
Google Scholar DOI: https://doi.org/10.1007/BF01371632

S. Leśniewski, “Grundzüge eines neuen Systems der Grundlagen der Mathematik,” Fundamenta Mathematicae, vol. 14, no. 1, 1929, pp. 1–81.
Google Scholar DOI: https://doi.org/10.4064/fm-14-1-1-81

C. A. Meredith, A. N. Prior, “Notes on the axiomatics of the propositional calculus,” Notre Dame Journal of Formal Logic, vol. 4, no. 3, 1963, pp. 171–187, DOI: https://doi.org/10.1305/ndjfl/1093957574
Google Scholar DOI: https://doi.org/10.1305/ndjfl/1093957574

J. G. Peterson, “Shortest single axioms for the classical equivalential calculus,” Notre Dame Journal of Formal Logic, vol. 17, no. 2, 1976, pp. 267–271, DOI: https://doi.org/10.1305/ndjfl/1093887534
Google Scholar DOI: https://doi.org/10.1305/ndjfl/1093887534

J. A. Robinson, “A Machine-Oriented Logic Based on the Resolution Principle,” Journal of the ACM, vol. 12, no. 1, 1965, pp. 23–41, DOI: https://doi.org/10.1145/321250.321253
Google Scholar DOI: https://doi.org/10.1145/321250.321253

D. Ulrich, “D-complete axioms for the classical equivalential calculus,” Bulletin of the Section of Logic, vol. 34, 2005, pp. 135–142.
Google Scholar

M. Wajsberg, “Metalogische Beiträge,” Wiadomości Matematyczne, vol. 43, 1937, pp. 131–168.
Google Scholar

L. Wos, D. Ulrich, B. Fitelson, “XCB, The last of the shortest single axioms for the classical equivalential calculus,” Bulletin of the Section of Logic, vol. 3, no. 32, 2003, pp. 131–136.
Google Scholar

J. Łukasiewicz, “Równoważnościowy rachunek zdań,” in: J. Łukasiewicz (ed.), Z zagadnień Logiki i Filozofii, Państwowe Wydawnictwo Naukowe, Warszawa, 1939, pp. 234–235.
Google Scholar