mathlib3 documentation


Skolem Functions and Downward Löwenheim–Skolem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 first_order.language.skolem₁
@[protected, instance]

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


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

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