Logicality and Invariance Conditions

@cite{peters-westerstahl-2006} @cite{feferman-1999} @cite{van-benthem-1984}

Invariance conditions that characterize "logical" quantifiers, ordered by strength: HOM → INJ → ISOM → EXT.

• ISOM (isomorphism invariance) = QuantityInvariant in Defs.lean
• EXT (extension) = trivial for GQ α (universe-free representation)
• INJ (injective-homomorphism invariance)
• HOM (surjective-homomorphism invariance, @cite{feferman-1999})

Key result: INJ ≡ ISOM + EXT (@cite{peters-westerstahl-2006} Ch 9 Prop 3). Since EXT is trivial for GQ α, INJ ↔ ISOM in our setting.

def Core.Quantification.Logicality.HomInvariant {α : Type u_1} {β : Type u_2} (q : GQ α) (q' : GQ β) : Prop

Homomorphism invariance (HOM): Q is preserved under surjective maps. @cite{feferman-1999}: HOM characterizes "absolutely logical" operations. Stronger than ISOM: surjections can collapse elements, so HOM-invariant quantifiers cannot distinguish elements that map to the same image.

For a family of quantifiers indexed by type, q on α and q' on β are HOM-related when any surjection preserves truth values.

Equations

• Core.Quantification.Logicality.HomInvariant q q' = ∀ (f : α → β), Function.Surjective f → ∀ (A B : β → Prop), q (A ∘ f) (B ∘ f) ↔ q' A B

def Core.Quantification.Logicality.InjInvariant {α : Type u_1} {β : Type u_2} (q : GQ α) (q' : GQ β) : Prop

Injective homomorphism invariance (INJ): Q is preserved under injections. INJ sits between HOM and ISOM: HOM → INJ → ISOM. @cite{peters-westerstahl-2006} Ch 9 §2.

Equations

• Core.Quantification.Logicality.InjInvariant q q' = ∀ (f : α → β), Function.Injective f → ∀ (A B : β → Prop), q (A ∘ f) (B ∘ f) ↔ q' A B

theorem Core.Quantification.Logicality.hom_implies_isom_same_type {α : Type u_1} (q : GQ α) (hHom : HomInvariant q q) : QuantityInvariant q

HOM (same type) implies ISOM. Every bijection is a surjection.

Convention alignment: QuantityInvariant uses A(f(x)) ↔ A'(x) (the bijection goes from the new domain to the old), while HomInvariant uses A ∘ f. Given hA : A(f(x)) ↔ A'(x), we have A ∘ f = A' (as functions, via funext). So HomInvariant with f gives q (A ∘ f) (B ∘ f) ↔ q A B, i.e., q A' B' ↔ q A B.

@cite{peters-westerstahl-2006} Ch 9.

theorem Core.Quantification.Logicality.isom_implies_inj_same_type {α : Type u_1} [Fintype α] (q : GQ α) (hIsom : QuantityInvariant q) : InjInvariant q q

@cite{peters-westerstahl-2006} Ch 9 Prop 3 (one direction): ISOM → INJ for same-type quantifiers on a finite domain.

On a finite type, every injection is a bijection, so ISOM (bijection invariance) immediately gives INJ (injection invariance).

theorem Core.Quantification.Logicality.quantityInvariant_is_isom {α : Type u_1} (q : GQ α) : QuantityInvariant q ↔ ∀ (A B A' B' : α → Prop) (f : α → α), Function.Bijective f → (∀ (x : α), A (f x) ↔ A' x) → (∀ (x : α), B (f x) ↔ B' x) → (q A B ↔ q A' B')

Bijection invariance is definitionally QuantityInvariant.