Formula synthesis for fixed finite choices #
A fixed finite family of defining formulas can be conjoined or disjoined without changing the relational polarity. The indexing type is independent of the structure, so these rules construct one finite formula uniformly across all domain sizes. They support, for example, finite machine transition tables in descriptive-complexity proofs.
Main results #
PolarityDefinable.constant: structure-independent truth values are definable.PolarityDefinable.exists_mem,PolarityDefinable.forall_mem: disjunctions and conjunctions over a fixed list, with definability required only of its members.PolarityDefinable.iEx,PolarityDefinable.iAll: fixed finite choices and conjunctions.
constant, iEx and iAll participate in the extensible FODefinable synthesis rule set.
theorem Cslib.Logic.FO.Operator.PolarityDefinable.constant {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {policy : Policy shape} {ι : Type t} {M : ι → Type z} [(i : ι) → L.Structure (M i)] {I : (i : ι) → Interpretation shape (M i)} {Γ : List ℕ} {ρ : (i : ι) → RelEnv Γ (M i)} {mark : Marking Γ} {sign : Bool} {α : Type w} (p : Prop) :
PolarityDefinable policy (fun {k : ℕ} => mark) sign M I ρ fun (x : ι) (x_1 : α → M x) => p
A proposition independent of the structure and assignment has a constant formula.
theorem Cslib.Logic.FO.Operator.PolarityDefinable.exists_mem {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {policy : Policy shape} {ι : Type t} {M : ι → Type z} [(i : ι) → L.Structure (M i)] {I : (i : ι) → Interpretation shape (M i)} {Γ : List ℕ} {ρ : (i : ι) → RelEnv Γ (M i)} {mark : Marking Γ} {sign : Bool} {α : Type w} {β : Type r} (l : List β) {P : β → (i : ι) → (α → M i) → Prop} (hP : ∀ b ∈ l, PolarityDefinable policy (fun {k : ℕ} => mark) sign M I ρ (P b)) :
PolarityDefinable policy (fun {k : ℕ} => mark) sign M I ρ fun (i : ι) (v : α → M i) => ∃ b ∈ l, P b i v
A disjunction over a fixed list preserves a certified polarity.
theorem Cslib.Logic.FO.Operator.PolarityDefinable.forall_mem {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {policy : Policy shape} {ι : Type t} {M : ι → Type z} [(i : ι) → L.Structure (M i)] {I : (i : ι) → Interpretation shape (M i)} {Γ : List ℕ} {ρ : (i : ι) → RelEnv Γ (M i)} {mark : Marking Γ} {sign : Bool} {α : Type w} {β : Type r} (l : List β) {P : β → (i : ι) → (α → M i) → Prop} (hP : ∀ b ∈ l, PolarityDefinable policy (fun {k : ℕ} => mark) sign M I ρ (P b)) :
PolarityDefinable policy (fun {k : ℕ} => mark) sign M I ρ fun (i : ι) (v : α → M i) => ∀ b ∈ l, P b i v
A conjunction over a fixed list preserves a certified polarity.
theorem Cslib.Logic.FO.Operator.PolarityDefinable.iEx {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {policy : Policy shape} {ι : Type t} {M : ι → Type z} [(i : ι) → L.Structure (M i)] {I : (i : ι) → Interpretation shape (M i)} {Γ : List ℕ} {ρ : (i : ι) → RelEnv Γ (M i)} {mark : Marking Γ} {sign : Bool} {α : Type w} {β : Type r} [Finite β] {P : β → (i : ι) → (α → M i) → Prop} (hP : ∀ (b : β), PolarityDefinable policy (fun {k : ℕ} => mark) sign M I ρ (P b)) :
PolarityDefinable policy (fun {k : ℕ} => mark) sign M I ρ fun (i : ι) (v : α → M i) => ∃ (b : β), P b i v
A fixed finite disjunction preserves a certified polarity.
theorem Cslib.Logic.FO.Operator.PolarityDefinable.iAll {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {policy : Policy shape} {ι : Type t} {M : ι → Type z} [(i : ι) → L.Structure (M i)] {I : (i : ι) → Interpretation shape (M i)} {Γ : List ℕ} {ρ : (i : ι) → RelEnv Γ (M i)} {mark : Marking Γ} {sign : Bool} {α : Type w} {β : Type r} [Finite β] {P : β → (i : ι) → (α → M i) → Prop} (hP : ∀ (b : β), PolarityDefinable policy (fun {k : ℕ} => mark) sign M I ρ (P b)) :
PolarityDefinable policy (fun {k : ℕ} => mark) sign M I ρ fun (i : ι) (v : α → M i) => ∀ (b : β), P b i v
A fixed finite conjunction preserves a certified polarity.