A constructive proof of Skolem theorem for constructive logic
Logic in Computer Science
2023-05-18 v1
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.
Keywords
Cite
@article{arxiv.2305.10016,
title = {A constructive proof of Skolem theorem for constructive logic},
author = {Gilles Dowek and Benjamin Werner},
journal= {arXiv preprint arXiv:2305.10016},
year = {2023}
}