Skolem Functions and Downward Löwenheim–Skolem #

Main Definitions #

Main Results #


A language consisting of Skolem functions for another language. Called skolem₁ because it is the first step in building a Skolemization of a language.

Instances For

    The structure assigning each function symbol of L.skolem₁ to a skolem function generated with choice.

    The Downward Löwenheim–Skolem theorem : If s is a set in an L-structure M and κ an infinite cardinal such that max (#s, L.card) ≤ κ and κ ≤ # M, then M has an elementary substructure containing s of cardinality κ.