A constructive proof of Skolem theorem for constructive logic

TL;DR

This paper provides a constructive proof of Skolem's theorem within constructive logic, demonstrating that certain extensions preserve provability without adding new theorems.

Contribution

It offers a constructive proof of Skolem's theorem, establishing conservativity of specific extensions in constructive natural deduction.

Findings

Proves conservativity of extensions with Skolem functions in constructive logic

Shows that provability in first-order constructive natural deduction is preserved

Provides a constructive method for Skolemization in this setting

Abstract

If the sequent (Gamma entails forall x exists y A) is provable in first order constructive natural deduction, then the theory (Gamma, forall x (f (x)/y)A), where f is a new function symbol, is a conservative extension of Gamma.