Density elimination and rational completeness for first-order logics

被引:4
|
作者
Ciabattoni, Agata [1 ]
Metcalfe, George [2 ]
机构
[1] Vienna Univ Technol, Inst Discrete Math & Geometry, Wiedner Hauptstr 8-10, A-1040 Vienna, Austria
[2] Vanderbilt Univ, Dept Math, Nashville, TN 37240 USA
来源
LOGICAL FOUNDATIONS OF COMPUTER SCIENCE, PROCEEDINGS | 2007年 / 4514卷
基金
奥地利科学基金会;
关键词
D O I
10.1007/978-3-540-72734-7_10
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
Density elimination by substitutions is introduced as a uniform method for removing applications of the Takeuti-Titani density rule from proofs in first-order hypersequent calculi. For a large class of calculi, density elimination by this method is guaranteed by known sufficient conditions for cut-elimination. Moreover, adding the density rule to any axiomatic extension of a simple first order logic gives a logic that is rational complete; i.e., complete with respect to linearly and densely ordered algebras: a precursor to showing that it is a fuzzy logic (complete for algebras with a real unit interval lattice reduct). Hence the sufficient conditions for cut-elimination guarantee rational completeness for a large class of first-order substructural logics.
引用
收藏
页码:132 / +
页数:2
相关论文
共 50 条
  • [31] A PROOF OF COMPLETENESS FOR CONTINUOUS FIRST-ORDER LOGIC
    Ben Yaacov, Itai
    Pedersen, Arthur Paul
    JOURNAL OF SYMBOLIC LOGIC, 2010, 75 (01) : 168 - 190
  • [32] Completeness for a First-Order Abstract Separation Logic
    Hou, Zhe
    Tiu, Alwen
    PROGRAMMING LANGUAGES AND SYSTEMS, APLAS 2016, 2016, 10017 : 444 - 463
  • [33] 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 - +
  • [34] On the completeness of the root vectors of first-order systems
    M. M. Malamud
    L. L. Oridoroga
    Doklady Mathematics, 2010, 82 : 899 - 904
  • [35] Weighted First-Order Logics over Semirings
    Mandrali, Eleni
    Rahonis, George
    ACTA CYBERNETICA, 2015, 22 (02): : 435 - 483
  • [36] STRUCTURAL COMPLETENESS OF FIRST-ORDER PREDICATE CALCULUS
    POGORZEL.WA
    PRUCNAL, T
    BULLETIN DE L ACADEMIE POLONAISE DES SCIENCES-SERIE DES SCIENCES MATHEMATIQUES ASTRONOMIQUES ET PHYSIQUES, 1974, 22 (03): : 215 - 217
  • [37] ON THE SATISFIABILITY OF LOCAL FIRST-ORDER LOGICS WITH DATA
    Bollig, Benedikt
    Sangnier, Arnaud
    Stietel, Olivier
    LOGICAL METHODS IN COMPUTER SCIENCE, 2024, 20 (03)
  • [38] Enumerating teams in first-order team logics
    Haak, Anselm
    Meier, Arne
    Muller, Fabian
    Vollmer, Heribert
    ANNALS OF PURE AND APPLIED LOGIC, 2022, 173 (10)
  • [39] Decidable fragments of first-order modal logics
    Wolter, F
    Zakharyaschev, M
    JOURNAL OF SYMBOLIC LOGIC, 2001, 66 (03) : 1415 - 1438
  • [40] 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)