zbMATH — the first resource for mathematics

What is a logic translation? (English) Zbl 1255.03023
Summary: We study logic translations from an abstract perspective, without any commitment to the structure of sentences and the nature of logical entailment, which also means that we cover both proof- theoretic and model-theoretic entailment. We show how logic translations induce notions of logical expressiveness, consistency strength and sublogic, leading to an explanation of paradoxes that have been described in the literature. Connectives and quantifiers, although not present in the definition of logic and logic translation, can be recovered by their abstract properties and are preserved and reflected by translations under suitable conditions.

03B22 Abstract deductive systems
03B70 Logic in computer science
03G30 Categorical logic, topoi
68Q65 Abstract data types; algebraic specification
Full Text: DOI
[1] Adámek J., Herrlich H., Strecker G.: Abstract and Concrete Categories. Wiley, New York (1990) · Zbl 0695.18001
[2] Avron A.: Simple consequence relations. Inf. Comput. 92(1), 105–140 (1991) · Zbl 0733.03007 · doi:10.1016/0890-5401(91)90023-U
[3] Avron A., Lev I.: Canonical propositional Gentzen-type systems. In: Goré, R., Leitsch, A., Nipkow, T. (eds) IJCAR. Lecture Notes in Computer Science, vol. 2083, pp. 529–544. Springer, Heidelberg (2001) · Zbl 0988.03011
[4] Béziau J.-Y.: Classical negation can be expressed by one of its halves. Logic J. IGPL 7(2), 145–151 (1999) · Zbl 0924.03012 · doi:10.1093/jigpal/7.2.145
[5] Blackburn P., de Rijke M., Venema Y.: Modal Logic. Cambridge University Press, Cambridge (2001) · Zbl 0988.03006
[6] Blok, W.J., Pigozzi, D.: Abstract algebraic logic and the deduction theorem. Bull. Symb. Logic (to appear) · Zbl 0755.03034
[7] Borceux F.: Handbook of Categorical Algebra I–III. Cambridge University Press, Cambridge (1994) · Zbl 0911.18001
[8] Brown D.J., Suszko R.: Abstract logics. Diss. Math. 102, 9–41 (1973) · Zbl 0317.02071
[9] Caleiro C., Gonçalves R.: Equipollent logical systems. In: Béziau, J.-Y. (eds) Logica Universalis, pp. 99–112. Birkhäuser Verlag, Basel (2005) · Zbl 1081.03012
[10] Carnielli W.A., D’Ottaviano I.M.L.: Translations between logical systems: A manifesto. Log. Anal. 157, 67–82 (1997) · Zbl 0982.03006
[11] Cerioli M., Meseguer J.: May I borrow your logic? (transporting logical structures along maps). Theor. Comput. Sci. 173, 311–347 (1997) · Zbl 0901.68186 · doi:10.1016/S0304-3975(96)00160-0
[12] da Silva J.J., D’Ottaviano I.M.L., Sette A.M.: Translations between logics. In: Caicedo, X., Montenegro, C.H. (eds) Models, Algebras and Proofs. Lecture Notes in Pure and Applied Mathematics, vol. 203, pp. 435–448. Marcel Dekker, New York (1999)
[13] Diaconescu R.: Institution-independent ultraproducts. Fundam. Inform. 55, 321–348 (2003) · Zbl 1036.03055
[14] Diaconescu R.: Herbrand theorems in arbitrary institutions. Inf. Process. Lett. 90, 29–37 (2004) · Zbl 1178.68132 · doi:10.1016/j.ipl.2004.01.005
[15] Diaconescu R.: Institution-Independent Model Theory. Birkhäuser, Basel (2008) · Zbl 1144.03001
[16] Epstein R.L.: The Semantic Foundations of Logic. Volume 1: Propositional Logics, volume 35 of Nijhoff International Philosophy Series. Kluwer, Dordrecht (1990) · Zbl 0699.03001
[17] Feitosa H.A., D’Ottaviano I.M.L.: Conservative translations. Ann. Pure Appl. Logic 108(1–3), 205–227 (2001) · Zbl 0983.03007 · doi:10.1016/S0168-0072(00)00046-4
[18] Fiadeiro J., Sernadas A.: Structuring theories on consequence. In: Sannella, D., Tarlecki, A. (eds) Fifth WADT. Lecture Notes in Computer Science, vol. 332, pp. 44–72. Springer, Heidelberg (1988) · Zbl 0671.03020
[19] Futatsugi, K., Jouannaud, J.-P., Meseguer, J. (eds): Algebra, Meaning, and Computation, Essays Dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday. Lecture Notes in Computer Science, vol. 4060. Springer, Heidelberg (2006) · Zbl 1113.68005
[20] Gabbay D.M.: Semantical Investigations in Heyting’s Intuitionistic Logic. Reidel, Dordrecht (1981) · Zbl 0453.03001
[21] Gentzen G.: On the relation between intuitionist and classical arithmetic. In: Szabo, M.E. (eds) The Collected Papers of Gerhard Gentzen, 1944, pp. 53–67. North–Holland, Amsterdam (1969)
[22] Gentzen G.: Investigations into logical deduction. In: Szabo, M.E. (eds) The Collected Papers of Gerhard Gentzen, pp. 68–213. North–Holland, Amsterdam (1969)
[23] Glivenko V.: Sur quelques points de la logique de M. Brouwer. Acad. R. Belg. Bull. Cl. Sci. 15(5), 183–188 (1929) · JFM 55.0030.05
[24] Gödel K.: Eine Interpretation des intuitionistischen Aussagenkalküls. Ergeb. Math. Kolloquiums 4, 34–40 (1933) · Zbl 0007.19303
[25] Gödel K.: On intuitionistic arithmetic and number theory. In: Feferman, S. et al. (eds) K. Gödel. Collected Works, 1933, pp. 287–295. Oxford University Press, Oxford (1986)
[26] Gödel K.: The consistency of the axiom of choice and of the generalized continuum hypothesis. Proc. Natl. Acad. Sci. USA 24, 556–557 (1938) · Zbl 0020.29701 · doi:10.1073/pnas.24.12.556
[27] Goguen J.A., Burstall R.M.: A study in the foundations of programming methodology: Specifications, institutions, charters and parchments. In: Pitt, D. et al. (eds) Category Theory and Computer Programming, Lecture Notes in Computer Science, vol. 240, pp. 313–333. Springer, Heidelberg (1985) · Zbl 0615.68002
[28] Goguen, J.A., Burstall, R.M.: Institutions: abstract model theory for specification and programming. J. Assoc. Comput. Mach. 39, 95–146, 1992, Predecessor in Lecture Notes in Computer Science 164, 221–256 (1984) · Zbl 0799.68134
[29] Goguen J.A., Roşu G.: Institution morphisms. Form. Asp. Comput. 13, 274–307 (2002) · Zbl 1001.68019 · doi:10.1007/s001650200013
[30] Humberstone L.: Béziau’s translation paradox. Theoria 2, 138–181 (2005)
[31] Humberstone L.: Logical discrimination. In: Beziau, J.-Y. (eds) Logica Universalis, pp. 207–228. Birkhäuser, Switzerland (2005) · Zbl 1076.03007
[32] Kolmogorov A.N.: On the principle of excluded middle. In: Heijenoort, J. (eds) From Frege to Gödel: a source book in mathematical logic 1879–1931, 1925, pp. 414–437. Harvard University Press, Cambridge (1977)
[33] Kreowski H.-J., Mossakowski T.: Equivalence and difference of institutions: simulating Horn clause logic with based algebras. Math. Struct. Comput. Sci. 5, 189–215 (1995) · Zbl 0849.68080 · doi:10.1017/S0960129500000712
[34] Lambek J., Scott P.J.: Introduction to Higher Order Categorical Logic. Cambridge University Press, Cambridge (1986) · Zbl 0596.03002
[35] Mac Lane S.: Categories for the Working Mathematician, 2nd edn. Springer, Heidelberg (1998) · Zbl 0906.18001
[36] Lawvere, F.W.: Functional Semantics of Algebraic Theories. PhD thesis, Columbia University (1963) · Zbl 0119.25901
[37] Lawvere F.W.: Functorial semantics of elementary theories. J. Symb. Log. 31, 294–295 (1966)
[38] Meseguer, J.: General logics. In: Logic Colloquium 87, pp. 275–329. North– Holland, Amsterdam (1989) · Zbl 0691.03001
[39] Mossakowski T.: Relating Casl with other specification languages: the institution level. Theor. Comput. Sci. 286, 367–475 (2002) · Zbl 1061.68106 · doi:10.1016/S0304-3975(01)00369-3
[40] Mossakowski T., Goguen J.A., Diaconescu R., Tarlecki A.: What is a logic?. In: Beziau, J.-Y. (eds) Logica Universalis, 2nd edn, pp. 111–134. Birkhäuser, Basel (2007) · Zbl 1143.03356
[41] Mosses, P.D. (eds): CASL Reference Manual, The Complete Documentation of the Common Algebraic Specification Language. Lecture Notes in Computer Science, vol. 2960. Springer, Heidelberg (2004) · Zbl 1046.68001
[42] Peirce, C.S.: Collected Papers. Harvard (1965). In: 6 volumes; see especially Volume 2: Elements of Logic
[43] Prawitz D., Malmnäs P.E.: A survey of some connections between classical, intuitionistic and minimal logic. In: Schmidt, H. et al. (eds) Contributions to Mathematical Logic, pp. 215–229. North–Holland, Amsterdam (1968)
[44] Rasiowa H., Sikorski R.: The Mathematics of Metamathematics. Polish Scientific Publishers, Warszawa (1963) · Zbl 0122.24311
[45] Scott, D.: Rules and derived rules. In: Stenlund, S. (ed.) Logical Theory and Semantic Analysis, pp. 147–161. Reidel (1974) · Zbl 0296.02012
[46] Shoenfield J.R.: Mathematical Logic. Addison-Wesley, Reading (1967) · Zbl 0155.01102
[47] Tarlecki A.: Quasi-varieties in abstract algebraic institutions. J. Comput. Syst. Sci. 33, 333–360 (1986) · Zbl 0622.68033 · doi:10.1016/0022-0000(86)90057-7
[48] Wojcicki R.: On reconstructability of the classical propositional logic into intuitionistic logic. Bull. Acad. Pol. Sci. Sér. Sci. Math. Astronomy. Phys. 18, 421–424 (1970)
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.