ONE-VARIABLE FRAGMENTS OF FIRST-ORDER LOGICS

被引:0
|
作者
Cintula, Petr [1 ]
Metcalfe, George [2 ]
Tokuda, Naomi [2 ]
机构
[1] Czech Acad Sci, Inst Comp Sci, Prague, Czech Republic
[2] Univ Bern, Math Inst, Bern, Switzerland
基金
瑞士国家科学基金会;
关键词
first-order logic; one-variable fragment; modal logic; substructural logic; superamalgamation; sequent calculus; MACNEILLE COMPLETIONS;
D O I
10.1017/bsl.2024.22
中图分类号
O1 [数学];
学科分类号
0701 ; 070101 ;
摘要
The one-variable fragment of a first-order logic may be viewed as an "S5- like" modal logic, where the universal and existential quantifiers are replaced by box and diamond modalities, respectively. Axiomatizations of these modal logics have been obtained for special cases-notably, the modal counterparts S5 and MIPC of the one-variable fragments of first-order classical logic and first-order intuitionistic logic, respectively-but a general approach, extending beyond first-order intermediate logics, has been lacking. To this end, a sufficient criterion is given in this paper for the one-variable fragment of a semantically defined first-order logic-spanning families of intermediate, substructural, many-valued, and modal logics-to admit a certain natural axiomatization. More precisely, an axiomatization is obtained for the one-variable fragment of any first-order logic based on a variety of algebraic structures with a lattice reduct that has the superamalgamation property, using a generalized version of a functional representation theorem for monadic Heyting algebras due to Bezhanishvili and Harding. An alternative proof-theoretic strategy for obtaining such axiomatization results is also developed for first-order substructural logics that have a cut-free sequent calculus and admit a certain interpolation property.
引用
收藏
页码:253 / 278
页数:26
相关论文
共 50 条
  • [31] First-order and temporal logics for nested words
    Alur, Rajeev
    Arenas, Marcelo
    Barcelo, Pablo
    Etessami, Kousha
    Immerman, Neil
    Libkin, Leonid
    22ND ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2007, : 151 - +
  • [32] Weighted First-Order Logics over Semirings
    Mandrali, Eleni
    Rahonis, George
    ACTA CYBERNETICA, 2015, 22 (02): : 435 - 483
  • [33] Enumerating teams in first-order team logics
    Haak, Anselm
    Meier, Arne
    Muller, Fabian
    Vollmer, Heribert
    ANNALS OF PURE AND APPLIED LOGIC, 2022, 173 (10)
  • [34] ON THE SATISFIABILITY OF LOCAL FIRST-ORDER LOGICS WITH DATA
    Bollig, Benedikt
    Sangnier, Arnaud
    Stietel, Olivier
    LOGICAL METHODS IN COMPUTER SCIENCE, 2024, 20 (03)
  • [35] FIRST-ORDER AND TEMPORAL LOGICS FOR NESTED WORDS
    Alur, Rajeev
    Arenas, Marcelo
    Barcelo, Pablo
    Etessami, Kousha
    Immerman, Neil
    Libkin, Leonid
    LOGICAL METHODS IN COMPUTER SCIENCE, 2008, 4 (04)
  • [36] Fibered universal algebra for first-order logics
    Bloomfield, Colin
    Maruyama, Yoshihiro
    JOURNAL OF PURE AND APPLIED ALGEBRA, 2024, 228 (02)
  • [37] First-order logics over fixed domain
    Taylor, R. Gregory
    THEORIA-A SWEDISH JOURNAL OF PHILOSOPHY, 2022, 88 (03): : 584 - 606
  • [38] Modal logics between propositional and first-order
    Fitting, M
    JOURNAL OF LOGIC AND COMPUTATION, 2002, 12 (06) : 1017 - 1026
  • [39] First-order resolution methods for modal logics
    1600, Springer Verlag (7797 LNCS):
  • [40] On natural deduction in first-order fixpoint logics
    Szalas, Andrzej
    Fundamenta Informaticae, 1996, 26 (01) : 81 - 94