Definitions and theorems relating propositional formulas and functions to variables

Main definitions

PropForm.vars - the set of syntactic variables of a formula PropFun.semVars - the set of semantic variables of a function PropFun.equivalentOver X - two functions are equivalent over a set X of variables PropFun.hasUniqueExtension X Y - the assignments to a function extend uniquely from a set X to a set Y of variables

NOTE: Semantic notions are not generally defined on PropForms. They are expected to be used on PropForms by composing with ⟦-⟧.

NOTE: We try to delay talking about dependently-typed functions {x // x ∈ X} → Bool for as long as possible by developing the theory in terms of total assignments ν → Bool.

Syntactic Variables

@[reducible]

def Trestle.Model.PropForm.vars {ν : Type u_1} [DecidableEq ν] : PropForm ν → Finset ν

Variables appearing in the formula. Sometimes called its "support set".

Equations

• (Trestle.Model.PropForm.var y).vars = {y}
• Trestle.Model.PropForm.tr.vars = ∅
• Trestle.Model.PropForm.fls.vars = ∅
• φ.neg.vars = φ.vars
• (φ₁.conj φ₂).vars = φ₁.vars ∪ φ₂.vars
• (φ₁.disj φ₂).vars = φ₁.vars ∪ φ₂.vars
• (φ₁.impl φ₂).vars = φ₁.vars ∪ φ₂.vars
• (φ₁.biImpl φ₂).vars = φ₁.vars ∪ φ₂.vars

theorem Trestle.Model.PropForm.eval_of_agreeOn_vars {ν : Type u_1} [DecidableEq ν] {φ : PropForm ν} {σ₁ σ₂ : PropAssignment ν} : PropAssignment.agreeOn (↑φ.vars) σ₁ σ₂ → eval σ₁ φ = eval σ₂ φ

theorem Trestle.Model.PropForm.eval_ext {ν : Type u_1} [DecidableEq ν] {φ : PropForm ν} {σ₁ σ₂ : PropAssignment ν} : (∀ x ∈ φ.vars, σ₁ x = σ₂ x) → eval σ₁ φ = eval σ₂ φ

theorem Trestle.Model.PropForm.eval_set_of_not_mem_vars {ν : Type u_1} [DecidableEq ν] {b : Bool} {x : ν} {φ : PropForm ν} {τ : PropAssignment ν} : x ∉ φ.vars → eval (τ.set x b) φ = eval τ φ

theorem Trestle.Model.PropForm.agreeOn_vars {ν : Type u_1} [DecidableEq ν] {φ : PropForm ν} {σ₁ σ₂ : PropAssignment ν} : PropAssignment.agreeOn (↑φ.vars) σ₁ σ₂ → (σ₁ ⊨ φ ↔ σ₂ ⊨ φ)

theorem Trestle.Model.PropForm.mem_vars_of_flip {ν : Type u_1} [DecidableEq ν] {φ : PropForm ν} {τ : PropAssignment ν} (x : ν) : τ ⊨ φ → (fun (M : PropAssignment ν) (φ : PropForm ν) => ¬M ⊨ φ) (τ.set x !τ x) φ → x ∈ φ.vars

theorem Trestle.Model.PropForm.exists_flip {ν : Type u_1} [DecidableEq ν] {φ : PropForm ν} {σ₁ σ₂ : PropAssignment ν} (h₁ : σ₁ ⊨ φ) (h₂ : ¬σ₂ ⊨ φ) : ∃ (x : ν) (τ : PropAssignment ν), σ₁ x ≠ σ₂ x ∧ τ ⊨ φ ∧ (fun (M : PropAssignment ν) (φ : PropForm ν) => ¬M ⊨ φ) (τ.set x !τ x) φ

theorem Trestle.Model.PropForm.exists_flip.go {ν : Type u_1} [DecidableEq ν] {φ : PropForm ν} {σ₁ σ₂ : PropAssignment ν} (h₁ : σ₁ ⊨ φ) (h₂ : ¬σ₂ ⊨ φ) (s : Finset ν) (hS : ∀ x ∈ s, σ₁ x ≠ σ₂ x) (hSC : ∀ x ∈ φ.vars \ s, σ₁ x = σ₂ x) : ∃ (x : ν) (τ : PropAssignment ν), x ∈ s ∧ τ ⊨ φ ∧ (fun (M : PropAssignment ν) (φ : PropForm ν) => ¬M ⊨ φ) (τ.set x !τ x) φ

Semantic Variables

noncomputable def Trestle.Model.PropFun.semVars {ν : Type u_1} [DecidableEq ν] (φ : PropFun ν) : Finset ν

The semantic variables of φ are those it is sensitive to as a Boolean function. Unlike vars, this set is stable under equivalence of formulas.

Equations

• φ.semVars = ⋯.toFinset

theorem Trestle.Model.PropFun.semVars_mk {ν : Type u_1} [DecidableEq ν] (φ : PropForm ν) : semVars ⟦φ⟧ ⊆ φ.vars

theorem Trestle.Model.PropFun.mem_semVars {ν : Type u_1} [DecidableEq ν] (φ : PropFun ν) (x : ν) : x ∈ φ.semVars ↔ ∃ (τ : PropAssignment ν), τ ⊨ φ ∧ (fun (M : PropAssignment ν) (φ : PropFun ν) => ¬M ⊨ φ) (τ.set x !τ x) φ

theorem Trestle.Model.PropFun.not_mem_semVars {ν : Type u_1} [DecidableEq ν] (φ : PropFun ν) (x : ν) : x ∉ φ.semVars ↔ ∀ (τ : PropAssignment ν) (b : Bool), τ.set x b ⊨ φ ↔ τ ⊨ φ

theorem Trestle.Model.PropFun.exists_semVar {ν : Type u_1} [DecidableEq ν] {φ : PropFun ν} {σ₁ σ₂ : PropAssignment ν} : σ₁ ⊨ φ → (fun (M : PropAssignment ν) (φ : PropFun ν) => ¬M ⊨ φ) σ₂ φ → ∃ (x : ν), σ₁ x ≠ σ₂ x ∧ x ∈ φ.semVars

Any two assignments with opposing evaluations on φ disagree on a semantic variable of φ.

theorem Trestle.Model.PropFun.agreeOn_semVars {ν : Type u_1} [DecidableEq ν] {φ : PropFun ν} {σ₁ σ₂ : PropAssignment ν} : PropAssignment.agreeOn (↑φ.semVars) σ₁ σ₂ → (σ₁ ⊨ φ ↔ σ₂ ⊨ φ)

theorem Trestle.Model.PropFun.eval_of_agreeOn_semVars {ν : Type u_1} [DecidableEq ν] {φ : PropFun ν} {σ₁ σ₂ : PropAssignment ν} : PropAssignment.agreeOn (↑φ.semVars) σ₁ σ₂ → eval σ₁ φ = eval σ₂ φ

@[simp]

theorem Trestle.Model.PropFun.semVars_var {ν : Type u_1} [DecidableEq ν] (x : ν) : (var x).semVars = {x}

@[simp]

theorem Trestle.Model.PropFun.semVars_tr (ν : Type u_1) [DecidableEq ν] : ⊤.semVars = ∅

@[simp]

theorem Trestle.Model.PropFun.semVars_fls (ν : Type u_1) [DecidableEq ν] : ⊥.semVars = ∅

@[simp]

theorem Trestle.Model.PropFun.semVars_neg {ν : Type u_1} [DecidableEq ν] (φ : PropFun ν) : φᶜ.semVars = φ.semVars

@[simp]

theorem Trestle.Model.PropFun.semVars_conj {ν : Type u_1} [DecidableEq ν] (φ₁ φ₂ : PropFun ν) : (φ₁ ⊓ φ₂).semVars ⊆ φ₁.semVars ∪ φ₂.semVars

Semantic variable set of a conjunction is contained in the union of each sub-prop's semantic variables.

Note that there aren't any obvious lower bounds on this set. Variables which are semantic in both sub-props may not be semantic:

• φ₁ = a ∨ b (b is semantic)
• φ₂ = a ∨ ¬b (b is semantic)
• φ₁ ⊓ φ₂ = a (b is NOT semantic) And variables in just one sub-prop may not be semantic:
• φ₁ = a ∨ b (b is semantic)
• φ₂ = a (b is NOT semantic)
• φ₁ ⊓ φ₂ = a (b is NOT semantic)

TODO: prove equality holds if Disjoint φ₁.semVars φ₂.semVars

@[simp]

theorem Trestle.Model.PropFun.semVars_disj {ν : Type u_1} [DecidableEq ν] (φ₁ φ₂ : PropFun ν) : (φ₁ ⊔ φ₂).semVars ⊆ φ₁.semVars ∪ φ₂.semVars

Semantic variable set of a conjunction is contained in the union of each sub-prop's semantic variables.

Note that there aren't any obvious lower bounds on this set. See [semVars_conj] for more details.

@[simp]

theorem Trestle.Model.PropFun.semVars_impl {ν : Type u_1} [DecidableEq ν] (φ₁ φ₂ : PropFun ν) : (φ₁ ⇨ φ₂).semVars ⊆ φ₁.semVars ∪ φ₂.semVars

@[simp]

theorem Trestle.Model.PropFun.semVars_biImpl {ν : Type u_1} [DecidableEq ν] (φ₁ φ₂ : PropFun ν) : ((fun (φ₁ φ₂ : PropFun ν) => (φ₁ ⇨ φ₂) ⊓ (φ₂ ⇨ φ₁)) φ₁ φ₂).semVars ⊆ φ₁.semVars ∪ φ₂.semVars

theorem Trestle.Model.PropFun.setMany_satisfies_iff_inter_semVars {ν : Type u_1} [DecidableEq ν] (τ : PropAssignment ν) (vs : Finset ν) (τ' : PropAssignment ν) (φ : PropFun ν) : τ.setMany vs τ' ⊨ φ ↔ τ.setMany (vs ∩ φ.semVars) τ' ⊨ φ

Equivalence Over Sets

def Trestle.Model.PropFun.equivalentOver {ν : Type u_1} (X : Set ν) (φ₁ φ₂ : PropFun ν) : Prop

Two functions φ₁ and φ₂ are equivalent over X when for every assignment τ, models of φ₁ extending τ over X are in bijection with models of φ₂ extending τ over X.

Equations

• One or more equations did not get rendered due to their size.

def Trestle.Model.PropFun.extendsOver {ν : Type u_1} (X : Set ν) (φ₁ φ₂ : PropFun ν) : Prop

Equations

• Trestle.Model.PropFun.extendsOver X φ₁ φ₂ = ∀ (σ₁ : Trestle.Model.PropAssignment ν), σ₁ ⊨ φ₁ → ∃ (σ₂ : Trestle.Model.PropAssignment ν), Trestle.Model.PropAssignment.agreeOn X σ₂ σ₁ ∧ σ₂ ⊨ φ₂

theorem Trestle.Model.PropFun.equivalentOver_iff_extendsOver {ν : Type u_1} (X : Set ν) (φ₁ φ₂ : PropFun ν) : equivalentOver X φ₁ φ₂ ↔ extendsOver X φ₁ φ₂ ∧ extendsOver X φ₂ φ₁

theorem Trestle.Model.PropFun.equivalentOver_refl {ν : Type u_1} {X : Set ν} (φ : PropFun ν) : equivalentOver X φ φ

theorem Trestle.Model.PropFun.equivalentOver.symm {α✝ : Type u_1} {X : Set α✝} {φ₁ φ₂ : PropFun α✝} : equivalentOver X φ₁ φ₂ → equivalentOver X φ₂ φ₁

theorem Trestle.Model.PropFun.equivalentOver.trans {α✝ : Type u_1} {X : Set α✝} {φ₁ φ₂ φ₃ : PropFun α✝} : equivalentOver X φ₁ φ₂ → equivalentOver X φ₂ φ₃ → equivalentOver X φ₁ φ₃

theorem Trestle.Model.PropFun.equivalentOver.subset {ν : Type u_1} {φ₁ φ₂ : PropFun ν} {X Y : Set ν} : X ⊆ Y → equivalentOver Y φ₁ φ₂ → equivalentOver X φ₁ φ₂

theorem Trestle.Model.PropFun.equivalentOver_semVars {ν : Type u_1} {φ₁ φ₂ : PropFun ν} [DecidableEq ν] {X : Set ν} : ↑φ₁.semVars ⊆ X → ↑φ₂.semVars ⊆ X → equivalentOver X φ₁ φ₂ → φ₁ = φ₂

Extension Over Sets

def Trestle.Model.PropFun.hasUniqueExtension {ν : Type u_1} (X Y : Set ν) (φ : PropFun ν) : Prop

A function has the unique extension property from X to Y (both sets of variables) when any satisfying assignment, if it exists, is uniquely determined on Y by its values on X. Formally, any two satisfying assignments which agree on X must also agree on Y.

Equations

• One or more equations did not get rendered due to their size.

theorem Trestle.Model.PropFun.hasUniqueExtension_refl {ν : Type u_1} (X : Set ν) (φ : PropFun ν) : hasUniqueExtension X X φ

theorem Trestle.Model.PropFun.hasUniqueExtension.subset_left {α✝ : Type u_1} {X X' Y : Set α✝} {φ : PropFun α✝} : X ⊆ X' → hasUniqueExtension X Y φ → hasUniqueExtension X' Y φ

theorem Trestle.Model.PropFun.hasUniqueExtension.subset_right {α✝ : Type u_1} {Y' Y X : Set α✝} {φ : PropFun α✝} : Y' ⊆ Y → hasUniqueExtension X Y φ → hasUniqueExtension X Y' φ

theorem Trestle.Model.PropFun.hasUniqueExtension.trans {α✝ : Type u_1} {X Y : Set α✝} {φ : PropFun α✝} {Z : Set α✝} : hasUniqueExtension X Y φ → hasUniqueExtension Y Z φ → hasUniqueExtension X Z φ

theorem Trestle.Model.PropFun.hasUniqueExtension.conj_right {ν : Type u_1} {X Y : Set ν} {φ : PropFun ν} (ψ : PropFun ν) : hasUniqueExtension X Y φ → hasUniqueExtension X Y (φ ⊓ ψ)

theorem Trestle.Model.PropFun.hasUniqueExtension.conj_left {ν : Type u_1} {X Y : Set ν} {φ : PropFun ν} (ψ : PropFun ν) : hasUniqueExtension X Y φ → hasUniqueExtension X Y (ψ ⊓ φ)

theorem Trestle.Model.PropFun.hasUniqueExtension_to_empty {ν : Type u_1} (X : Set ν) (φ : PropFun ν) : hasUniqueExtension X ∅ φ

theorem Trestle.Model.PropForm.equivalentOver_of_equivalent {ν : Type u_1} {φ₁ φ₂ : PropForm ν} (X : Set ν) : φ₁ ≈ φ₂ → PropFun.equivalentOver X ⟦φ₁⟧ ⟦φ₂⟧

theorem Trestle.Model.PropForm.semVars_eq_of_equivalent {ν : Type u_1} [DecidableEq ν] {φ₁ φ₂ : PropForm ν} : φ₁ ≈ φ₂ → PropFun.semVars ⟦φ₁⟧ = PropFun.semVars ⟦φ₂⟧

@[simp]

theorem Trestle.Model.PropForm.semVars_subset_vars {ν : Type u_1} [DecidableEq ν] (φ : PropForm ν) : PropFun.semVars ⟦φ⟧ ⊆ φ.vars

theorem Trestle.Model.PropForm.equivalentOver_vars {ν : Type u_1} [DecidableEq ν] {φ₁ φ₂ : PropForm ν} {X : Set ν} : ↑φ₁.vars ⊆ X → ↑φ₂.vars ⊆ X → PropFun.equivalentOver X ⟦φ₁⟧ ⟦φ₂⟧ → φ₁.equivalent φ₂