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

Petrukhin, Yaroslav; Shangin, Vasily

Eur. J. Math. 6, No. 4, 1452-1495 (2020).

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

Keywords:

correspondence analysis; natural deduction; proof-searching; first degree entailment; proof theory; four-valued logic; \(n\)-sequent systems; ordinary sequent calculi

Citations:

Zbl 1270.03045

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)