Isomorphism preservation for first-order logic.

Key results:

1. Term evaluation commutes with isomorphisms
2. Satisfaction is preserved by isomorphisms
3. FO sentences are order-independent (Immerman Proposition 1.16)

theorem Complexity.DescriptiveComplexity.Term.eval_iso {V : Vocabulary} {A B : FinStruct V} {n : Nat} (f : Iso A B) (σ : Env A.card n) (t : Term V n) : eval B (f.toFun ∘ σ) t = f.toFun (eval A σ t)

Term evaluation commutes with isomorphisms.

theorem Complexity.DescriptiveComplexity.Formula.sat_iso {V : Vocabulary} {A B : FinStruct V} {n : Nat} (f : Iso A B) (σ : Env A.card n) (φ : Formula V n) : Sat A σ φ ↔ Sat B (f.toFun ∘ σ) φ

Satisfaction is preserved by isomorphisms.

theorem Complexity.DescriptiveComplexity.Sentence.orderIndependent {V : Vocabulary} (φ : Sentence V) : BooleanQuery.IsOrderIndependent fun (A : FinStruct V) => Models A φ

FO sentences are order-independent (Immerman Proposition 1.16).