Tagged interpretations

Reductions between problems often build structures whose elements are of several kinds: the literal vertices and the clause gadgets of a graph built from a formula, the variables and the clauses of a formula built from a structure. A tagged interpretation I of L' in L (Cslib.Logic.FO.TaggedInterpretation) has a finite type T of tags and, for each tag t, a type ι t of coordinates and a domain formula; the interpreted structure I.Model M is the disjoint union over the tags t of the tuples ι t → M satisfying the domain formula of t, and a relation symbol is defined, for each choice of tags of its arguments, by a formula in the coordinates of the arguments. Senellart and Gnatenko's interpretations are tagged in this way, with the same coordinates Fin dim for every tag Senellart and Gnatenko.

The first-order interpretations of this library (Cslib.Logic.FO.Interpretation) are untagged, and the structures are unordered and have no constants, so a tag cannot be named by a fixed element. It is named by an equality pattern instead: the coordinates of the compiled interpretation I.toInterpretation S are two coordinates p ≠ q, a coordinate per tag, equal to q at the tag of the element and to p at the others, and the coordinates of every tag, those of the other tags equal to p. Every ordered pair p ≠ q thus carries a copy of I.Model M, and the compiled structure is isomorphic to Copies J (I.Model M), the disjoint union of copies indexed by the pairs J (Cslib.Logic.FO.TaggedInterpretation.copiesEquiv). A structure with at most one element has no such pair; on it, the compiled interpretation is a given interpretation S of dimension one (Cslib.Logic.FO.TaggedInterpretation.subsingletonEquiv).

So a tagged interpretation gives an order-free reduction to every class that is closed under isomorphism and under taking a positive number of disjoint copies, such as satisfiability of formulas in conjunctive normal form or colorability of graphs (Cslib.Logic.FO.Reduces.of_tagged).

Binary relations of tagged interpretations are conveniently defined by templates (Cslib.Logic.FO.TaggedInterpretation.Template): a template from tag t relates an element of tag t whose coordinates satisfy a guard to the elements of a target tag whose coordinates are copied from it, or are arbitrary.

Main definitions

• Cslib.Logic.FO.TaggedInterpretation, Cslib.Logic.FO.TaggedInterpretation.Model, Cslib.Logic.FO.TaggedInterpretation.Model.toSigma, Cslib.Logic.FO.subsingletonFormula: tagged interpretations, the structures they interpret, and the subsingleton guard formula.
• Cslib.Logic.FO.TaggedInterpretation.reindex, Cslib.Logic.FO.TaggedInterpretation.reindexEquiv: renaming the tags and the induced isomorphism.
• Cslib.Logic.FO.Copies, Cslib.Logic.FO.Copies.equivProd, Cslib.Logic.FO.CopyInvariant: disjoint copies of a structure, their product equivalence, and the classes closed under them.
• Cslib.Logic.FO.TaggedInterpretation.Coord, Cslib.Logic.FO.TaggedInterpretation.Coord.tag, Cslib.Logic.FO.TaggedInterpretation.Coord.data, Cslib.Logic.FO.TaggedInterpretation.domainAt, Cslib.Logic.FO.TaggedInterpretation.relAt, Cslib.Logic.FO.TaggedInterpretation.toInterpretation: coordinates, component formulas, and the compiled first-order interpretation.
• Cslib.Logic.FO.TaggedInterpretation.Pairs, Cslib.Logic.FO.TaggedInterpretation.coords, Cslib.Logic.FO.TaggedInterpretation.ofCopies: distinct-element pairs, coordinate encoding, and the map from copies into the compiled model.
• Cslib.Logic.FO.TaggedInterpretation.Template, Cslib.Logic.FO.TaggedInterpretation.Template.Compat, Cslib.Logic.FO.TaggedInterpretation.Template.Holds, Cslib.Logic.FO.TaggedInterpretation.Template.formula, Cslib.Logic.FO.TaggedInterpretation.Template.listFormula, Cslib.Logic.FO.TaggedInterpretation.binaryRel: templates and formulas for binary relations.

Main results

• Cslib.Logic.FO.TaggedInterpretation.copiesEquiv: on a structure with two distinct elements, the compiled interpretation is a disjoint union of copies of the tagged one.
• Cslib.Logic.FO.TaggedInterpretation.subsingletonEquiv: on a structure with at most one element, it is the given interpretation of dimension one.
• Cslib.Logic.FO.Reduces.of_tagged: tagged interpretations give order-free reductions to classes closed under isomorphism and copies.
• Cslib.Logic.FO.TaggedInterpretation.Template.realize_formula: the semantics of templates.

References

• N. Immerman, Descriptive Complexity
• P. Senellart and A. Gnatenko, Descriptive Complexity in Lean: Completeness by First-Order Reductions

structure Cslib.Logic.FO.TaggedInterpretation (L : FirstOrder.Language) (L' : FirstOrder.Language) (T : Type u_1) (ι : T → Type u_2) : Type (max (max (max (max u u_1) u_2) v) v')

A tagged interpretation of L' in L: for each tag t a domain formula in the coordinates ι t, and for each relation symbol of arity n and each choice of tags of its n arguments a formula in their coordinates.

• domain (t : T) : L.Formula (ι t)

  The domain formula of each tag.

• rel {n : ℕ} : L'.Relations n → (ts : Fin n → T) → L.Formula ((j : Fin n) × ι (ts j))

  The formula defining a relation symbol among arguments of the given tags.

def Cslib.Logic.FO.subsingletonFormula (L : FirstOrder.Language) (α : Type u_1) : L.Formula α

In a structure with at most one element: the formula ∀ x y, x = y.

@[simp]

theorem Cslib.Logic.FO.realize_subsingletonFormula {L : FirstOrder.Language} {α : Type u_1} {M : Type w} [L.Structure M] (v : α → M) : (subsingletonFormula L α).Realize v ↔ Subsingleton M

subsingletonFormula L α holds in M if and only if M is a Subsingleton.

def Cslib.Logic.FO.TaggedInterpretation.Model {L : FirstOrder.Language} {L' : FirstOrder.Language} {T : Type u_1} {ι : T → Type u_2} (I : TaggedInterpretation L L' T ι) (M : Type w) [L.Structure M] : Type (max (max u_2 w) u_1)

The universe of the structure interpreted by I in M: for each tag, the tuples satisfying its domain formula.

instance Cslib.Logic.FO.TaggedInterpretation.instFiniteModel {L : FirstOrder.Language} {L' : FirstOrder.Language} {T : Type u_1} {ι : T → Type u_2} {I : TaggedInterpretation L L' T ι} {M : Type w} [L.Structure M] [Finite T] [∀ (t : T), Finite (ι t)] [Finite M] : Finite (I.Model M)

When T, each ι t, and M are finite, the tagged model I.Model M is finite.

def Cslib.Logic.FO.TaggedInterpretation.Model.toSigma {L : FirstOrder.Language} {L' : FirstOrder.Language} {T : Type u_1} {ι : T → Type u_2} {I : TaggedInterpretation L L' T ι} {M : Type w} [L.Structure M] (e : I.Model M) : (t : T) × (ι t → M)

The tag and coordinates of an element of the interpreted structure.

theorem Cslib.Logic.FO.TaggedInterpretation.Model.ext_toSigma {L : FirstOrder.Language} {L' : FirstOrder.Language} {T : Type u_1} {ι : T → Type u_2} {I : TaggedInterpretation L L' T ι} {M : Type w} [L.Structure M] {e e' : I.Model M} (h : e.toSigma = e'.toSigma) : e = e'

Two elements of I.Model M with equal toSigma projections are equal.

@[instance_reducible]

instance Cslib.Logic.FO.TaggedInterpretation.instStructureModel {L : FirstOrder.Language} {L' : FirstOrder.Language} {T : Type u_1} {ι : T → Type u_2} {I : TaggedInterpretation L L' T ι} {M : Type w} [L.Structure M] [L'.IsRelational] : L'.Structure (I.Model M)

The structure interpreted by I: a relation holds of some elements when its defining formula for their tags holds of their coordinates.

theorem Cslib.Logic.FO.TaggedInterpretation.relMap_model {L : FirstOrder.Language} {L' : FirstOrder.Language} {T : Type u_1} {ι : T → Type u_2} {I : TaggedInterpretation L L' T ι} {M : Type w} [L.Structure M] [L'.IsRelational] {n : ℕ} (R : L'.Relations n) (xs : Fin n → I.Model M) : FirstOrder.Language.Structure.RelMap R xs ↔ (I.rel R fun (j : Fin n) => (xs j).fst).Realize fun (p : (j : Fin n) × ι (xs j).fst) => ↑(xs p.fst).snd p.snd

A relation R holds on xs in I.Model M iff I.rel R for their tags holds of their coordinates.

Renaming tags

def Cslib.Logic.FO.TaggedInterpretation.reindex {L : FirstOrder.Language} {L' : FirstOrder.Language} {T : Type u_1} {T' : Type u_2} {ι : T → Type u_3} (I : TaggedInterpretation L L' T ι) (e : T ≃ T') : TaggedInterpretation L L' T' (ι ∘ ⇑e.symm)

The tagged interpretation with tags renamed along e.

def Cslib.Logic.FO.TaggedInterpretation.reindexEquiv {L : FirstOrder.Language} {L' : FirstOrder.Language} {T : Type u_1} {T' : Type u_2} {ι : T → Type u_3} (I : TaggedInterpretation L L' T ι) [L'.IsRelational] (e : T ≃ T') (M : Type w) [L.Structure M] : L'.Equiv ((I.reindex e).Model M) (I.Model M)

Renaming the tags of a tagged interpretation does not change the interpreted structure, up to isomorphism.

Disjoint copies

structure Cslib.Logic.FO.Copies (J : Type u_1) (N : Type u_2) : Type (max u_1 u_2)

The disjoint union of copies of N indexed by J: a relation holds of some elements of one copy when it holds of them in N.

• idx : J

  The copy containing the element.

• val : N

  The element of N it is a copy of.

def Cslib.Logic.FO.Copies.equivProd {J : Type u_1} {N : Type u_2} : Copies J N ≃ J × N

The copies, as pairs.

instance Cslib.Logic.FO.Copies.instFinite {J : Type u_1} {N : Type u_2} [Finite J] [Finite N] : Finite (Copies J N)

When J and N are finite, Copies J N is finite.

@[instance_reducible]

instance Cslib.Logic.FO.Copies.instStructureOfIsRelational {L' : FirstOrder.Language} {J : Type u_1} {N : Type u_2} [L'.IsRelational] [L'.Structure N] : L'.Structure (Copies J N)

Relational structure on Copies J N: a relation holds on a tuple iff all arguments lie in the same copy and the relation holds on their underlying values in N.

theorem Cslib.Logic.FO.Copies.relMap_copies {L' : FirstOrder.Language} {J : Type u_1} {N : Type u_2} [L'.IsRelational] [L'.Structure N] {n : ℕ} (R : L'.Relations n) (xs : Fin n → Copies J N) : FirstOrder.Language.Structure.RelMap R xs ↔ (∀ (i j : Fin n), (xs i).idx = (xs j).idx) ∧ FirstOrder.Language.Structure.RelMap R fun (i : Fin n) => (xs i).val

A relation R holds on xs in Copies J N iff all xs i share the same copy index and R holds on i ↦ (xs i).val in N.

theorem Cslib.Logic.FO.Copies.relMap_copies_two {L' : FirstOrder.Language} {J : Type u_1} {N : Type u_2} [L'.IsRelational] [L'.Structure N] (R : L'.Relations 2) (a b : Copies J N) : FirstOrder.Language.Structure.RelMap R ![a, b] ↔ a.idx = b.idx ∧ FirstOrder.Language.Structure.RelMap R ![a.val, b.val]

A binary relation holds of two elements of the copies when they are in the same copy and related in N.

theorem Cslib.Logic.FO.Copies.relMap_copies_one {L' : FirstOrder.Language} {J : Type u_1} {N : Type u_2} [L'.IsRelational] [L'.Structure N] (R : L'.Relations 1) (a : Copies J N) : FirstOrder.Language.Structure.RelMap R ![a] ↔ FirstOrder.Language.Structure.RelMap R ![a.val]

A unary relation in a copy holds exactly when it holds of the underlying element.

theorem Cslib.Logic.FO.Copies.ncard_set_val {J : Type u_1} {N : Type u_2} (s : Set N) : {x : Copies J N | x.val ∈ s}.ncard = Nat.card J * s.ncard

The copies of a set have cardinality the number of copies times its cardinality.

def Cslib.Logic.FO.CopyInvariant {L' : FirstOrder.Language} [L'.IsRelational] (K : Set (CategoryTheory.Bundled L'.Structure)) : Prop

A class of structures is invariant under copies when a finite structure belongs to it exactly when the disjoint union of a finite positive number of copies of it does.

The compiled interpretation

@[reducible, inline]

abbrev Cslib.Logic.FO.TaggedInterpretation.Coord (T : Type) (ι : T → Type) : Type

The coordinates of the compiled interpretation: the two coordinates p and q of a copy, a coordinate for each tag, and the coordinates of every tag.

@[reducible, inline]

abbrev Cslib.Logic.FO.TaggedInterpretation.Coord.p {T : Type} {ι : T → Type} : Coord T ι

The first coordinate of a copy.

@[reducible, inline]

abbrev Cslib.Logic.FO.TaggedInterpretation.Coord.q {T : Type} {ι : T → Type} : Coord T ι

The second coordinate of a copy, distinct from the first.

@[reducible, inline]

abbrev Cslib.Logic.FO.TaggedInterpretation.Coord.tag {T : Type} {ι : T → Type} (t : T) : Coord T ι

The coordinate of a tag, equal to q at the tag of an element and to p at the others.

@[reducible, inline]

abbrev Cslib.Logic.FO.TaggedInterpretation.Coord.data {T : Type} {ι : T → Type} (σ : (t : T) × ι t) : Coord T ι

A coordinate of a tag, equal to p unless the element has this tag.

noncomputable def Cslib.Logic.FO.TaggedInterpretation.domainAt {L : FirstOrder.Language} {L' : FirstOrder.Language} {T : Type} {ι : T → Type} [Finite T] [∀ (t : T), Finite (ι t)] (I : TaggedInterpretation L L' T ι) (t : T) : L.Formula (Coord T ι)

The domain formula of the compiled interpretation on elements of tag t: the coordinates p and q are distinct, the coordinate of each tag is q at t and p elsewhere, the coordinates of the other tags are p, and the coordinates of t satisfy its domain formula.

noncomputable def Cslib.Logic.FO.TaggedInterpretation.relAt {L : FirstOrder.Language} {L' : FirstOrder.Language} {T : Type} {ι : T → Type} [Finite T] (I : TaggedInterpretation L L' T ι) {n : ℕ} (R : L'.Relations n) : L.Formula (Fin n × Coord T ι)

The formula defining a relation symbol in the compiled interpretation: all arguments belong to the same copy, and the formula of I for their tags holds of their coordinates.

noncomputable def Cslib.Logic.FO.TaggedInterpretation.toInterpretation {L : FirstOrder.Language} {L' : FirstOrder.Language} {T : Type} {ι : T → Type} [Finite T] [∀ (t : T), Finite (ι t)] (I : TaggedInterpretation L L' T ι) (S : Interpretation L L' Unit) : Interpretation L L' (Coord T ι)

The compiled interpretation of a tagged interpretation I, using the interpretation S of dimension one on structures with at most one element.

theorem Cslib.Logic.FO.TaggedInterpretation.realize_domainAt {L : FirstOrder.Language} {L' : FirstOrder.Language} {T : Type} {ι : T → Type} [Finite T] [∀ (t : T), Finite (ι t)] {I : TaggedInterpretation L L' T ι} {M : Type w} [L.Structure M] (t : T) (c : Coord T ι → M) : (I.domainAt t).Realize c ↔ c Coord.p ≠ c Coord.q ∧ (∀ (t' : T), c (Coord.tag t') = if t' = t then c Coord.q else c Coord.p) ∧ (∀ (σ : (t' : T) × ι t'), σ.fst ≠ t → c (Coord.data σ) = c Coord.p) ∧ (I.domain t).Realize fun (i : ι t) => c (Coord.data ⟨t, i⟩)

I.domainAt t holds of c iff c p ≠ c q, c (tag t') is c q at t and c p elsewhere, all data coordinates for tags t' ≠ t equal c p, and the t-coordinates satisfy I.domain t.

theorem Cslib.Logic.FO.TaggedInterpretation.realize_relAt {L : FirstOrder.Language} {L' : FirstOrder.Language} {T : Type} {ι : T → Type} [Finite T] {I : TaggedInterpretation L L' T ι} {M : Type w} [L.Structure M] {n : ℕ} (R : L'.Relations n) (c : Fin n × Coord T ι → M) : (I.relAt R).Realize c ↔ (∀ (j j' : Fin n), c (j, Coord.p) = c (j', Coord.p) ∧ c (j, Coord.q) = c (j', Coord.q)) ∧ ∃ (ts : Fin n → T), (∀ (j : Fin n), c (j, Coord.tag (ts j)) = c (j, Coord.q)) ∧ (I.rel R ts).Realize fun (σ : (j : Fin n) × ι (ts j)) => c (σ.fst, Coord.data ⟨ts σ.fst, σ.snd⟩)

I.relAt R holds of c iff all arguments share the same copy pair (p, q) and there is a tag assignment ts selected by the tag coordinates whose data coordinates satisfy I.rel R ts.

theorem Cslib.Logic.FO.TaggedInterpretation.realize_toInterpretation_domain_of_subsingleton {L : FirstOrder.Language} {L' : FirstOrder.Language} {T : Type} {ι : T → Type} [Finite T] [∀ (t : T), Finite (ι t)] {I : TaggedInterpretation L L' T ι} {M : Type w} [L.Structure M] (S : Interpretation L L' Unit) [Subsingleton M] (c : Coord T ι → M) : (I.toInterpretation S).domain.Realize c ↔ S.domain.Realize fun (x : Unit) => c Coord.p

On a subsingleton structure M, the domain formula of I.toInterpretation S reduces to S.domain at coordinate p.

theorem Cslib.Logic.FO.TaggedInterpretation.realize_toInterpretation_domain_of_nontrivial {L : FirstOrder.Language} {L' : FirstOrder.Language} {T : Type} {ι : T → Type} [Finite T] [∀ (t : T), Finite (ι t)] {I : TaggedInterpretation L L' T ι} {M : Type w} [L.Structure M] (S : Interpretation L L' Unit) [Nontrivial M] (c : Coord T ι → M) : (I.toInterpretation S).domain.Realize c ↔ ∃ (t : T), (I.domainAt t).Realize c

On a nontrivial structure M, the domain formula of I.toInterpretation S holds iff I.domainAt t holds for some tag t.

theorem Cslib.Logic.FO.TaggedInterpretation.realize_toInterpretation_rel_of_subsingleton {L : FirstOrder.Language} {L' : FirstOrder.Language} {T : Type} {ι : T → Type} [Finite T] [∀ (t : T), Finite (ι t)] {I : TaggedInterpretation L L' T ι} {M : Type w} [L.Structure M] (S : Interpretation L L' Unit) [Subsingleton M] {n : ℕ} (R : L'.Relations n) (c : Fin n × Coord T ι → M) : ((I.toInterpretation S).rel R).Realize c ↔ (S.rel R).Realize fun (x : Fin n × Unit) => c (x.1, Coord.p)

On a subsingleton structure M, the relation formula of I.toInterpretation S for R reduces to S.rel R at coordinate p.

theorem Cslib.Logic.FO.TaggedInterpretation.realize_toInterpretation_rel_of_nontrivial {L : FirstOrder.Language} {L' : FirstOrder.Language} {T : Type} {ι : T → Type} [Finite T] [∀ (t : T), Finite (ι t)] {I : TaggedInterpretation L L' T ι} {M : Type w} [L.Structure M] (S : Interpretation L L' Unit) [Nontrivial M] {n : ℕ} (R : L'.Relations n) (c : Fin n × Coord T ι → M) : ((I.toInterpretation S).rel R).Realize c ↔ (I.relAt R).Realize c

On a nontrivial structure M, the relation formula of I.toInterpretation S for R reduces to I.relAt R.

Structures with at most one element

def Cslib.Logic.FO.TaggedInterpretation.subsingletonEquiv {L : FirstOrder.Language} {L' : FirstOrder.Language} {T : Type} {ι : T → Type} [Finite T] [∀ (t : T), Finite (ι t)] {I : TaggedInterpretation L L' T ι} {M : Type w} [L.Structure M] (S : Interpretation L L' Unit) [L'.IsRelational] [Subsingleton M] : L'.Equiv ((I.toInterpretation S).Model M) (S.Model M)

On a structure with at most one element, the compiled interpretation is the interpretation S.

Structures with two distinct elements

def Cslib.Logic.FO.TaggedInterpretation.Pairs (M : Type w) : Type w

The ordered pairs of distinct elements, each indexing a copy of the tagged structure.

instance Cslib.Logic.FO.TaggedInterpretation.instFinitePairs {M : Type w} [Finite M] : Finite (Pairs M)

When M is finite, Pairs M is finite.

instance Cslib.Logic.FO.TaggedInterpretation.instNonemptyPairsOfNontrivial {M : Type w} [Nontrivial M] : Nonempty (Pairs M)

When M is nontrivial, Pairs M is nonempty.

noncomputable def Cslib.Logic.FO.TaggedInterpretation.coords {L : FirstOrder.Language} {L' : FirstOrder.Language} {T : Type} {ι : T → Type} {I : TaggedInterpretation L L' T ι} {M : Type w} [L.Structure M] (a b : M) (e : I.Model M) : Coord T ι → M

The coordinates of an element e of the tagged structure in the copy of the pair (a, b): the coordinates p and q are a and b.

@[simp]

theorem Cslib.Logic.FO.TaggedInterpretation.coords_data_self {L : FirstOrder.Language} {L' : FirstOrder.Language} {T : Type} {ι : T → Type} {I : TaggedInterpretation L L' T ι} {M : Type w} [L.Structure M] (a b : M) (e : I.Model M) (i : ι e.fst) : coords a b e (Coord.data ⟨e.fst, i⟩) = ↑e.snd i

At the tag e.1 of e, coords a b e evaluates data ⟨e.1, i⟩ to e.2.1 i.

theorem Cslib.Logic.FO.TaggedInterpretation.realize_domainAt_coords {L : FirstOrder.Language} {L' : FirstOrder.Language} {T : Type} {ι : T → Type} [Finite T] [∀ (t : T), Finite (ι t)] {I : TaggedInterpretation L L' T ι} {M : Type w} [L.Structure M] (a b : M) (h : a ≠ b) (e : I.Model M) : (I.domainAt e.fst).Realize (coords a b e)

For distinct elements a ≠ b and e : I.Model M, coords a b e satisfies I.domainAt e.1.

noncomputable def Cslib.Logic.FO.TaggedInterpretation.ofCopies {L : FirstOrder.Language} {L' : FirstOrder.Language} {T : Type} {ι : T → Type} [Finite T] [∀ (t : T), Finite (ι t)] {I : TaggedInterpretation L L' T ι} {M : Type w} [L.Structure M] (S : Interpretation L L' Unit) [Nontrivial M] (x : Copies (Pairs M) (I.Model M)) : (I.toInterpretation S).Model M

The map from the copies of the tagged structure to the compiled structure.

theorem Cslib.Logic.FO.TaggedInterpretation.ofCopies_bijective {L : FirstOrder.Language} {L' : FirstOrder.Language} {T : Type} {ι : T → Type} [Finite T] [∀ (t : T), Finite (ι t)] {I : TaggedInterpretation L L' T ι} {M : Type w} [L.Structure M] (S : Interpretation L L' Unit) [Nontrivial M] : Function.Bijective (ofCopies S)

On a nontrivial structure M, ofCopies S is a bijection from Copies (Pairs M) (I.Model M) to (I.toInterpretation S).Model M.

noncomputable def Cslib.Logic.FO.TaggedInterpretation.copiesEquiv {L : FirstOrder.Language} {L' : FirstOrder.Language} {T : Type} {ι : T → Type} [Finite T] [∀ (t : T), Finite (ι t)] {I : TaggedInterpretation L L' T ι} {M : Type w} [L.Structure M] (S : Interpretation L L' Unit) [L'.IsRelational] [Nontrivial M] : L'.Equiv (Copies (Pairs M) (I.Model M)) ((I.toInterpretation S).Model M)

On a structure with two distinct elements, the compiled interpretation is a disjoint union of copies of the tagged one, a copy for each ordered pair of distinct elements.

theorem Cslib.Logic.FO.TaggedInterpretation.nontrivial_toInterpretation_model {L : FirstOrder.Language} {L' : FirstOrder.Language} {T : Type} [Finite T] {ι : T → Type} [∀ (t : T), Finite (ι t)] (I : TaggedInterpretation L L' T ι) (S : Interpretation L L' Unit) {M : Type w} [L.Structure M] [Nontrivial M] [Nonempty (I.Model M)] : Nontrivial ((I.toInterpretation S).Model M)

On a structure with two distinct elements, the compiled interpretation of a tagged interpretation whose structures are nonempty is nontrivial: there are at least two copies.

Reductions by tagged interpretations

theorem Cslib.Logic.FO.Reduces.of_tagged {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] {K : Set (CategoryTheory.Bundled L.Structure)} {K' : Set (CategoryTheory.Bundled L'.Structure)} (hK' : IsoClosed K') (hcopy : CopyInvariant K') {T : Type} [Finite T] {ι : T → Type} [∀ (t : T), Finite (ι t)] (I : TaggedInterpretation L L' T ι) (S : Interpretation L L' Unit) (hlarge : ∀ (M : CategoryTheory.Bundled L.Structure) [Finite ↑M], Nontrivial ↑M → (M ∈ K ↔ CategoryTheory.Bundled.of (I.Model ↑M) ∈ K')) (hsmall : ∀ (M : CategoryTheory.Bundled L.Structure) [Finite ↑M], Subsingleton ↑M → (M ∈ K ↔ CategoryTheory.Bundled.of (S.Model ↑M) ∈ K')) : Reduces K K'

Tagged interpretations give order-free reductions to classes closed under isomorphism and under copies: if the structure interpreted by I decides membership on the finite structures with two distinct elements, and the interpretation S of dimension one decides it on those with at most one element, then the compiled interpretation is a order-free reduction.

Templates for binary relations

structure Cslib.Logic.FO.TaggedInterpretation.Template (L : FirstOrder.Language) {T : Type u_3} (ι : T → Type u_4) (t : T) : Type (max (max (max u u_3) u_4) v)

A template for a binary relation from elements of tag t: it relates an element of tag t whose coordinates x satisfy the guard to the elements of tag target whose coordinate j is x i whenever map j = some i, the coordinates j with map j = none being arbitrary.

• target : T

  The tag of the related elements.

• guard : L.Formula (ι t)

  The condition on the coordinates of the element of tag t.

• map : ι self.target → Option (ι t)

  The coordinates of the related elements copied from the element of tag t.

def Cslib.Logic.FO.TaggedInterpretation.Template.Compat {L : FirstOrder.Language} {T : Type u_1} {ι : T → Type u_2} {t : T} (τ : Template L ι t) {M : Type w} (x : ι t → M) (y : ι τ.target → M) : Prop

The tuples of tag τ.target related to the coordinates x of an element of tag t.

def Cslib.Logic.FO.TaggedInterpretation.Template.Holds {L : FirstOrder.Language} {T : Type u_1} {ι : T → Type u_2} {t : T} (τ : Template L ι t) {M : Type w} [L.Structure M] (x : ι t → M) (e : (w : T) × (ι w → M)) : Prop

The template relates the coordinates x of an element of tag t to an element of tag w with coordinates y.

noncomputable def Cslib.Logic.FO.TaggedInterpretation.Template.formula {L : FirstOrder.Language} {T : Type u_1} {ι : T → Type u_2} {t : T} (τ : Template L ι t) [∀ (t : T), Finite (ι t)] (w : T) : L.Formula (ι t ⊕ ι w)

The formula of a template, relating an element of tag t to an element of tag w.

theorem Cslib.Logic.FO.TaggedInterpretation.Template.realize_formula {L : FirstOrder.Language} {T : Type u_1} {ι : T → Type u_2} {t : T} (τ : Template L ι t) {M : Type w} [∀ (t : T), Finite (ι t)] [L.Structure M] {w : T} (x : ι t → M) (y : ι w → M) : (τ.formula w).Realize (Sum.elim x y) ↔ τ.Holds x ⟨w, y⟩

The formula of a template holds of the coordinates of two elements exactly when the template relates them.

noncomputable def Cslib.Logic.FO.TaggedInterpretation.Template.listFormula {L : FirstOrder.Language} {T : Type u_1} {ι : T → Type u_2} {t : T} [∀ (t : T), Finite (ι t)] (l : List (Template L ι t)) (w : T) : L.Formula (ι t ⊕ ι w)

The disjunction of the formulas of a list of templates.

theorem Cslib.Logic.FO.TaggedInterpretation.Template.realize_listFormula {L : FirstOrder.Language} {T : Type u_1} {ι : T → Type u_2} {t : T} {M : Type w} [∀ (t : T), Finite (ι t)] [L.Structure M] (l : List (Template L ι t)) {w : T} (x : ι t → M) (y : ι w → M) : (listFormula l w).Realize (Sum.elim x y) ↔ ∃ τ ∈ l, τ.Holds x ⟨w, y⟩

The formula of a list of templates holds exactly when one of them relates the elements.

def Cslib.Logic.FO.TaggedInterpretation.binaryRel {L : FirstOrder.Language} {T : Type u_1} {ι : T → Type u_2} (F : (t w : T) → L.Formula (ι t ⊕ ι w)) (ts : Fin 2 → T) : L.Formula ((j : Fin 2) × ι (ts j))

The formula of a binary relation among arguments of tags ts 0 and ts 1, from a formula in the coordinates of the two arguments.

theorem Cslib.Logic.FO.TaggedInterpretation.relMap_binaryRel {L : FirstOrder.Language} {T : Type u_1} {ι : T → Type u_2} {L' : FirstOrder.Language} [L'.IsRelational] {I : TaggedInterpretation L L' T ι} {M : Type w} [L.Structure M] {R : L'.Relations 2} {F : (t w : T) → L.Formula (ι t ⊕ ι w)} (hR : ∀ (ts : Fin 2 → T), I.rel R ts = binaryRel F ts) (a b : I.Model M) : FirstOrder.Language.Structure.RelMap R ![a, b] ↔ (F a.fst b.fst).Realize (Sum.elim ↑a.snd ↑b.snd)

When I.rel R is defined by binaryRel F, RelMap R ![a, b] holds in I.Model M iff F a.1 b.1 holds of Sum.elim a.2.1 b.2.1.