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

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.

31 pages; generalization of main results for calculus with cuts, added section on cut elimination, added discussion on eigenvariable condition

References in corpus (1)

• Unsound Inferences Make Proofs Shorter