mathlib documentation

model_theory.skolem

Skolem Functions and Downward Löwenheim–Skolem #

Main Definitions #

Main Results #

TODO #

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

Equations
Instances for first_order.language.skolem₁
@[protected, instance]

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

Equations

Any L.sum L.skolem₁-substructure is an elementary L-substructure.

Equations
Instances for first_order.language.substructure.elementary_skolem₁_reduct

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 κ.