A Simple Proof of Completeness and Cut-admissibility for Propositional Godel Logic

被引:5
|
作者
Avron, Arnon [1 ]
机构
[1] Tel Aviv Univ, Sch Comp Sci, IL-69978 Tel Aviv, Israel
关键词
Propositional Godel Logic; Hypersequents; Strong cut-elimination; Completeness;
D O I
10.1093/logcom/exp055
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
We provide a constructive, direct and simple proof of the completeness of the cut-free part of the hypersequential calculus HG for Godel logic (thereby proving both completeness of the calculus for its standard semantics, and the admissibility of the cut rule in the full calculus). We then extend the results and proofs to derivations from assumptions, showing that such derivations can be confined to those in which cuts are made only on formulas which occur in the assumptions. The article is self-contained, and no previous knowledge concerning HG (or even Godel logic) is needed for understanding it.
引用
收藏
页码:813 / 821
页数:9
相关论文
共 50 条
  • [21] A DISCUSSION OF SOME COMPLETENESS PROOFS FOR PROPOSITIONAL LOGIC
    WASSERMA.HC
    JOURNAL OF SYMBOLIC LOGIC, 1967, 32 (03) : 446 - &
  • [22] FUNCTIONAL COMPLETENESS FOR SUBSYSTEMS OF INTUITIONISTIC PROPOSITIONAL LOGIC
    WANSING, H
    JOURNAL OF PHILOSOPHICAL LOGIC, 1993, 22 (03) : 303 - 321
  • [23] CRITERION OF FUNCTIONAL COMPLETENESS IN INTUITIONISTIC PROPOSITIONAL LOGIC
    RATSA, MF
    DOKLADY AKADEMII NAUK SSSR, 1971, 201 (04): : 794 - &
  • [24] Propositional proof compressions and DNF logic
    Gordeev, L.
    Haeusler, E. H.
    Pereira, L. C.
    LOGIC JOURNAL OF THE IGPL, 2011, 19 (01) : 62 - 86
  • [25] Proof complexity of propositional default logic
    Beyersdorff, Olaf
    Meier, Arne
    Mueller, Sebastian
    Thomas, Michael
    Vollmer, Heribert
    ARCHIVE FOR MATHEMATICAL LOGIC, 2011, 50 (7-8): : 727 - 742
  • [26] Proof Complexity of Propositional Default Logic
    Beyersdorff, Olaf
    Meier, Arne
    Mueller, Sebastian
    Thomas, Michael
    Vollmer, Heribert
    THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2010, PROCEEDINGS, 2010, 6175 : 30 - +
  • [27] Proof systems for effectively propositional logic
    Navarro, Juan Antonio
    Voronkov, Andrei
    AUTOMATED REASONING, PROCEEDINGS, 2008, 5195 : 426 - 440
  • [28] CUT ELIMINATION IN INFINITE PROPOSITIONAL LOGIC
    TAIT, WW
    JOURNAL OF SYMBOLIC LOGIC, 1966, 31 (01) : 151 - &
  • [29] A Quantitative Method of n-valued Godel Propositional Logic
    Li, Jun
    Zhou, Yan
    2011 INTERNATIONAL CONFERENCE ON FUZZY SYSTEMS AND NEURAL COMPUTING (FSNC 2011), VOL II, 2011, : 81 - 84
  • [30] Proof complexity of propositional default logic
    Olaf Beyersdorff
    Arne Meier
    Sebastian Müller
    Michael Thomas
    Heribert Vollmer
    Archive for Mathematical Logic, 2011, 50 : 727 - 742