Language Maps #
Maps between first-order languages in the style of the Flypitch project, as well as several important maps between structures.
Main Definitions #
L →ᴸ L', is a map between languages, sending the symbols of one to symbols of the same kind and arity in the other.
L ≃ᴸ L', is an invertible language homomorphism.
FirstOrder.Language.withConstantsis defined so that if
A : Set M,
L.withConstants A, denoted
L[[A]], is a language which adds constant symbols for elements of
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]
A language homomorphism maps the symbols of one language to symbols of another.
Defines a map between languages defined with
The map between two sum-languages induced by maps on the two factors.
A language homomorphism is injective when all the maps between symbol types are.
L-structure along a language map
ϕ : L →ᴸ L', and then expands it
A language homomorphism is an expansion on a structure if it commutes with the interpretation of all symbols on that structure.
A language equivalence maps the symbols of one language to symbols of another bijectively.