Finite relational vocabularies and structures
Lax512892.RelationalStructures · concepts/Lax512892/RelationalStructures.lean · lax-512892
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
A finite relational vocabulary consists of finitely many relation symbols, each with a specified finite arity, and finitely many constant symbols. A structure interprets every relation symbol as a relation of the corresponding arity and every constant symbol as an element of its carrier.
This is the notion of relational vocabulary used in the stated version of Gaifman's theorem. Function symbols of positive arity are deliberately absent. The theorem will quantify over finite carrier types, while the definitions in this file make sense over any carrier type.
Concept map
Lean source view on GitHub
| 1 | import Mathlib.Data.Fin.Tuple.Basic |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Finite relational vocabularies and structures |
| 6 | type: definition |
| 7 | --- |
| 8 | A finite relational vocabulary consists of finitely many relation symbols, each |
| 9 | with a specified finite arity, and finitely many constant symbols. A structure |
| 10 | interprets every relation symbol as a relation of the corresponding arity and |
| 11 | every constant symbol as an element of its carrier. |
| 12 | |
| 13 | This is the notion of relational vocabulary used in the stated version of |
| 14 | Gaifman's theorem. Function symbols of positive arity are deliberately absent. |
| 15 | The theorem will quantify over finite carrier types, while the definitions in |
| 16 | this file make sense over any carrier type. |
| 17 | |
| 18 | # Formalization notes |
| 19 | |
| 20 | The relation symbols are positions in `relationArities`; the entry at a position |
| 21 | is that symbol's arity. Thus finiteness is built into the type of a vocabulary, |
| 22 | rather than imposed by a typeclass side condition. Constants are represented by |
| 23 | `Fin constantCount`. A structure on an empty carrier can exist exactly when the |
| 24 | vocabulary has no constants, matching the usual convention. |
| 25 | -/ |
| 26 | |
| 27 | namespace Lax512892.RelationalStructures |
| 28 | |
| 29 | /-- A finite relational vocabulary: a finite list of relation arities and a |
| 30 | finite number of constant symbols. -/ |
| 31 | structure Vocabulary where |
| 32 | /-- One arity for each relation symbol. -/ |
| 33 | relationArities : List ℕ |
| 34 | /-- The number of constant symbols. -/ |
| 35 | constantCount : ℕ |
| 36 | |
| 37 | namespace Vocabulary |
| 38 | |
| 39 | /-- The finite type of relation symbols of `σ`. -/ |
| 40 | abbrev Relation (σ : Vocabulary) := Fin σ.relationArities.length |
| 41 | |
| 42 | /-- The arity of a relation symbol. -/ |
| 43 | def arity (σ : Vocabulary) (R : σ.Relation) : ℕ := |
| 44 | σ.relationArities.get R |
| 45 | |
| 46 | /-- The finite type of constant symbols of `σ`. -/ |
| 47 | abbrev Constant (σ : Vocabulary) := Fin σ.constantCount |
| 48 | |
| 49 | end Vocabulary |
| 50 | |
| 51 | /-- An interpretation of the relational vocabulary `σ` on the carrier `M`. -/ |
| 52 | structure Structure (σ : Vocabulary) (M : Type*) where |
| 53 | /-- Interpretation of every relation symbol as a relation of its arity. -/ |
| 54 | relation : (R : σ.Relation) → (Fin (σ.arity R) → M) → Prop |
| 55 | /-- Interpretation of every constant symbol. -/ |
| 56 | constant : σ.Constant → M |
| 57 | |
| 58 | end Lax512892.RelationalStructures |
| 59 |
Formalization notes
The relation symbols are positions in ; the entry at a position is that symbol's arity. Thus finiteness is built into the type of a vocabulary, rather than imposed by a typeclass side condition. Constants are represented by . A structure on an empty carrier can exist exactly when the vocabulary has no constants, matching the usual convention.
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments