Logic Journal of IGPL Advance Access originally published online on October 16, 2007
Logic Journal of IGPL 2008 16(2):121-153; doi:10.1093/jigpal/jzm057
Heterogeneous Fibring of Deductive Systems Via Abstract Proof Systems
SQIG-IT and Dep. Informatics, FC, U Lisbon
SQIG-IT and Dep. Mathematics, IST, TU Lisbon
SQIG-IT and Dep. Mathematics, IST, TU Lisbon
Fibring is a meta-logical constructor that applied to two logics produces a new logic whose formulas allow the mixing of symbols. Homogeneous fibring assumes that the original logics are presented in the same way (e.g via Hilbert calculi). Heterogeneous fibring, allowing the original logics to have different presentations (e.g. one presented by a Hilbert calculus and the other by a sequent calculus), has been an open problem. Herein, consequence systems are shown to be a good solution for heterogeneous fibring when one of the logics is presented in a semantic way and the other by a calculus and also a solution for the heterogeneous fibring of calculi. The new notion of abstract proof system is shown to provide a better solution to heterogeneous fibring of calculi namely because derivations in the fibring keep the constructive nature of derivations in the original logics. Preservation of compactness and semi-decidability is investigated.
Key Words: heterogeneous fibring abstract proof system preservation
References
-
1 Beckert B, Gabbay D. Fibring semantic tableaux. In: In Automated Reasoning with Analytic Tableaux and Related Methods, volume 1397 of Lecture Notes in Computer Science. (1998) Springer. 77–92.
2 Bell J, Machover M. A Course in Mathematical Logic. (1977) North-Holland.
3 Blackburn P, De Rijke M. Why combine logics? Studia Logica (1997) 59(1):5–27.[CrossRef]
4 Caleiro C, Carnielli WA, Coniglio ME, Sernadas A, Sernadas C. Fibring non-truth-functional logics: Completeness preservation. Journal of Logic, Language and Information (2003) 12(2):183–211.[CrossRef]
5 Carnielli W, Rasga J, Sernadas C. Preservation of interpolation features by fibring. In: Journal of Logic and Computation. (in print).
6 Church A, Kleene SC. Formal definitions in the theory of ordinal numbers. Fundamenta Mathematica (1937) 28:11–21.
7 Coniglio ME, Sernadas A, Sernadas C. Fibring logics with topos semantics. Journal of Logic and Computation (2003) 13(4):595–624.
8 D'Agostino M, Gabbay D. Fibred tableaux for multi-implication logics. In: In Theorem Proving with Analytic Tableaux and Related Methods, volume 1071 of Lecture Notes in Computer Science. (1996) Springer. 16–35.
9 Finger M, Gabbay D. Combining temporal logic systems. Notre Dame Journal of Formal Logic (1996) 37(2):204–232.[CrossRef]
10 Finger M, Weiss M. The unrestricted combination of temporal logic systems. Logic Journal of the IGPL (2002) 10(2):165–189.[CrossRef][Web of Science]
11 Gabbay D. Fibred semantics and the weaving of logics: Part 1. Journal of Symbolic Logic (1996) 61(4):1057–1120.[CrossRef][Web of Science]
12 Gabbay D. Fibring Logics. (1999) Oxford University Press.
13 Gabbay D, Kurucz A, Wolter F, Zakharyaschev M. Many-Dimensional Modal Logics: Theory and Applications, volume 148 of Studies in Logic and the Foundations of Mathematics. (2003) North-Holland.
14 Gabbay D, Shehtman V. Products of modal logics.I. Logic Journal of the IGPL (1998) 6(1):73–146.[CrossRef]
15 Gabbay D, Shehtman V. Products of modal logics.II. Relativised quantifiers in classical logic. Logic Journal of the IGPL (2000) 8(2):165–210.[CrossRef]
16 Gabbay D, Shehtman V. Products of modal logics.III. Products of modal and temporal logics. Studia Logica (2002) 72(2):157–183.[CrossRef]
17 Governatori G, Padmanabhan V, Sattar A. On fibring semantics for BDI logics. In: JELIA, volume 2424 of Lecture Notes in Artificial Intelligence.—Flesca S, Ianni G, eds. (2002) Springer Verlag. 198–210.
18 Kontchakov R, Lutz C, Wolter F, Zakharyaschev M. Temporalising tableaux. Studia Logica (2004) 76(1):91–134.[CrossRef]
19 Kracht M, Wolter F. Properties of independently axiomatizable bimodal logics. Journal of Symbolic Logic (1991) 56(4):1469–1485.[CrossRef][Web of Science]
20 Rasga J, Sernadas A, Sernadas C, Viganò L. Fibring labelled deduction systems. Journal of Logic and Computation (2002) 12(3):443–473.
21 Sernadas A, Sernadas C. Combining logic systems: Why, how, what for? CIM Bulletin (2003) December;15:9–14.
22 Sernadas A, Sernadas C, Zanardo A. Fibring modal first-order logics: Completeness preservation. Logic Journal of the IGPL (2002) 10(4):413–451.[CrossRef][Web of Science]
23 Sernadas C, Rasga J, Carnielli WA. Modulated fibring and the collapsing problem. Journal of Symbolic Logic (2002) 67(4):1541–1569.[CrossRef][Web of Science]
24 Thomason RH. Combinations of tense and modality. In: In Handbook of Philosophical Logic, Vol. II, volume 165 of Synthese Library. (Reidel, 1984) 135–165.
25 Troelstra AS, Schwichtenberg H. Basic Proof Theory, volume 43 of Cambridge Tracts in Theoretical Computer Science. (2000) second edition. Cambridge: Cambridge University Press.
26 Wolter F. Fusions of modal logics revisited. In: In Advances in Modal Logic, Vol. 1, volume 87 of CSLI Lecture Notes. (1998) Stanford University. 361–379.
27 Wolter F, Zakharyaschev M. Temporalizing description logics. In Frontiers of Combining Systems, 2, volume 7 (2000) Research Studies Press. 379–401.
28 Zanardo A, Sernadas A, Sernadas C. Fibring: Completeness preservation. Journal of Symbolic Logic (2001) 66(1):414–439.[CrossRef][Web of Science]
| ||||||||||||||||||||||||||||||||||||||||||||||||||