Basics on First-Order Structures #
This file defines first-order languages and structures in the style of the Flypitch project, as well as several important maps between structures.
Main Definitions #
- A
FirstOrder.Language
defines a language as a pair of functions from the natural numbers toType l
. One sendsn
to the type ofn
-ary functions, and the other sendsn
to the type ofn
-ary relations. - A
FirstOrder.Language.Structure
interprets the symbols of a givenFirstOrder.Language
in the context of a given type. - A
FirstOrder.Language.Hom
, denotedM →[L] N
, is a map from theL
-structureM
to theL
-structureN
that commutes with the interpretations of functions, and which preserves the interpretations of relations (although only in the forward direction). - A
FirstOrder.Language.Embedding
, denotedM ↪[L] N
, is an embedding from theL
-structureM
to theL
-structureN
that commutes with the interpretations of functions, and which preserves the interpretations of relations in both directions. - A
FirstOrder.Language.Equiv
, denotedM ≃[L] N
, is an equivalence from theL
-structureM
to theL
-structureN
that commutes with the interpretations of functions, and which preserves the interpretations of relations in both directions.
References #
For the Flypitch project:
- [J. Han, F. van Doorn, A formal proof of the independence of the continuum hypothesis] [flypitch_cpp]
- [J. Han, F. van Doorn, A formalization of forcing and the unprovability of the continuum hypothesis][flypitch_itp]
Languages and Structures #
For every arity, a
Type*
of functions of that arityFor every arity, a
Type*
of relations of that arity
A first-order language consists of a type of functions of every natural-number arity and a type of relations of every natural-number arity.
Instances For
The empty language has no symbols.
Instances For
The sum of two languages consists of the disjoint union of their symbols.
Instances For
The type of constants in a given language.
Instances For
The type of symbols in a given language.
Instances For
The cardinality of a language is the cardinality of its type of symbols.
Instances For
- empty_functions : ∀ (n : ℕ), IsEmpty (FirstOrder.Language.Functions L n)
There are no function symbols in the language.
A language is relational when it has no function symbols.
Instances
- empty_relations : ∀ (n : ℕ), IsEmpty (FirstOrder.Language.Relations L n)
There are no relation symbols in the language.
A language is algebraic when it has no relation symbols.
Instances
- funMap : {n : ℕ} → FirstOrder.Language.Functions L n → (Fin n → M) → M
Interpretation of the function symbols
- RelMap : {n : ℕ} → FirstOrder.Language.Relations L n → (Fin n → M) → Prop
Interpretation of the relation symbols
A first-order structure on a type M
consists of interpretations of all the symbols in a given
language. Each function of arity n
is interpreted as a function sending tuples of length n
(modeled as (Fin n → M)
) to M
, and a relation of arity n
is a function from tuples of length
n
to Prop
.
Instances
Used for defining FirstOrder.Language.Theory.ModelType.instInhabited
.
Instances For
Maps #
- toFun : M → N
The underlying function of a homomorphism of structures
- map_fun' : ∀ {n : ℕ} (f : FirstOrder.Language.Functions L n) (x : Fin n → M), FirstOrder.Language.Hom.toFun s (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (s.toFun ∘ x)
The homomorphism commutes with the interpretations of the function symbols
- map_rel' : ∀ {n : ℕ} (r : FirstOrder.Language.Relations L n) (x : Fin n → M), FirstOrder.Language.Structure.RelMap r x → FirstOrder.Language.Structure.RelMap r (s.toFun ∘ x)
The homomorphism sends related elements to related elements
A homomorphism between first-order structures is a function that commutes with the interpretations of functions and maps tuples in one structure where a given relation is true to tuples in the second structure where that relation is still true.
Instances For
A homomorphism between first-order structures is a function that commutes with the interpretations of functions and maps tuples in one structure where a given relation is true to tuples in the second structure where that relation is still true.
Instances For
- toFun : M → N
- inj' : Function.Injective s.toFun
- map_fun' : ∀ {n : ℕ} (f : FirstOrder.Language.Functions L n) (x : Fin n → M), Function.Embedding.toFun s.toEmbedding (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (s.toFun ∘ x)
The homomorphism commutes with the interpretations of the function symbols
- map_rel' : ∀ {n : ℕ} (r : FirstOrder.Language.Relations L n) (x : Fin n → M), FirstOrder.Language.Structure.RelMap r (s.toFun ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x
The homomorphism sends related elements to related elements
An embedding of first-order structures is an embedding that commutes with the interpretations of functions and relations.
Instances For
An embedding of first-order structures is an embedding that commutes with the interpretations of functions and relations.
Instances For
- toFun : M → N
- invFun : N → M
- left_inv : Function.LeftInverse s.invFun s.toFun
- right_inv : Function.RightInverse s.invFun s.toFun
- map_fun' : ∀ {n : ℕ} (f : FirstOrder.Language.Functions L n) (x : Fin n → M), Equiv.toFun s.toEquiv (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (s.toFun ∘ x)
The homomorphism commutes with the interpretations of the function symbols
- map_rel' : ∀ {n : ℕ} (r : FirstOrder.Language.Relations L n) (x : Fin n → M), FirstOrder.Language.Structure.RelMap r (s.toFun ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x
The homomorphism sends related elements to related elements
An equivalence of first-order structures is an equivalence that commutes with the interpretations of functions and relations.
Instances For
An equivalence of first-order structures is an equivalence that commutes with the interpretations of functions and relations.
Instances For
Interpretation of a constant symbol
Instances For
Given a language with a nonempty type of constants, any structure will be nonempty. This cannot
be a global instance, because L
becomes a metavariable.
The function map for FirstOrder.Language.Structure₂
.
Instances For
The relation map for FirstOrder.Language.Structure₂
.
Instances For
A structure constructor to match FirstOrder.Language₂
.
Instances For
- map_fun : ∀ (φ : F) {n : ℕ} (f : FirstOrder.Language.Functions L n) (x : Fin n → M), ↑φ (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (↑φ ∘ x)
The homomorphism commutes with the interpretations of the function symbols
- map_rel : ∀ (φ : F) {n : ℕ} (r : FirstOrder.Language.Relations L n) (x : Fin n → M), FirstOrder.Language.Structure.RelMap r x → FirstOrder.Language.Structure.RelMap r (↑φ ∘ x)
The homomorphism sends related elements to related elements
HomClass L F M N
states that F
is a type of L
-homomorphisms. You should extend this
typeclass when you extend FirstOrder.Language.Hom
.
Instances
- map_fun : ∀ (φ : F) {n : ℕ} (f : FirstOrder.Language.Functions L n) (x : Fin n → M), ↑φ (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (↑φ ∘ x)
The homomorphism commutes with the interpretations of the function symbols
- map_rel : ∀ (φ : F) {n : ℕ} (r : FirstOrder.Language.Relations L n) (x : Fin n → M), FirstOrder.Language.Structure.RelMap r (↑φ ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x
The homomorphism sends related elements to related elements
StrongHomClass L F M N
states that F
is a type of L
-homomorphisms which preserve
relations in both directions.
Instances
Not an instance to avoid a loop.
The identity map from a structure to itself.
Instances For
Composition of first-order homomorphisms.
Instances For
Composition of first-order homomorphisms is associative.
Any element of a HomClass
can be realized as a first_order homomorphism.
Instances For
A first-order embedding is also a first-order homomorphism.
Instances For
In an algebraic language, any injective homomorphism is an embedding.
Instances For
The identity embedding from a structure to itself.
Instances For
Composition of first-order embeddings.
Instances For
Composition of first-order embeddings is associative.
Any element of an injective StrongHomClass
can be realized as a first_order embedding.
Instances For
The inverse of a first-order equivalence is a first-order equivalence.
Instances For
A first-order equivalence is also a first-order embedding.
Instances For
A first-order equivalence is also a first-order homomorphism.
Instances For
The identity equivalence from a structure to itself.
Instances For
Composition of first-order equivalences.
Instances For
Composition of first-order homomorphisms is associative.
Any element of a bijective StrongHomClass
can be realized as a first_order isomorphism.
Instances For
Makes a Language.empty.Hom
out of any function.
Instances For
Makes a Language.empty.Embedding
out of any function.
Instances For
Makes a Language.empty.Equiv
out of any function.
Instances For
A structure induced by a bijection.
Instances For
A bijection as a first-order isomorphism with the induced structure on the codomain.