Foundation.ProvabilityLogic.Realization

source

structure LO.ProvabilityLogic.Realization {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T : FirstOrder.Theory L} (𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T) :

Type u_1

Mapping modal prop vars to first-order sentence

val : ℕ → FirstOrder.Sentence L

Instances For

source

@[reducible, inline]

abbrev LO.FirstOrder.ArithmeticTheory.StandardRealization (T : ArithmeticTheory) [Theory.Δ₁ T] :

Type

Equations

T.StandardRealization = LO.ProvabilityLogic.Realization (LO.FirstOrder.Theory.standardProvability T)

Instances For

source

def LO.ProvabilityLogic.Realization.interpret {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} (f : Realization 𝔅) :

Modal.Formula ℕ → FirstOrder.Sentence L

Mapping modal formulae to first-order sentence

Equations

↑f (LO.Modal.Formula.atom a) = f.val a
↑f φ.box = ↑𝔅 (↑f φ)
↑f LO.Modal.Formula.falsum = ⊥
↑f (φ.imp ψ) = ↑f φ ➝ ↑f ψ

Instances For

source

instance LO.ProvabilityLogic.Realization.instCoeFunForallFormulaNatSentence {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} :

CoeFun (Realization 𝔅) fun (x : Realization 𝔅) => Modal.Formula ℕ → FirstOrder.Sentence L

Equations

LO.ProvabilityLogic.Realization.instCoeFunForallFormulaNatSentence = { coe := LO.ProvabilityLogic.Realization.interpret }

source

theorem LO.ProvabilityLogic.Realization.letterless_interpret {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} {f₁ f₂ : Realization 𝔅} {A : Modal.Formula ℕ} (A_letterless : A.Letterless) :

↑f₁ A = ↑f₂ A

source

theorem LO.ProvabilityLogic.Realization.iff_provable_letterless_interpret {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T U : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} {f₁ f₂ : Realization 𝔅} {A : Modal.Formula ℕ} (A_letterless : A.Letterless) :

U ⊢ ↑f₁ A ↔ U ⊢ ↑f₂ A

source

@[simp]

theorem LO.ProvabilityLogic.Realization.interpret.def_atom {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} {f : Realization 𝔅} {a : ℕ} :

↑f (Modal.Formula.atom a) = f.val a

source

@[simp]

theorem LO.ProvabilityLogic.Realization.interpret.def_imp {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} {f : Realization 𝔅} {A B : Modal.Formula ℕ} :

↑f (A ➝ B) = ↑f A ➝ ↑f B

source

@[simp]

theorem LO.ProvabilityLogic.Realization.interpret.def_bot {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} {f : Realization 𝔅} :

↑f ⊥ = ⊥

source

@[simp]

theorem LO.ProvabilityLogic.Realization.interpret.def_box {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} {f : Realization 𝔅} {A : Modal.Formula ℕ} :

↑f (□A) = ↑𝔅 (↑f A)

source

@[simp]

theorem LO.ProvabilityLogic.Realization.interpret.def_boxItr {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} {f : Realization 𝔅} {A : Modal.Formula ℕ} (n : ℕ) :

↑f (□^[n]A) = (↑𝔅)^[n] (↑f A)

source

@[simp]

theorem LO.ProvabilityLogic.Realization.interpret.iff_provable_atom {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T U : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} {f : Realization 𝔅} {a : ℕ} :

U ⊢ ↑f (Modal.Formula.atom a) ↔ U ⊢ f.val a

source

theorem LO.ProvabilityLogic.Realization.interpret.iff_provable_imp_inside {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T U : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} {f : Realization 𝔅} {A B : Modal.Formula ℕ} [DecidableEq (FirstOrder.Sentence L)] :

U ⊢ ↑f (A ➝ B) ⭤ ↑f A ➝ ↑f B

source

theorem LO.ProvabilityLogic.Realization.interpret.iff_provable_imp {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T U : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} {f : Realization 𝔅} {A B : Modal.Formula ℕ} [DecidableEq (FirstOrder.Sentence L)] :

U ⊢ ↑f (A ➝ B) ↔ U ⊢ ↑f A ➝ ↑f B

source

@[simp]

theorem LO.ProvabilityLogic.Realization.interpret.iff_provable_bot {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T U : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} {f : Realization 𝔅} :

U ⊢ ↑f ⊥ ↔ U ⊢ ⊥

source

theorem LO.ProvabilityLogic.Realization.interpret.iff_provable_box_inside {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T U : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} {f : Realization 𝔅} {A : Modal.Formula ℕ} :

U ⊢ ↑f (□A) ⭤ ↑𝔅 (↑f A)

source

theorem LO.ProvabilityLogic.Realization.interpret.iff_provable_box {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T U : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} {f : Realization 𝔅} {A : Modal.Formula ℕ} [DecidableEq (FirstOrder.Sentence L)] :

U ⊢ ↑f (□A) ↔ U ⊢ ↑𝔅 (↑f A)

source

theorem LO.ProvabilityLogic.Realization.interpret.iff_provable_boxItr_inside {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T U : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} {f : Realization 𝔅} {A : Modal.Formula ℕ} {n : ℕ} :

U ⊢ ↑f (□^[n]A) ⭤ (↑𝔅)^[n] (↑f A)

source

@[simp]

theorem LO.ProvabilityLogic.Realization.interpret.iff_provable_boxItr {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T U : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} {f : Realization 𝔅} {A : Modal.Formula ℕ} [DecidableEq (FirstOrder.Sentence L)] {n : ℕ} :

U ⊢ ↑f (□^[n]A) ↔ U ⊢ (↑𝔅)^[n] (↑f A)

source

theorem LO.ProvabilityLogic.Realization.interpret.iff_provable_neg_inside {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T U : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} {f : Realization 𝔅} {A : Modal.Formula ℕ} [DecidableEq (FirstOrder.Sentence L)] :

U ⊢ ↑f (∼A) ⭤ ∼↑f A

source

theorem LO.ProvabilityLogic.Realization.interpret.iff_provable_neg {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T U : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} {f : Realization 𝔅} {A : Modal.Formula ℕ} [DecidableEq (FirstOrder.Sentence L)] :

U ⊢ ↑f (∼A) ↔ U ⊢ ∼↑f A

source

theorem LO.ProvabilityLogic.Realization.interpret.iff_provable_or_inside {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T U : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} {f : Realization 𝔅} {A B : Modal.Formula ℕ} [DecidableEq (FirstOrder.Sentence L)] :

U ⊢ ↑f (A ⋎ B) ⭤ ↑f A ⋎ ↑f B

source

theorem LO.ProvabilityLogic.Realization.interpret.iff_provable_or {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T U : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} {f : Realization 𝔅} {A B : Modal.Formula ℕ} [DecidableEq (FirstOrder.Sentence L)] :

U ⊢ ↑f (A ⋎ B) ↔ U ⊢ ↑f A ⋎ ↑f B

source

theorem LO.ProvabilityLogic.Realization.interpret.iff_provable_and_inside {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T U : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} {f : Realization 𝔅} {A B : Modal.Formula ℕ} [DecidableEq (FirstOrder.Sentence L)] :

U ⊢ ↑f (A ⋏ B) ⭤ ↑f A ⋏ ↑f B

source

theorem LO.ProvabilityLogic.Realization.interpret.iff_provable_and' {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T U : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} {f : Realization 𝔅} {A B : Modal.Formula ℕ} [DecidableEq (FirstOrder.Sentence L)] :

U ⊢ ↑f (A ⋏ B) ↔ U ⊢ ↑f A ⋏ ↑f B

source

theorem LO.ProvabilityLogic.Realization.interpret.iff_provable_and {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T U : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} {f : Realization 𝔅} {A B : Modal.Formula ℕ} [DecidableEq (FirstOrder.Sentence L)] :

U ⊢ ↑f (A ⋏ B) ↔ U ⊢ ↑f A ∧ U ⊢ ↑f B

source

@[simp]

theorem LO.ProvabilityLogic.Realization.interpret.iff_provable_lconj₂ {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T U : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} {f : Realization 𝔅} [DecidableEq (FirstOrder.Sentence L)] {l : List (Modal.Formula ℕ)} :

U ⊢ ↑f (⋀l) ↔ ∀ A ∈ l, U ⊢ ↑f A

source

@[simp]

theorem LO.ProvabilityLogic.Realization.interpret.iff_provable_lconj' {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T U : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} {f : Realization 𝔅} [DecidableEq (FirstOrder.Sentence L)] {α✝ : Type u_1} {ι : Modal.Formula α✝ → Modal.Formula ℕ} {l : List (Modal.Formula α✝)} :

U ⊢ ↑f (List.conj' ι l) ↔ ∀ A ∈ l, U ⊢ ↑f (ι A)

source

@[simp]

theorem LO.ProvabilityLogic.Realization.interpret.iff_provable_fconj {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T U : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} {f : Realization 𝔅} [DecidableEq (FirstOrder.Sentence L)] {s : Finset (Modal.Formula ℕ)} :

U ⊢ ↑f s.conj ↔ ∀ A ∈ s, U ⊢ ↑f A

source

@[simp]

theorem LO.ProvabilityLogic.Realization.interpret.iff_provable_fconj' {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T U : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} {f : Realization 𝔅} [DecidableEq (FirstOrder.Sentence L)] {α✝ : Type u_1} {ι : Modal.Formula α✝ → Modal.Formula ℕ} {s : Finset (Modal.Formula α✝)} :

U ⊢ ↑f (s.conj' ι) ↔ ∀ A ∈ s, U ⊢ ↑f (ι A)

source

theorem LO.ProvabilityLogic.Realization.interpret.iff_provable_boxdot_inside {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T U : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} {f : Realization 𝔅} {A : Modal.Formula ℕ} [DecidableEq (FirstOrder.Sentence L)] :

U ⊢ ↑f (⊡A) ⭤ ↑f A ⋏ ↑𝔅 (↑f A)

source

theorem LO.ProvabilityLogic.Realization.interpret.iff_provable_boxdot {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T U : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} {f : Realization 𝔅} {A : Modal.Formula ℕ} [DecidableEq (FirstOrder.Sentence L)] :

U ⊢ ↑f (⊡A) ↔ U ⊢ ↑f A ⋏ ↑𝔅 (↑f A)

source

@[simp]

theorem LO.ProvabilityLogic.Realization.interpret.models₀_top {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} {f : Realization 𝔅} {M : Type u_2} [Nonempty M] [FirstOrder.Structure L M] :

M ⊧ₘ ↑f ⊤

source

@[simp]

theorem LO.ProvabilityLogic.Realization.interpret.models₀_bot {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} {f : Realization 𝔅} {M : Type u_2} [Nonempty M] [FirstOrder.Structure L M] :

¬M ⊧ₘ ↑f ⊥

source

@[simp]

theorem LO.ProvabilityLogic.Realization.interpret.iff_models₀_neg {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} {f : Realization 𝔅} {A : Modal.Formula ℕ} {M : Type u_2} [Nonempty M] [FirstOrder.Structure L M] :

M ⊧ₘ ↑f (∼A) ↔ ¬M ⊧ₘ ↑f A

source

@[simp]

theorem LO.ProvabilityLogic.Realization.interpret.iff_models₀_imp {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} {f : Realization 𝔅} {A B : Modal.Formula ℕ} {M : Type u_2} [Nonempty M] [FirstOrder.Structure L M] :

M ⊧ₘ ↑f (A ➝ B) ↔ M ⊧ₘ ↑f A → M ⊧ₘ ↑f B

source

@[simp]

theorem LO.ProvabilityLogic.Realization.interpret.iff_models₀_and {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} {f : Realization 𝔅} {A B : Modal.Formula ℕ} {M : Type u_2} [Nonempty M] [FirstOrder.Structure L M] :

M ⊧ₘ ↑f (A ⋏ B) ↔ M ⊧ₘ ↑f A ∧ M ⊧ₘ ↑f B

source

@[simp]

theorem LO.ProvabilityLogic.Realization.interpret.iff_models₀_or {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} {f : Realization 𝔅} {A B : Modal.Formula ℕ} {M : Type u_2} [Nonempty M] [FirstOrder.Structure L M] :

M ⊧ₘ ↑f (A ⋎ B) ↔ M ⊧ₘ ↑f A ∨ M ⊧ₘ ↑f B

source

@[simp]

theorem LO.ProvabilityLogic.Realization.interpret.iff_models₀_box {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} {f : Realization 𝔅} {A : Modal.Formula ℕ} {M : Type u_2} [Nonempty M] [FirstOrder.Structure L M] :

M ⊧ₘ ↑f (□A) ↔ M ⊧ₘ ↑𝔅 (↑f A)

source

@[simp]

theorem LO.ProvabilityLogic.Realization.interpret.iff_models₀_boxItr {L : FirstOrder.Language} [L.ReferenceableBy L] {T₀ T : FirstOrder.Theory L} {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T₀ T} {f : Realization 𝔅} {A : Modal.Formula ℕ} {M : Type u_2} [Nonempty M] [FirstOrder.Structure L M] {n : ℕ} :

M ⊧ₘ ↑f (□^[n]A) ↔ M ⊧ₘ (↑𝔅)^[n] (↑f A)