Efficient elimination of Skolem functions in $\text{LK}^{\text{h}}$

TL;DR

This paper demonstrates that removing a single Skolem function from proofs in a sequent calculus increases proof length only linearly, under certain conditions, improving understanding of proof complexity in logic.

Contribution

It provides a new proof-theoretic result showing linear proof length increase when eliminating a Skolem function in a specific sequent calculus.

Findings

Proof length increases linearly with Skolem function elimination

Applicable to derivations with cuts free for the Skolem function

Uses a sequent calculus with strong locality property

Abstract

Elimination of a single Skolem function in pure logic increases the length of proofs only linearly. The result is shown for derivations with cuts that are free for the Skolem function in a sequent calculus with strong locality property.