Substitution and Helper Lemmas

The lemmas here are mostly from Sections 2.1 and 2.2.

Single-step replacing

def repl_in_F (x : ℕ) (ψ : Formula) : Formula → Formula

Replace atomic proposition x by ψ in a formula.

Equations

• repl_in_F x ψ Formula.bottom = ⊥
• repl_in_F x ψ (·c) = if (c == x) = true then ψ else ·c
• repl_in_F x ψ (~φ) = (~ repl_in_F x ψ φ)
• repl_in_F x ψ (φ1⋀φ2) = repl_in_F x ψ φ1⋀repl_in_F x ψ φ2
• repl_in_F x ψ (⌈α⌉φ) = ⌈repl_in_P x ψ α⌉repl_in_F x ψ φ

def repl_in_P (x : ℕ) (ψ : Formula) : Program → Program

Replace atomic proposition x by ψ in a program.

Equations

• repl_in_P x ψ (·c) = ·c
• repl_in_P x ψ (α;'β) = (repl_in_P x ψ α;'repl_in_P x ψ β)
• repl_in_P x ψ (α⋓β) = (repl_in_P x ψ α⋓repl_in_P x ψ β)
• repl_in_P x ψ (∗α) = (∗repl_in_P x ψ α)
• repl_in_P x ψ (?'φ) = (?'repl_in_F x ψ φ)

theorem repl_in_Con {x : ℕ} {ψ : Formula} {l : List Formula} : repl_in_F x ψ (Con l) = Con (List.map (repl_in_F x ψ) l)

@[simp]

theorem repl_in_or {x : ℕ} {ψ φ1 φ2 : Formula} : repl_in_F x ψ (φ1⋁φ2) = repl_in_F x ψ φ1⋁repl_in_F x ψ φ2

theorem repl_in_dis {x : ℕ} {ψ : Formula} {l : List Formula} : repl_in_F x ψ (dis l) = dis (List.map (repl_in_F x ψ) l)

theorem repl_in_F_non_occ_eq {x : ℕ} {φ ρ : Formula} : Sum.inl x ∉ φ.voc → repl_in_F x ρ φ = φ

theorem repl_in_P_non_occ_eq {x : ℕ} {α : Program} {ρ : Formula} : Sum.inl x ∉ α.voc → repl_in_P x ρ α = α

theorem repl_in_boxes_non_occ_eq_neg {x : ℕ} {ψ : Formula} (δ : List Program) : Sum.inl x ∉ Vocab.fromList (List.map Program.voc δ) → repl_in_F x ψ (⌈⌈δ⌉⌉~·x) = ⌈⌈δ⌉⌉~ψ

theorem repl_in_boxes_non_occ_eq_pos {x : ℕ} {ψ : Formula} (δ : List Program) : Sum.inl x ∉ Vocab.fromList (List.map Program.voc δ) → repl_in_F x ψ (⌈⌈δ⌉⌉·x) = ⌈⌈δ⌉⌉ψ

theorem repl_in_list_non_occ_eq {x : ℕ} {ρ : Formula} (F : List Formula) : Sum.inl x ∉ Vocab.fromList (List.map Formula.voc F) → List.map (repl_in_F x ρ) F = F

theorem repl_in_F_voc_def (p : ℕ) (φ ψ : Formula) : (repl_in_F p φ ψ).voc = ψ.voc \ {Sum.inl p} ∪ if Sum.inl p ∈ ψ.voc then φ.voc else ∅

theorem repl_in_P_voc_def (p : ℕ) (φ : Formula) (α : Program) : (repl_in_P p φ α).voc = α.voc \ {Sum.inl p} ∪ if Sum.inl p ∈ α.voc then φ.voc else ∅

def repl_in_model {W : Type} (x : ℕ) (ψ : Formula) : KripkeModel W → KripkeModel W

Overwrite the valuation of x with the current value of ψ in a model.

Equations

• repl_in_model x ψ { val := V, Rel := R } = { val := fun (w : W) (c : ℕ) => if (c == x) = true then ({ val := V, Rel := R }, w)⊨ψ else V w c, Rel := R }

theorem repl_in_model_sat_iff (x : ℕ) (ψ φ : Formula) {W : Type} (M : KripkeModel W) (w : W) : (M, w)⊨repl_in_F x ψ φ ↔ (repl_in_model x ψ M, w)⊨φ

theorem repl_in_model_rel_iff (x : ℕ) (ψ : Formula) (α : Program) {W : Type} (M : KripkeModel W) (w v : W) : relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v

theorem repl_in_F_equiv {φ1 φ2 : Formula} (x : ℕ) (ψ : Formula) : φ1≡φ2 → repl_in_F x ψ φ1≡repl_in_F x ψ φ2

theorem repl_in_P_equiv {α1 α2 : Program} (x : ℕ) (ψ : Formula) : α1≡ᵣα2 → repl_in_P x ψ α1≡ᵣrepl_in_P x ψ α2

theorem repl_in_disMap {α : Type u_1} (x : ℕ) (ρ : Formula) (L : List α) (p : α → Prop) (f : α → Formula) [DecidablePred p] : repl_in_F x ρ (dis (List.map (fun (Fδ : α) => if p Fδ then Formula.bottom else f Fδ) L)) = dis (List.map (fun (Fδ : α) => if p Fδ then Formula.bottom else repl_in_F x ρ (f Fδ)) L)

Cancellation of replacements

@[simp]

theorem repl_in_F_cancel_via_non_occ (φ : Formula) (p q : ℕ) : Sum.inl q ∉ φ.voc → repl_in_F q (·p) (repl_in_F p (·q) φ) = φ

Replacing p with a fresh q and then replacing q by p results in the same formula.

theorem repl_in_P_cancel_via_non_occ (α : Program) (p q : ℕ) : Sum.inl q ∉ α.voc → repl_in_P q (·p) (repl_in_P p (·q) α) = α

Replacing p with a fresh q and then replacing q by p results in the same program.

Replacement of atoms in tautologies

theorem taut_repl (φ : Formula) (p q : ℕ) : tautology φ → tautology (repl_in_F p (·q) φ)

Replacing an atom in a tautology results in a tautology.

theorem non_occ_taut_then_taut_repl_in_imp (φ ψ : Formula) (p q : ℕ) : Sum.inl p ∉ ψ.voc → Sum.inl q ∉ ψ.voc → tautology (~φ⋀(~ψ)) → tautology (~ repl_in_F p (·q) φ⋀(~ψ))

A special case of taut_repl for the proof of beth.

theorem non_occ_taut_then_taut_imp_repl_in (φ ψ : Formula) (p q : ℕ) : Sum.inl p ∉ ψ.voc → Sum.inl q ∉ ψ.voc → tautology (~ψ⋀(~φ)) → tautology (~ψ⋀(~ repl_in_F p (·q) φ))

Another special case of taut_repl for the proof of beth.

Simultaneous Substitutions

@[reducible, inline]

abbrev Substitution : Type

Equations

• Substitution = (ℕ → Formula)

def subst_in_F (σ : Substitution) (φ : Formula) : Formula

Apply substitution σ to formula φ.

Equations

• subst_in_F σ Formula.bottom = ⊥
• subst_in_F σ (·c) = σ c
• subst_in_F σ (~φ) = (~subst_in_F σ φ)
• subst_in_F σ (φ1⋀φ2) = subst_in_F σ φ1⋀subst_in_F σ φ2
• subst_in_F σ (⌈α⌉φ) = ⌈subst_in_P σ α⌉subst_in_F σ φ

def subst_in_P (σ : Substitution) (α : Program) : Program

Apply substitution σ to program α.

Equations

• subst_in_P σ (·c) = ·c
• subst_in_P σ (α;'β) = (subst_in_P σ α;'subst_in_P σ β)
• subst_in_P σ (α⋓β) = (subst_in_P σ α⋓subst_in_P σ β)
• subst_in_P σ (∗α) = (∗subst_in_P σ α)
• subst_in_P σ (?'φ) = (?'subst_in_F σ φ)

def subst_in_model {W : Type} (σ : Substitution) (M : KripkeModel W) : KripkeModel W

Overwrite the valuation in M with the substitution σ.

Equations

• subst_in_model σ { val := V, Rel := R } = { val := fun (w : W) (c : ℕ) => ({ val := V, Rel := R }, w)⊨σ c, Rel := R }

theorem substitutionLemma (σ : Substitution) (φ : Formula) {W : Type} (M : KripkeModel W) (w : W) : (M, w)⊨subst_in_F σ φ ↔ (subst_in_model σ M, w)⊨φ

theorem substitutionLemmaRel (σ : Substitution) (α : Program) {W : Type} (M : KripkeModel W) (w v : W) : relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v

Semantic Equivalents

theorem equiv_con {φ1 φ2 : Formula} (h : φ1≡φ2) (ψ : Formula) : φ1⋀ψ≡φ2⋀ψ

A true instance of wrong_equiv_repl, here we replaced frm with a special case.