Neighbourhood and Lattice Models of Second-Order Intuitionistic Propositional Logic

• Autorzy: Kurata Toshihiko , Fujita Ken-etsu

Identyfikatory

DOI

10.3233/FI-2019-1861

• Języki publikacji: EN

Abstrakty

EN

We study a version of the Stone duality between the Alexandrov spaces and the completely distributive algebraic lattices. This enables us to present lattice-theoretical models of second-order intuitionistic propositional logic which correlates with the Kripke models introduced by Sobolev. This can be regarded as a second-order extension of the well-known correspondence between Heyting algebras and Kripke models in the semantics of intuitionistic propositional logic.

Słowa kluczowe

EN

second-order intuitionistic propositional logic; complete Heyting algebras; completeness theorem

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2019
• Tom: Vol. 170, nr 1-3
• Strony: 223--240
• Opis fizyczny: Bibliogr. 16 poz., rys.

Twórcy

autor

Kurata Toshihiko

• Faculty of Business Administration, Hosei University, 2-17-1 Fujimi, Chiyoda-ku, Tokyo 102-8160, Japan

autor

Fujita Ken-etsu

• Department of Computer Science, Gunma University, 1-5-1 Tenjin-cho, Kiryu-shi, Gunma 376-8515, Japan

Bibliografia

• [1] van Dalen D. Intuitionistic Logic. In: Gabbay DM, Guenthner F (eds.), Handbook of Philosophical Logic, volume 166 of Synthese Library. Springer, Dordrecht, 1986. doi:10.1007/978-94-009-5203-4_4.
• [2] Rasiowa H, Sikorski R. The Mathematics of Metamathematics. Państwowe Wydawnictwo Naukowe, Warszawa, 1963. ISBN-978-0900318160.
• [3] Sørensen MH, Urzyczyn P. Lectures on the Curry-Howard Isomorphism, volume 149 of Studies in Logic and the Foundations of Mathematics. Elsevier, 2006. ISBN-978-0444520777.
• [4] Sobolev SK. The intuitionistic propositional calculus with quantifiers. Matematicheskie Zametki, 1977. 22(1):69-76. English translation in Mathematical notes of the Academy of Sciences of the USSR, 1977. 22(1): 528-532. doi:10.1007/BF01147694.
• [5] Zdanowski K. On second order intuitionistic logic without a universal quantifier. Journal of Symbolic Logic, 2009. 74(1):157-167. doi:10.2178/jsl/1231082306.
• [6] Dowek G. Truth values algebras and proof normalization. In: Altenkirch T, McBride C (eds.), Types for proofs and programs, volume 4502 of Lecture Notes in Computer Science, pp. 110-124. Springer, Berlin, Heidelberg, 2007. doi:10.1007/978-3-540-74464-1_8.
• [7] Kremer P. Completeness of second-order propositional S4 and H in topological semantics. The Review of Symbolic Logic, 2018. 11(3):507-518. doi:10.1017/S1755020318000229.
• [8] Montague R. Universal grammar. Theoria, 1970. 36(3):373-398. doi:10.1111/j.1755-2567.1970.tb00434.x.
• [9] Scott D. Advice on modal logic. In: Lambert K (ed.), Philosophical Problems in Logic, volume 29 of Synthese Library. Springer, Dordrecht, 1970. doi:10.1007/978-94-010-3272-8_7.
• [10] Fujita K, Kurata T. On duality between Kripke models and lattice-theoretical models of second order intuitionistic propositional logic. Kyoto University RIMS Kokyuroku, 2011. 1729:1-8.
• [11] MacLane S. Categories for the Working Mathematician. Springer-Verlag, 1971. ISBN-978-1441931238.
• [12] Gierz G, Hofmann KH, Keimel K, Lawson JD, Mislove M, Scott DS. A Compendium of Continuous Lattices. Springer-Verlag, 1980. ISBN-978-3642676802.
• [13] Abramsky S, Jung A. Domain Theory. In: Abramsky S, Gabbay DM, Maibaum TSE (eds.), Semantic Structures, volume 3 of Handbook of Logic in Computer Science. Oxford Science Publications, 1994.
• [14] Johnstone PT. Stone Spaces. Cambridge University Press, 1982. ISBN-978-0521337793.
• [15] Raney GN. Completely distributive complete lattices. Proceedings of the American Mathematical Society, 1952. 3(5):677-680. doi:10.2307/2032165.
• [16] Winskel G. A representation of completely distributive algebraic lattices. Technical Report CMU-CS-83-154, Carnegie-Mellon University SCS, 1983.

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2019).