Composition of canonical full-tuple interpretations

Composition pulls back each output input-relation formula and flattens the outer coordinate before the inner coordinate. Canonical numeric formulas are reconstructed on the full product dimension. The flattening rank theorem proves that these have exactly the semantics of the successive canonical expansions, including order, BIT and the numeric constants.

The source universe has at least two elements and both dimensions are positive. No automatic numeric preservation is claimed for arbitrary restricted domains, and no machine bound is implied.

Main definitions

• Cslib.Logic.FO.Ordered.FullTupleInterpretation.comp: native full-tuple composition.

Main results

• Cslib.Logic.FO.Ordered.FullTupleInterpretation.compEquiv: canonical composition isomorphism.
• Cslib.Logic.FO.Ordered.FullTupleInterpretation.realize_comp_onFormula: semantic agreement with successive native pullbacks.

References

• N. Immerman, Descriptive Complexity, Proposition 1.28, Exercise 1.30, Remark 1.32 and Exercise 1.33, with the full tuple universe.

noncomputable def Cslib.Logic.FO.Ordered.FullTupleInterpretation.comp {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} {k l : ℕ} [L'.IsRelational] (J : FullTupleInterpretation L' L'' l) (I : FullTupleInterpretation L L' k) : FullTupleInterpretation L L'' (l * k)

Pull back output input-relation formulas and flatten (j, i) to j * k + i. All numeric symbols are supplied by the canonical full-tuple construction at dimension l * k.

theorem Cslib.Logic.FO.Ordered.FullTupleInterpretation.realize_comp_rel {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} {k l : ℕ} [L'.IsRelational] (J : FullTupleInterpretation L' L'' l) (I : FullTupleInterpretation L L' k) {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] (hk : 0 < k) {r : ℕ} (R : L''.Relations r) (v : Fin r → Fin l → Fin k → Fin n) : (((J.comp I).rel R).Realize fun (p : Fin r × Fin (l * k)) => flattenTuple (v p.1) p.2) ↔ (J.rel R).Realize fun (p : Fin r × Fin l) => lexEquiv (v p.1 p.2)

The composite relation definition agrees with the second interpretation on the inner ranks.

def Cslib.Logic.FO.Ordered.FullTupleInterpretation.compEquiv {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} {k l : ℕ} [L'.IsRelational] (J : FullTupleInterpretation L' L'' l) (I : FullTupleInterpretation L L' k) {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] [L''.IsRelational] (hk : 0 < k) (hl : 0 < l) : (language L'').Equiv (Fin ((n ^ k) ^ l)) (Fin (n ^ (l * k)))

Successive canonical interpretations and the flattened composite are isomorphic as full ordered structures. The map preserves the natural index of every element.

@[simp]

theorem Cslib.Logic.FO.Ordered.FullTupleInterpretation.compEquiv_apply_val {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} {k l : ℕ} [L'.IsRelational] (J : FullTupleInterpretation L' L'' l) (I : FullTupleInterpretation L L' k) {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] [L''.IsRelational] (hk : 0 < k) (hl : 0 < l) (x : Fin ((n ^ k) ^ l)) : ↑((J.compEquiv I hk hl) x) = ↑x

The composition isomorphism changes only the type-level expression for the same size.

theorem Cslib.Logic.FO.Ordered.FullTupleInterpretation.realize_comp_onFormula {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} {k l : ℕ} [L'.IsRelational] (J : FullTupleInterpretation L' L'' l) (I : FullTupleInterpretation L L' k) {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] [L''.IsRelational] (hk : 0 < k) (hl : 0 < l) {α : Type u_1} (φ : (language L'').Formula α) (v : α → Fin l → Fin k → Fin n) : (((J.comp I).onFormula φ).Realize fun (p : α × Fin (l * k)) => flattenTuple (v p.1) p.2) ↔ (I.onFormula (J.onFormula φ)).Realize fun (p : (α × Fin l) × Fin k) => v p.1.1 p.1.2 p.2

Every ordered formula has the same truth value under the composite pullback and the two successive pullbacks. Constants and quantifiers are included.

theorem Cslib.Logic.FO.Ordered.FullTupleInterpretation.realize_comp_onSentence {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} {k l : ℕ} [L'.IsRelational] (J : FullTupleInterpretation L' L'' l) (I : FullTupleInterpretation L L' k) {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] [L''.IsRelational] (hk : 0 < k) (hl : 0 < l) (φ : (language L'').Sentence) : Fin n ⊨ (J.comp I).onSentence φ ↔ Fin n ⊨ I.onSentence (J.onSentence φ)

Composition preserves sentence pullback, including the canonical numeric vocabulary.