## Correspondence analysis and automated proof-searching for first degree entailment.(English)Zbl 1485.03029

Summary: In this paper, we present correspondence analysis for the well-known four-valued logic First Degree Entailment (FDE). Correspondence analysis is Kooi and Tamminga’s technique for finding adequate natural deduction systems for all the truth-functional unary and binary extensions of an arbitrary functionally incomplete many-valued logic. In particular, B. Kooi and A. Tamminga [Rev. Symb. Log. 5, No. 4, 720–730 (2012; Zbl 1270.03045)] initially presented correspondence analysis for Asenjo-Priest’s three-valued the Logic of Paradox. Generally speaking, a tabular functionally incomplete many-valued logic is added with an arbitrary unary or binary connective $$\circ$$ following the truth-table definition of $$\circ$$. As a result, a tremendous amount of logics obtains a sound and complete natural deduction system in one go. In this paper, we generalize its application proposed by Kooi and Tamminga [loc. cit.] for the unary extensions of FDE and obtain correspondence analysis for the binary extensions of the logic in question. On the other hand, we use a proof-searching algorithm to have been successfully applied to classical and a variety of non-classical logics and present a finite, sound, and complete proof-searching algorithm for natural deduction systems for the binary extensions of FDE obtained via correspondence analysis. In the end, a comparative study of this method and the method presented by Avron and his collaborators is given.

### MSC:

 03B35 Mechanization of proofs and logical operations 68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) 03B50 Many-valued logic 03B47 Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) 03B53 Paraconsistent logics

Zbl 1270.03045
Full Text:

### References:

 [1] Anderson, AR; Belnap, ND Jr, Entailment: The Logic of Relevance and Necessity (1975), Princeton: Princeton University Press, Princeton · Zbl 0323.02030 [2] Anderson, AR; Belnap, ND; Dunn, JM, Entailment: The Logic of Relevance and Necessity (1992), Princeton: Princeton University Press, Princeton · Zbl 0921.03025 [3] Anshakov, O.; Rychkov, S., On finite-valued propositional logical calculi, Notre Dame J. Form. Log., 36, 4, 606-629 (1994) · Zbl 0852.03009 [4] Arieli, O.; Avron, A., Reasoning with logical bilattices, J. Logic Lang. Inf., 5, 1, 25-63 (1996) · Zbl 0851.03017 [5] Arieli, O.; Avron, A., The values of four values, Artificial Intelligence, 102, 1, 97-141 (1998) · Zbl 0928.03025 [6] Arieli, O.; Avron, A., Four-valued paradefinite logics, Studia Logica, 105, 6, 1087-1122 (2017) · Zbl 1417.03190 [7] Asenjo, FG, A calculus of antinomies, Notre Dame J. Form. Log., 7, 103-105 (1966) · Zbl 0145.00508 [8] Avron, A., Natural 3-valued logics—characterization and proof theory, J. Symb. Log., 56, 1, 276-294 (1991) · Zbl 0745.03017 [9] Avron, A.; Arieli, O.; Zamansky, A., Theory of Effective Propositional Paraconsistent (2018), Milton Keynes: College Publications, Milton Keynes · Zbl 1448.03001 [10] Avron, A.; Ben-Naim, J.; Konikowska, B., Cut-free ordinary sequent calculi for logics having generalized finite-valued semantics, Log. Univers., 1, 1, 41-70 (2007) · Zbl 1118.03049 [11] Avron, A.; Konikowska, B.; Zamansky, A., Cut-free sequent calculi for C-systems with generalized finite-valued semantics, J. Logic Comput., 23, 3, 517-540 (2013) · Zbl 1267.03032 [12] Avron, A.; Zamansky, A.; Gabbay, DM; Guenthner, F., Non-deterministic semantics for logical systems, Handbook of Philosophical Logic, 227-304 (2011), Dordrecht: Springer, Dordrecht [13] Baaz, M.; Hájek, P., Infinite-valued Gödel logic with 0-1-projections and relativisations, Gödel’96: Logical Foundations of Mathematics, Computer Science and Physics, 23-33 (1996), Berlin: Springer, Berlin [14] Belnap, ND Jr; Dunn, M.; Epstein, G., A useful four-valued logic, Modern Uses of Multiple-Valued Logic, 5-37 (1977), Dordrecht: Reidel, Dordrecht [15] Belnap, ND; Ryle, G., How a computer should think, Contemporary Aspects of Philosophy, 30-56 (1977), Stocksfield: Oriel Press, Stocksfield [16] Béziau, J-Y, A new four-valued approach to modal logic, Logique et Anal. (N.S.), 54, 213, 109-121 (2011) · Zbl 1228.03003 [17] Bolotov, A.; Shangin, V., Natural deduction system in paraconsistent setting: proof search for PCont, J. Intell. Syst., 21, 1, 1-24 (2012) [18] Brady, RT, Completeness proofs for the systems RM3 and BN4, Logique et Anal. (N.S.), 25, 97, 9-32 (1982) · Zbl 0498.03012 [19] Brunner, ABM; Carnielli, WA, Anti-intuitionism and paraconsistency, J. Appl. Log., 3, 1, 161-184 (2005) · Zbl 1067.03033 [20] Carnielli, W.; Coniglio, ME; Marcos, J.; Gabbay, DM; Guenthner, F., Logics of formal inconsistency, Handbook of Philosophical Logic, vol. 14, 1-93 (2007), Berlin: Springer, Berlin · Zbl 1266.03006 [21] Carnielli, WA; Marcos, J.; Carnielli, WA; Coniglio, ME; D’Ottaviano, IML, A taxonomy of $${ C}$$-systems, Paraconsistency, 1-94 (2002), New York: Marcel Dekker, New York [22] Cook, SA; Reckhow, RA, The relative efficiency of propositional proof systems, J. Symb. Log., 44, 1, 36-50 (1979) · Zbl 0408.03044 [23] Copi, IM; Cohen, C.; McMahon, K., Introduction to Logic (2011), Harlow: Pearson, Harlow [24] Costa, VG; Sanz, W.; Haeusler, EH; Pinheiro, LC; Pereira, D., Peirce’s rule in a full natural deduction system, Electron. Notes Theor. Comput. Sci., 256, 5-18 (2009) · Zbl 1291.03109 [25] D’Agostino, M.; Mondadori, M., The taming of the cut. Classical refutations with analytic cut, J. Log. Comput., 4, 3, 285-319 (1994) · Zbl 0806.03037 [26] De, M.; Omori, H., Classical negation and expansions of Belnap-Dunn logic, Studia Logica, 103, 4, 825-851 (2015) · Zbl 1373.03029 [27] Degauquier, V., Partial and paraconsistent three-valued logics, Log. Log. Philos., 25, 2, 143-171 (2016) · Zbl 1402.03031 [28] Devyatkin, L.Y.: Non-classical modifications of many-valued matrices of the classical propositional logic. Part I. Logical Investigations 22(2), 27-58 (2016) (in Russian) · Zbl 1392.03033 [29] Dunn, JM, Intuitive semantics for first-degree entailment and ‘coupled trees’, Philos. Studies, 29, 3, 149-168 (1976) · Zbl 1435.03043 [30] Dunn, J.M.: The Algebra of Intensional Logics. PhD thesis, University of Pittsburgh (1966) [31] Dunn, JM, The effective equivalence of certain propositions about De Morgan lattices, J. Symb. Log., 32, 3, 433-434 (1967) [32] Ferrari, M.; Fiorentini, C.; De Nivelle, H., Proof-search in natural deduction calculus for classical propositional logic, Automated Reasoning with Analytic Tableaux and Related Methods, 237-252 (2015), Cham: Springer, Cham · Zbl 1471.68308 [33] Ferrari, M.; Fiorentini, C., Goal-oriented proof-search in natural deduction for intuitionistic propositional logic, J. Automat. Reason., 62, 1, 127-167 (2019) · Zbl 1474.03067 [34] Fitting, M.: Negation as refutation. In: Parikh, R. (ed.) Proceedings of the Fourth Annual Symposium on Logic in Computer Science, pp. 63-70. IEEE (1989) · Zbl 0716.68024 [35] Fitting, M.; Bolander, T.; Hendricks, VF; Pedersen, SA, Bilattices are nice things, Self-Reference, 53-77 (2006), Stanford: CSLI-Publications, Stanford · Zbl 1157.03308 [36] Fitting, M., First-Order Logic and Automated Theorem Proving (1996), New York: Springer, New York · Zbl 0848.68101 [37] Font, JM, Belnap’s four-valued logic and De Morgan lattices, Log. J. IGPL, 5, 3, 413-440 (1997) · Zbl 0871.03012 [38] Font, JM; Hájek, P., On Łukasiewicz’s four-valued modal logic, Studia Logica, 70, 2, 157-182 (2002) · Zbl 0998.03022 [39] Font, JM; Moussavi, M., Note on a six-valued extension of three-valued logic, J. Appl. Non-Class. Log., 3, 2, 173-187 (1993) · Zbl 0806.03019 [40] Font, JM; Rius, M., An abstract algebraic logic approach to tetravalent modal logics, J. Symb. Log., 65, 2, 481-518 (2000) · Zbl 1013.03075 [41] Gabbay, DM, Labelled Deductive Systems, Vol. I (1996), Oxford: Oxford University Press, Oxford · Zbl 0858.03004 [42] Gabbay, DM; Wansing, H., What is Negation? Applied Logic Series, vol. 13 (1999), Dordrecht: Kluwer, Dordrecht · Zbl 0957.00012 [43] Gödel, K.: Zum intuitionistischen Aussagenkalkül. Anzeiger der Akademie der Wissenschaften in Wien 69, 65-66 (1932). English translation: On the intuitionistic propositional calculus. In: Gödel, K., Collected Works, vol. I, pp. 300-301. Oxford University Press, New York (1986) [44] Hazen, AP; Pelletier, FJ, Gentzen and Jaśkowski natural deduction: fundamentally similar but importantly different, Studia Logica, 102, 6, 1103-1142 (2014) · Zbl 1344.03044 [45] Heyting, A.: Die Formalen Regeln der intuitionistischen Logik. Sitzungsberichte der Preussischen Academie der Wissenschaften zu Berlin, 42-46 (1930). English translation: The Formal Rules of Intuitionistic Logic’. In: Mancosu, P. (ed.) From Brouwer to Hilbert, pp. 311-328. Oxford University Press, New York (1998) [46] Indrzejczak, A., Introduction, Studia Logica, 102, 6, 1091-1094 (2014) · Zbl 1306.00035 [47] Ivlev, JV, A semantics for modal calculi, Bull. Sect. Logic Univ. Łódź, 17, 3-4, 114-126 (1988) · Zbl 0721.03009 [48] Jaśkowski, S.: Recherches sur le syst eme de la logique intuitioniste. Actes Congr. Internat. Philos. Sci. 6, 58-61 (1936). English translation: Investigations into the system of intuitionistic logic. Studia Logica 34(2), 117-120 (1975) · Zbl 0313.02014 [49] Karpenko, AS, Factor semantics for $$n$$-valued logics, Studia Logica, 42, 2-3, 179-185 (1983) · Zbl 0549.03015 [50] Karpenko, AS, Four-valued logics BD and DM4: expansions, Bull. Sect. Logic Univ. Łódź, 46, 1-2, 33-45 (2017) · Zbl 1423.03070 [51] Karpenko, A.; Tomova, N., Bochvar’s three-valued logic and literal paralogics: their lattice and functional equivalence, Log. Log. Philos., 26, 2, 207-235 (2017) · Zbl 1477.03074 [52] Kearns, JT, Modal semantics without possible worlds, J. Symb. Log., 46, 1, 77-86 (1981) · Zbl 0479.03011 [53] Kleene, SC, Introduction to Metamathematics (1952), New York: D. Van Nostrand, New York · Zbl 0047.00703 [54] Kleene, SC, On a notation for ordinal numbers, J. Symb. Log., 3, 4, 150-155 (1938) · JFM 64.0932.03 [55] Kooi, B.; Tamminga, A., Completeness via correspondence for extensions of the logic of paradox, Rev. Symb. Log., 5, 4, 720-730 (2012) · Zbl 1270.03045 [56] Kooi, B., Tamminga, A.: Natural deduction for truth-functional extensions of first degree entailment. Unpublished note (2015) [57] Kubyshkina, E.; Zaitsev, DV, Rational agency from a truth-functional perspective, Log. Log. Philos., 25, 4, 499-520 (2016) · Zbl 1369.03054 [58] Łukasiewicz, J., A system of modal logic, J. Computing Systems, 1, 111-149 (1953) · Zbl 0052.01003 [59] Marcos, J.; Béziau, J-Y; Coniglio, ME, The value of the two values, Logic Without Frontiers, 277-294 (2011), London: College Publication, London [60] McCarthy, J.; Braffort, P.; Hirschberg, D., A basis for a mathematical theory of computation, Computer Programming and Formal Systems, 33-70 (1963), Amsterdam: North Holland, Amsterdam [61] Méndez, JM; Robles, G., A strong and rich 4-valued modal logic without Łukasiewicz-type paradoxes, Log. Univers., 9, 4, 501-522 (2015) · Zbl 1373.03026 [62] Méndez, JM; Robles, G., Strengthening Brady’s paraconsistent 4-valued logic BN4 with truth-functional modal operators, J. Log. Lang. Inf., 25, 2, 163-189 (2016) · Zbl 1396.03045 [63] Méndez, JM; Robles, G., The logic determined by Smiley’s matrix for Anderson and Belnap’s first-degree entailment logic, J. Appl. Non-Class. Log., 26, 1, 47-68 (2016) · Zbl 1398.03109 [64] Méndez, JM; Robles, G.; Salto, F., An interpretation of Łukasiewicz’s 4-valued modal logic, J. Philos. Logic, 45, 1, 73-87 (2016) · Zbl 1347.03047 [65] Novodvorsky, A.; Smirnov, A., A shell for generic interactive proof search, J. Appl. Non-Class. Log., 8, 1-2, 123-140 (1998) · Zbl 0955.03503 [66] Omori, H.; Andreas, H.; Verdée, P., From paraconsistent logic to dialetheic logic, Logical Studies of Paraconsistent Reasoning in Science and Mathematics, 111-134 (2016), Cham: Springer, Cham · Zbl 1429.03108 [67] Omori, H.; Sano, K.; Ciuni, R.; Wansing, H.; Willkommen, C., da Costa meets Belnap and Nelson, Recent Trends in Philosophical Logic, 145-166 (2014), Cham: Springer, Cham · Zbl 1347.03052 [68] Omori, H.; Sano, K., Generalizing functional completeness in Belnap-Dunn logic, Studia Logica, 103, 5, 883-917 (2015) · Zbl 1376.03024 [69] Omori, H.; Wansing, H., 40 years of FDE: an introductory overview, Studia Logica, 105, 6, 1021-1049 (2017) · Zbl 1417.03027 [70] Petrukhin, Ya.I.: Axiomatisation of extensions of $$E_{\rm fde}$$. Unpublished manuscript (2015) (in Russian) [71] Petrukhin, Ya.I.: Correspondence analysis for first degree entailment. Logical Investigations 22(1), 108-124 (2016) · Zbl 1364.03037 [72] Petrukhin, Ya.I.: Natural deduction for Fitting’s four-valued generalizations of Kleene’s logics. Log. Univers. 11(4), 525-532 (2017) · Zbl 1385.03032 [73] Petrukhin, Ya, Natural deduction for three-valued regular logics, Log. Log. Philos., 26, 2, 197-206 (2017) · Zbl 1417.03181 [74] Petrukhin, Ya, Generalized correspondence analysis for three-valued logics, Log. Univers., 12, 3-4, 423-460 (2018) · Zbl 1435.03047 [75] Petrukhin, Ya, Natural deduction for four-valued both regular and monotonic logics, Log. Log. Philos., 27, 1, 53-66 (2018) · Zbl 1456.03048 [76] Petrukhin, Ya; Shangin, V., Automated correspondence analysis for the binary extensions of the logic of paradox, Rev. Symb. Log., 10, 4, 756-781 (2017) · Zbl 1387.03009 [77] Petrukhin, Ya; Shangin, V., Automated proof-searching for strong Kleene logic and its binary extensions via correspondence analysis, Log. Log. Philos. (2018) · Zbl 1446.03055 [78] Petrukhin, Ya; Shangin, V., Natural three-valued logics characterised by natural deduction, Log. Anal. (N.S.), 61, 244, 407-427 (2018) · Zbl 1430.03046 [79] Petrukhin, Ya; Shangin, V., On Vidal’s trivalent explanations for defective conditional in mathematics, J. Appl. Non-Class. Log., 29, 1, 64-77 (2019) · Zbl 1444.03091 [80] Pietz, A.; Rivieccio, U., Nothing but the truth, J. Philos. Logic, 42, 1, 125-135 (2013) · Zbl 1269.03027 [81] Popov, V.M.: Sequent formulations of paraconsistent logical systems. In: Smirnov, V.A. (ed.) Semantic and Syntactic Investigations of Non-Extensional Logics, pp. 285-289. Nauka, Moscow (1989) (in Russian) · Zbl 0736.03007 [82] Priest, G.; Gabbay, M.; Guenthner, F., Paraconsistent logic, Handbook of Philosophical Logic, 287-393 (2002), Dordrecht: Kluwer, Dordrecht [83] Priest, G., The logic of paradox, J. Philos. Logic, 8, 2, 219-241 (1979) · Zbl 0402.03012 [84] Pynko, AP, Functional completeness and axiomatizability within Belnap’s four-valued logic and and its expansion, J. Appl. Non-Class. Log., 9, 1, 61-105 (1999) · Zbl 1033.03017 [85] Robles, G., Reduced Routley-Meyer semantics for the logics characterized by natural implicative expansions of Kleene’s strong 3-valued matrix, Log. J. IGPL, 27, 1, 69-92 (2019) · Zbl 1494.03062 [86] Robles, G.; Méndez, JM, A companion to Brady’s 4-valued relevant logic BN4: the 4-valued logic of entailment E4, Log. J. IGPL, 24, 5, 838-858 (2016) · Zbl 1405.03061 [87] Robles, G.; Méndez, JM, Belnap-Dunn semantics for natural implicative expansions of Kleene’s strong three-valued matrix with two designated values, J. Appl. Non-Class. Log., 29, 1, 37-63 (2019) · Zbl 1444.03092 [88] Rosser, JB; Turquette, AR, Many-Valued Logics (1952), Amsterdam: Horth-Holland, Amsterdam · Zbl 0047.01503 [89] Routley, R.; Plumwood, V.; Meyer, RK; Brady, RT, Relevant Logics and their Rivals (1982), Atascadero: Ridgeview, Atascadero · Zbl 0579.03011 [90] Routley, R.; Routley, V., Semantics of first degree entailment, Noûs, 6, 4, 335-359 (1972) · Zbl 1366.03122 [91] Ruet, P.: Complete set of connectives and complete sequent calculus for Belnap’s logic. Technical report. Ecole Normale Superieure. Logic Colloquium 96, Document LIENS-96-28 (1996) [92] Sano, K.; Omori, H., An expansion of first-order Belnap-Dunn logic, Log. J. IGPL, 22, 3, 458-481 (2014) · Zbl 1342.03025 [93] Sette, AM, On propositional calculus $$P_1$$, Math. Japon., 18, 173-180 (1973) · Zbl 0289.02013 [94] Sette, A-M; Carnieli, WA, Maximal weakly-intuitionistic logics, Studia Logica, 55, 1, 181-203 (1995) · Zbl 0841.03009 [95] Shangin, VO, A precise definition of an inference (by the example of natural deduction systems for logics $$I_{\langle \alpha ,\beta \rangle } )$$, Logical Investigations, 23, 1, 83-104 (2017) · Zbl 1417.03203 [96] Shramko, Ya; Zaitsev, D.; Belikov, A., First degree entailment and its relatives, Studia Logica, 105, 6, 1291-1317 (2017) · Zbl 1417.03182 [97] Shramko, Ya; Zaitsev, D.; Belikov, A., The Fmla-Fmla axiomatizations of the exactly true and non-falsity logics and some of their cousins, J. Philos. Logic (2018) · Zbl 1457.03051 [98] Shramko, Ya; Wansing, H., Truth and Falsehood. An Inquiry into Generalized Logical Values. Trends in Logic—Studia Logica Library, vol. 36 (2012), Dordrecht: Springer, Dordrecht · Zbl 1251.03002 [99] Sieg, W.; Byrnes, J., Normal natural deduction proofs (in classical logic). Natural deduction, Studia Logica, 60, 1, 67-106 (1998) · Zbl 0954.03015 [100] Sieg, W.; Pfenning, F., Note by the guest editors, Studia Logica, 60, 1, 1 (1998) [101] Slaney, J.K.: The implications of paraconsistency. In: Mylopoulos, J., Reiter, R. (eds.) Proceedings of the 12th International Joint Conference on Artificial Intelligence, vol. 2, pp. 1052-1057. Morgan Kaufmann, Sydney (1991) · Zbl 0755.03009 [102] Sotirov, V., Non-classical operations hidden in classical logic, J. Appl. Non-Class. Log., 18, 2-3, 309-324 (2008) · Zbl 1181.03026 [103] Statman, R.: Structural Complexity of Proofs. Ph.D. Dissertation, Stanford University (1974) [104] Tamminga, A., Correspondence analysis for strong three-valued logic, Logical Investigations, 20, 255-268 (2014) · Zbl 1308.03041 [105] Tamminga, AM; Tanaka, K., A natural deduction system for first degree entailment, Notre Dame J. Form. Log., 40, 2, 258-272 (1999) · Zbl 0967.03018 [106] Tomova, N., A lattice of implicative extensions of regular Kleene’s logics, Rep. Math. Logic, 47, 173-182 (2012) · Zbl 1308.03042 [107] Tomova, N.E.: Natural $$p$$-logics. Logical Investigations 17, 256-268 (2011) (in Russian) · Zbl 1244.03086 [108] Vidal, M., The defective conditional in mathematics, J. Appl. Non-Class. Log., 24, 1-2, 169-179 (2014) · Zbl 1398.03047 [109] Voishvillo, E.K.: Philosophical and Methodological Aspects of Relevant Logic. Moscow University Press, Moscow (1988) (in Russian) · Zbl 0694.03005 [110] Voishvillo, EK, A theory of logical relevance, Logique et Anal. (N.S.), 39, 155-156, 207-228 (1996) · Zbl 0973.03027 [111] Wansing, H.: Connexive logic. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy (2014). https://plato.stanford.edu/entries/logic-connexive/. Accessed 20 Oct 2017 [112] Zaitsev, D.; Shramko, Ya, Bi-facial truth: a case for generalized truth values, Studia Logica, 101, 6, 1299-1318 (2013) · Zbl 1329.03030 [113] Zaitsev, D.V.: Shramko, YaV: Logical entailment and designated values. Logical Investigations 11, 126-137 (2004) (in Russian) [114] Zaitsev, D.V.: Generalized Relevant Logic and Models of Reasoning. Doctoral (Doctor of Science) Dissertation, Lomonosov Moscow State University (2012) (in Russian) [115] Zaitsev, D.; Markin, V.; Zaitsev, D., Generalized Vasiliev-style propositions, The Logical Legacy of Nikolai Vasiliev and Modern Logic. Synthese Library (2017), Cham: Springer, Cham · Zbl 1378.03005 [116] Zaitsev, DV, Two variations on the theme of “useful four-valued logic”, J. Mult.-Valued Logic Soft Comput., 11, 3-4, 253-262 (2005) · Zbl 1070.03011 [117] Zaitsev, DV, Yet another semantics for first-degree entailment, Bull. Sect. Logic Univ. Łódź, 27, 2, 63-65 (1998)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.