A lower bound for intuitionistic logic

被引:11
作者
Hrubes, Pavel [1 ]
机构
[1] Acad Sci Czech Republ, Inst Math, CR-11567 Prague, Czech Republic
关键词
proof complexity; intuitionistic logic; modal logic;
D O I
10.1016/j.apal.2007.01.001
中图分类号
O29 [应用数学];
学科分类号
070104 ;
摘要
We give an exponential lower bound on the number of proof-lines in intuitionistic propositional logic, I L, axiomatised in the usual Frege-style fashion; i.e., we give an example of I L-tautologies A(1), A(2), ... s.t. every I L-proof of A(i) must have a number of proof-lines exponential in terms of the size of Ai. We show that the results do not apply to the system of classical logic and we obtain an exponential speed-up between classical and intuitionistic logic. (c) 2007 Elsevier B.V. All rights reserved.
引用
收藏
页码:72 / 90
页数:19
相关论文
共 50 条
  • [21] A Generalized Realizability and Intuitionistic Logic
    Konovalov, Aleksandr
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2023, 24 (02)
  • [22] A local system for intuitionistic logic
    Tiu, Alwen
    Logic for Programming, Artificial Intelligence, and Reasoning, Proceedings, 2006, 4246 : 242 - 256
  • [23] TOWARDS INTUITIONISTIC DYNAMIC LOGIC
    Degen, J. W.
    Werner, J. M.
    LOGIC AND LOGICAL PHILOSOPHY, 2006, 15 (04) : 305 - 324
  • [24] Questions and Dependency in Intuitionistic Logic
    Ciardelli, Ivano
    Iemhoff, Rosalie
    Yang, Fan
    NOTRE DAME JOURNAL OF FORMAL LOGIC, 2020, 61 (01) : 75 - 115
  • [25] Semi-intuitionistic Logic
    Manuel Cornejo, Juan
    STUDIA LOGICA, 2011, 98 (1-2) : 9 - 25
  • [26] A semantic hierarchy for intuitionistic logic
    Bezhanishvili, Guram
    Holliday, Wesley H.
    INDAGATIONES MATHEMATICAE-NEW SERIES, 2019, 30 (03): : 403 - 469
  • [27] Semi-intuitionistic Logic
    Juan Manuel Cornejo
    Studia Logica, 2011, 98 : 9 - 25
  • [28] Intuitionistic logic and Muchnik degrees
    Andrea Sorbi
    Sebastiaan A. Terwijn
    Algebra universalis, 2012, 67 : 175 - 188
  • [29] Stable Formulas in Intuitionistic Logic
    Bezhanishvili, Nick
    de Jongh, Dick
    NOTRE DAME JOURNAL OF FORMAL LOGIC, 2018, 59 (03) : 307 - 324
  • [30] Basic Intuitionistic Conditional Logic
    Weiss, Yale
    JOURNAL OF PHILOSOPHICAL LOGIC, 2019, 48 (03) : 447 - 469