Compositional truth with propositional tautologies and quantifier-free correctness

被引：1
|
作者：
Wcislo, Bartosz [1 ]
机构：
[1] Univ Gdansk, Inst Philosophy, Ul Jana Bazynskiego 4, PL-80309 Gdansk, Poland
来源：
ARCHIVE FOR MATHEMATICAL LOGIC | 2024年 / 63卷 / 1-2期
关键词：
Compositional truth; Conservativeness; CT0; Tarski boundary; Propositional soundness; Disjunctive correctness;
D O I：
10.1007/s00153-023-00893-3
中图分类号：
O1 [数学];
学科分类号：
0701 ; 070101 ;
摘要：
In Cie & sacute;li & nacute;ski (J Philos Logic 39:325-337, 2010), Cie & sacute;li & nacute;ski asked whether compositional truth theory with the additional axiom that all propositional tautologies are true is conservative over Peano Arithmetic. We provide a partial answer to this question, showing that if we additionally assume that truth predicate agrees with arithmetical truth on quantifier-free sentences, the resulting theory is as strong as Delta 0-induction for the compositional truth predicate, hence non-conservative. On the other hand, it can be shown with a routine argument that the principle of quantifier-free correctness is itself conservative.
引用
收藏
页码：239 / 257
页数：19
相关论文
共 50 条
  • [41] The Effects of Adding Reachability Predicates in Quantifier-Free Separation Logic
    Demri, Stephane
    Lozes, Etienne
    Mansutti, Alessio
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2021, 22 (02)
  • [42] DYNAMIC CONTACT ALGEBRAS AND QUANTIFIER-FREE LOGICS FOR SPACE AND TIME
    Dimitrov, Plamen
    Vakarelov, Dimiter
    SIBERIAN ELECTRONIC MATHEMATICAL REPORTS-SIBIRSKIE ELEKTRONNYE MATEMATICHESKIE IZVESTIYA, 2018, 15 : 1103 - 1144
  • [43] A quantifier-free SMT encoding of non-linear hybrid automata
    Cimatti, Alessandro
    Mover, Sergio
    Tonetta, Stefano
    PROCEEDINGS OF THE 12TH CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN (FMCAD 2012), 2012, : 187 - 195
  • [44] Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory
    Stevens, Lukas
    AUTOMATED DEDUCTION, CADE 29, 2023, 14132 : 491 - 508
  • [45] Test selection criteria for quantifier-free first-order specifications
    Aiguier, Marc
    Arnould, Agnes
    Le Gall, Pascale
    Longuet, Delphine
    INTERNATIONAL SYMPOSIUM ON FUNDAMENTALS OF SOFTWARE ENGINEERING, PROCEEDINGS, 2007, 4767 : 144 - +
  • [46] Deciding quantifier-free Presburger formulas using parameterized solution bounds
    Seshia, SA
    Bryant, RE
    19TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2004, : 100 - 109
  • [47] Universal Invariant Checking of Parametric Systems with Quantifier-free SMT Reasoning
    Cimatti, Alessandro
    Griggio, Alberto
    Redondi, Gianluca
    AUTOMATED DEDUCTION, CADE 28, 2021, 12699 : 131 - 147
  • [48] Duality-Based Interpolation for Quantifier-Free Equalities and Uninterpreted Functions
    Alt, Leonardo
    Hyvaerinen, Antti E. J.
    Asadi, Sepideh
    Sharygina, Natasha
    PROCEEDINGS OF THE 17TH CONFERENCE ON FORMAL METHODS IN COMPUTER AIDED DESIGN (FMCAD 2017), 2017, : 39 - 46
  • [49] Computational complexity of quantifier-free negationless theory of field of rational numbers
    Kossovski, N
    ANNALS OF PURE AND APPLIED LOGIC, 2002, 113 (1-3) : 175 - 180
  • [50] Quantifier-free epistemic term-modal logic with assignment operator
    Wang, Yanjing
    Wei, Yu
    Seligman, Jeremy
    ANNALS OF PURE AND APPLIED LOGIC, 2022, 173 (03)
12345