# Theories with Skolem function [closed]

We say an $\mathcal{L}$-theory $T$ has built in Skolem functions if for all $\mathcal{L}$-formula $\phi(x,\bar{y})$ there is a function symbol $f$ such that $T\models \forall\bar{y}(\exists x\phi(x,\bar{y} )\rightarrow \phi(f(\bar{y}),\bar{y}))$.

$\textbf{Question}.$ Let a theory $T$ have built in Skolem functions. How can we prove that $T$ has $\forall$-axiomatization?

## closed as off-topic by Leucippus, user91500, E. Joseph, Namaste, Daniel W. FarlowNov 4 '16 at 16:14

This question appears to be off-topic. The users who voted to close gave this specific reason:

• "This question is missing context or other details: Please improve the question by providing additional context, which ideally includes your thoughts on the problem and any attempts you have made to solve it. This information helps others identify where you have difficulties and helps them write answers appropriate to your experience level." – Leucippus, E. Joseph, Namaste
If this question can be reworded to fit the rules in the help center, please edit the question.

• I think you are referring to the idea of "Skolemization" to rid the axioms of existential quantifiers. See for example Skolem normal form. The details of your "built in Skolem functions" are needed if you intend to "prove" $T$ has universally quantified axioms only, but the idea presented in broad terms is clear enough for most purposes. – hardmath Nov 4 '16 at 7:36
• @hardmath The OP is referring to the model theoretic notion of definable Skolem functions, see here: modeltheory.wikia.com/wiki/Skolem_functions – Alex Kruckman Nov 4 '16 at 14:50

1. If a theory $T$ has built-in (also called definable) Skolem functions, then every substructure of a model of $T$ is an elementary substructure.
2. A theory $T$ has a universal axiomatization if and only if it's class of models is closed under substructure.