How many times do we need and assumption ?

TL;DR

This paper introduces a class of formulas requiring exponentially many assumptions for proof in minimal logic, highlighting implications for automated proof system design.

Contribution

It identifies formulas with exponential assumption requirements in minimal logic and analyzes their proof complexity across different proof systems.

Findings

Formulas Fn need at least 2^n assumptions in minimal logic.

In classical logic with Peirce's rule, Fn are proved with only one assumption.

These formulas have exponential-sized proofs in cut-free Sequent Calculus and Tableaux.

Abstract

In this article we present a class of formulas Fn, n in Nat, that need at least 2^n assumptions to be proved in a normal proof in Natural Deduction for purely implicational minimal propositional logic. In purely implicational classical propositional logic, with Peirce's rule, each Fn is proved with only one assumption in Natural Deduction in a normal proof. Hence, the formulas Fn have exponentially sized proofs in cut-free Sequent Calculus and Tableaux. In fact 2^n is the lower-bound for normal proofs in ND, cut-free Sequent proofs and Tableaux. We discuss the consequences of the existence of this class of formulas for designing automatic proof-procedures based on these deductive systems.