Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A simplified lower bound for implicational logic

Emil Jeřábek

TL;DR

This work delivers a direct exponential lower bound for proof length in the implicational fragment of intuitionistic logic within a dag-like natural deduction framework, challenging claims that all such tautologies admit polynomial-size proofs. By adapting Kleene's slash and establishing a feasible monotone interpolation tailored to the implicational setting, the authors reduce reliance on full intuitionistic translation and provide a self-contained argument anchored in monotone circuit lower bounds. The result implies that even restricted implicational intuitionistic tautologies can require exponentially long NM_\to proofs, and it yields separations from Substitution Frege and connections to Frege/Extended Frege systems. The approach clarifies the landscape of proof complexity for nonclassical logics and presents a streamlined route to exponential lower bounds in this domain, with extensions to broader logics and full propositional language discussed as well.

Abstract

We present a streamlined and simplified exponential lower bound on the length of proofs in intuitionistic implicational logic, adapted to Gordeev and Haeusler's dag-like natural deduction.

A simplified lower bound for implicational logic

TL;DR

This work delivers a direct exponential lower bound for proof length in the implicational fragment of intuitionistic logic within a dag-like natural deduction framework, challenging claims that all such tautologies admit polynomial-size proofs. By adapting Kleene's slash and establishing a feasible monotone interpolation tailored to the implicational setting, the authors reduce reliance on full intuitionistic translation and provide a self-contained argument anchored in monotone circuit lower bounds. The result implies that even restricted implicational intuitionistic tautologies can require exponentially long NM_\to proofs, and it yields separations from Substitution Frege and connections to Frege/Extended Frege systems. The approach clarifies the landscape of proof complexity for nonclassical logics and presents a streamlined route to exponential lower bounds in this domain, with extensions to broader logics and full propositional language discussed as well.

Abstract

We present a streamlined and simplified exponential lower bound on the length of proofs in intuitionistic implicational logic, adapted to Gordeev and Haeusler's dag-like natural deduction.
Paper Structure (12 sections, 28 theorems, 64 equations)

This paper contains 12 sections, 28 theorems, 64 equations.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. An exponential lower bound
  4. Extensions
  5. Logics of unbounded branching.
  6. Full propositional language.
  7. Frege and Extended Frege.
  8. Separation from Substitution Frege.
  9. Larger bounds.
  10. Conclusion
  11. Equivalence with Frege
  12. Equivalence of dag-like and tree-like proofs

Key Result

Lemma 2.1

Let $\Pi\subseteq\mathrm{Form}$, $\varphi\in\mathrm{Form}$, and let $\Gamma$ be a finite sequence of formulas. Then

Theorems & Definitions (38)

  • Lemma 2.1: deduction theorem
  • Theorem 2.2: finite model property
  • Lemma 2.3: gor-hae:crap-ii
  • Lemma 2.4
  • Lemma 2.5
  • Theorem 2.6
  • Definition 3.1
  • Lemma 3.3
  • Definition 3.4
  • Lemma 3.6
  • ...and 28 more