Efficient elimination of Skolem functions in \(\text{LK}^\text{h} \) (Q2144618)

The author proposes a variant of the classical sequent calculus with structural rules admissible, denoted \(\mathrm{LK}^h\), that uses Henkin constants instead of eigenvariables. The eigenvariables of the strong sequent rules \(L\exists\) and \(R\forall\) can be considered as parameters varying over the domain of the quantification. The standard eigenvariable condition of the strong quantifier rules stipulates a weak locality condition, that the eigenvariable does not occur in the conclusion sequent, and therefore does not appear in the context of the rule. From weak locality follows that the validity of a rule depends not only on the principal formulas. Therefore, the author strengthens the use of the eigenvariables, to a strong locality condition which is independent of the context, by letting the parameters of the strong quantifier rules be tied to the introduced formula. These parameters become Henkin constants. As an example, due to the strong locality property of the eigenvariable condition, there is a straightforward derivation of the drinker paradox (Example 5.2) that would otherwise violate the standard variable condition. All propositional and strong quantifier \(\mathrm{LK}^h\)-rules are shown to be invertible with length, cut-rank, and height preserving inversion. In Section 7, cut elimination is proven via a ``non-Gentzen-style algorithm without resorting to regularization''. Note that the notion of non-Gentzen-style refers to not using a mix-rule and a proof is regular if all eigenvariables are distinct and occur only above the strong sequent rule to which the eigenvariable belongs. Cut reduction is proven through invertibility by reducing an uppermost cut of maximal rank. The notion of quasiregularity is used here in order to be able to reduce a cut on a quantified formula to cuts on subfomulas without altering the conclusion when substitution is performed. The property of deep replacement used may introduce new Henkin constants in a sequent and is a term replacement that operates also on the indices of Henkin constants. Critical cuts on quantified formulas have the corresponding Henkin constant in its conclusion. The notion of \(r\)-quasiregular proof is defined as lack of critical cuts of rank \(r\). Any proof can be transformed into a quasiregular proof by exponential increase of the height. The main purpose of the article is to consider the problem of deskolemization for \(\mathrm{LK}^h\). Namely, if assuming \(\forall x A[x, f(x)]\) as an axiom lets us derive some sequent \(S\), then find a proof of \(S\) from the axiom \(\forall x\exists y A[x, y]\) and determine the complexity of the Skolem function \(f\). The author proves that elimination of a single Skolem function from an \(\mathrm{LK}^h\)-proof with cut rules that are free for the Skolem function increases the length of the proof only linearly.