Documentation

Linglib.Core.Logic.FirstOrder.Comparative

Comparative possibility over a first-order base #

[Lew73b]'s comparative possibility as a formula language: classical first-order formulas embedded wholesale (the ModalFormula.ofFormula pattern), boolean connectives, and a binary comparative A ≻ B (.comp) evaluated at an index of an ordered family of structures — some (A∧¬B)-index in the cone strictly dominates every (B∧¬A)-index. realize_comp_iff_strict_dominationLift identifies ≻ with the strict l-lifting of [HI13] §5 — Lewis's lift, which is also the lift of [Kra91]'s ordering semantics, with complete logic WJR ([Hal03]); comparing difference sets follows [Kra12]'s revised lifting. [RK24] instantiates the language with interpretations as indices.

source
def FirstOrder.Language.Structure.ext₁ {L : Language} {E : Type u_1} (S : L.Structure E) (R : L.Relations 1) :
Set E

The extension of a unary relation symbol in a structure carried as a term.

Equations
  • S.ext₁ R = {e : E | FirstOrder.Language.Structure.RelMap R ![e]}
Instances For
    source
    @[simp]
    theorem FirstOrder.Language.Structure.mem_ext₁ {L : Language} {E : Type u_1} {S : L.Structure E} {R : L.Relations 1} {e : E} :
    e ∈ S.ext₁ R ↔ RelMap R ![e]
    source
    @[implicit_reducible]
    instance FirstOrder.Language.instDecidableMemSetExt₁OfRelMapVecConsVecEmpty {L : Language} {E : Type u_1} (S : L.Structure E) (R : L.Relations 1) (e : E) [h : Decidable (Structure.RelMap R ![e])] :
    Decidable (e ∈ S.ext₁ R)
    Equations
    source
    inductive FirstOrder.Language.CompFormula (L : Language) (E : Type u_1) :
    Type (max (max u_1 u_2) u_3)

    Comparative-possibility formulas: an embedded classical formula (free variables valued by domain elements), booleans, and the comparative ≻ (.comp). Booleans exist at both layers because negation and the derived equi must scope over ≻.

    Instances For
      source
      @[reducible, inline]
      abbrev FirstOrder.Language.CompFormula.matom {L : Language} {E : Type u_1} (R : L.Relations 1) (e : E) :
      L.CompFormula E

      Ground unary predication R(e), as an embedded formula.

      Equations
      Instances For
        source
        def FirstOrder.Language.CompFormula.equi {L : Language} {E : Type u_1} (A B : L.CompFormula E) :
        L.CompFormula E

        Equipossibility: A ≈ B := ¬(A ≻ B) ∧ ¬(B ≻ A).

        Equations
        Instances For
          source
          def FirstOrder.Language.CompFormula.CompFree {L : Language} {E : Type u_1} :
          L.CompFormula E → Prop

          Formulas free of the comparative: the fragment whose truth does not consult the ordering (realize_congr_of_compFree).

          Equations
          Instances For
            source
            @[reducible, inline]
            abbrev FirstOrder.Language.DecidableAtoms {L : Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) :
            Type (max (max (max u_1 u_2) u_3) u_5)

            Pointwise decidability of atoms across a doubly-indexed structure family — the hook that makes decide available on finite models; the semantics itself is decidability-free.

            Equations
            • FirstOrder.Language.DecidableAtoms interp = ((i : I) → (w : W) → (n : ℕ) → (r : L.Relations n) → (x : Fin n → E) → Decidable (FirstOrder.Language.Structure.RelMap r x))
            Instances For
              source
              def FirstOrder.Language.CompFormula.Realize {L : Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) (φ : L.CompFormula E) (le : I → I → Prop) (i : I) (w : W) :
              Prop

              Truth at an index of an ordered structure family, relative to a raw ordering relation le (restricted orderings need not be total). The comparative: some (A∧¬B)-index in the ≤-cone strictly dominates every (B∧¬A)-index.

              Equations
              Instances For
                source
                @[implicit_reducible]
                instance FirstOrder.Language.CompFormula.instDec {L : Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) [Fintype I] [Fintype E] [DecidableEq E] [hA : DecidableAtoms interp] (φ : L.CompFormula E) (le : I → I → Prop) [DecidableRel le] (i : I) (w : W) :
                Decidable (Realize interp φ le i w)
                Equations
                source
                theorem FirstOrder.Language.CompFormula.realize_comp_iff {L : Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) (A B : L.CompFormula E) (ord : Core.Order.TotalPreorder I) (i : I) (w : W) :
                Realize interp (A.comp B) ord.le i w ↔ ∃ (i' : I), ord.le i' i ∧ Realize interp A ord.le i' w ∧ ¬Realize interp B ord.le i' w ∧ ∀ (i'' : I), ord.le i'' i → Realize interp B ord.le i'' w → ¬Realize interp A ord.le i'' w → ord.lt i'' i'

                The comparative clause over a total preorder — definitional; the rewriting interface, with the domination conjunction packaged as ord.lt.

                source
                @[simp]
                theorem FirstOrder.Language.CompFormula.realize_matom {L : Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) (le : I → I → Prop) (i : I) (w : W) (R : L.Relations 1) (e : E) :
                Realize interp (matom R e) le i w ↔ Structure.RelMap R ![e]

                Realization of a ground unary atom.

                source
                theorem FirstOrder.Language.CompFormula.realize_congr_of_compFree {L : Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) (φ : L.CompFormula E) :
                φ.CompFree → ∀ (le le' : I → I → Prop) (i : I) (w : W), Realize interp φ le i w ↔ Realize interp φ le' i w

                Comparative-free formulas are ordering-invariant.

                source
                theorem FirstOrder.Language.CompFormula.realize_comp_iff_strict_dominationLift {L : Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) (A B : L.CompFormula E) (ord : Core.Order.TotalPreorder I) (i : I) (w : W) :
                Realize interp (A.comp B) ord.le i w ↔ ComparativeProbability.Strict (ComparativeProbability.dominationLift fun (a b : I) => ord.le b a) {x : I | ord.le x i ∧ Realize interp A ord.le x w ∧ ¬Realize interp B ord.le x w} {x : I | ord.le x i ∧ Realize interp B ord.le x w ∧ ¬Realize interp A ord.le x w}

                ≻ is the strict l-lifting of the ordering ([HI13]; Lewis's lifting) applied to the cone at the evaluation index: comparative possibility, with the ∃∀ clause as the strict Smyth order via strict_dominationLift_iff.

                source
                theorem FirstOrder.Language.CompFormula.not_realize_comp_self {L : Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) (A : L.CompFormula E) (le : I → I → Prop) (i : I) (w : W) :
                ¬Realize interp (A.comp A) le i w

                ≻ is irreflexive — a witness would make A both true and false.

                source
                theorem FirstOrder.Language.CompFormula.realize_equi_self {L : Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) (A : L.CompFormula E) (le : I → I → Prop) (i : I) (w : W) :
                Realize interp (A.equi A) le i w

                ≈ is reflexive.

                source
                theorem FirstOrder.Language.CompFormula.realize_equi_comm {L : Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) (A B : L.CompFormula E) (le : I → I → Prop) (i : I) (w : W) :
                Realize interp (A.equi B) le i w ↔ Realize interp (B.equi A) le i w

                ≈ is symmetric.