def LO.Modal.Standard.Provability.realization (L : LO.FirstOrder.Language) (α : Type u) : Type (max u u_2)

Mapping modal prop vars to first-order sentence

Equations

• LO.Modal.Standard.Provability.realization L α = (α → LO.FirstOrder.Sentence L)

def LO.Modal.Standard.Provability.interpretation {α : Type u_1} {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] (f : LO.Modal.Standard.Provability.realization L α) (β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L) : LO.Modal.Standard.Formula α → LO.FirstOrder.Sentence L

Mapping modal formulae to first-order sentence

Equations

• LO.Modal.Standard.Provability.interpretation f β (LO.Modal.Standard.Formula.atom a) = f a
• LO.Modal.Standard.Provability.interpretation f β p.box = ⦍β⦎LO.Modal.Standard.Provability.interpretation f β p
• LO.Modal.Standard.Provability.interpretation f β LO.Modal.Standard.Formula.falsum = ⊥
• LO.Modal.Standard.Provability.interpretation f β (p.imp q) = LO.Modal.Standard.Provability.interpretation f β p ⟶ LO.Modal.Standard.Provability.interpretation f β q

def LO.Modal.Standard.Provability.«term_[_]_» : Lean.TrailingParserDescr

Equations

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

theorem LO.Modal.Standard.Provability.interpretation.imp_def {L : LO.FirstOrder.Language} {α : Type u_1} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] {f : LO.Modal.Standard.Provability.realization L α} {β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L} {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} : LO.Modal.Standard.Provability.interpretation f β (p ⟶ q) = LO.Modal.Standard.Provability.interpretation f β p ⟶ LO.Modal.Standard.Provability.interpretation f β q

theorem LO.Modal.Standard.Provability.interpretation.box_def {L : LO.FirstOrder.Language} {α : Type u_1} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] {f : LO.Modal.Standard.Provability.realization L α} {β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L} {p : LO.Modal.Standard.Formula α} : LO.Modal.Standard.Provability.interpretation f β (□p) = ⦍β⦎LO.Modal.Standard.Provability.interpretation f β p

theorem LO.Modal.Standard.Provability.interpretation.neg_def {L : LO.FirstOrder.Language} {α : Type u_1} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] {f : LO.Modal.Standard.Provability.realization L α} {β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L} {p : LO.Modal.Standard.Formula α} : LO.Modal.Standard.Provability.interpretation f β (~p) = LO.Modal.Standard.Provability.interpretation f β p ⟶ ⊥

theorem LO.Modal.Standard.Provability.arithmetical_soundness_K4Loeb {α : Type u_1} {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] [DecidableEq (LO.FirstOrder.Sentence L)] (T₀ : LO.FirstOrder.Theory L) (T : LO.FirstOrder.Theory L) [T₀ ≼ T] [LO.FirstOrder.DerivabilityCondition.Diagonalization T₀] (β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L) {p : LO.Modal.Standard.Formula α} [β.HBL T₀ T] (h : 𝐊𝟒(𝐋) ⊢! p) {f : LO.Modal.Standard.Provability.realization L α} : T ⊢! LO.Modal.Standard.Provability.interpretation f β p

theorem LO.Modal.Standard.Provability.arithmetical_soundness_GL {α : Type u_1} [DecidableEq α] {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] [DecidableEq (LO.FirstOrder.Sentence L)] (T₀ : LO.FirstOrder.Theory L) (T : LO.FirstOrder.Theory L) [T₀ ≼ T] [LO.FirstOrder.DerivabilityCondition.Diagonalization T₀] (β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L) {p : LO.Modal.Standard.Formula α} [β.HBL T₀ T] (h : 𝐆𝐋 ⊢! p) {f : LO.Modal.Standard.Provability.realization L α} : T ⊢! LO.Modal.Standard.Provability.interpretation f β p

theorem LO.Modal.Standard.Provability.arithmetical_soundness_N {α : Type u_1} {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] [DecidableEq (LO.FirstOrder.Sentence L)] (T₀ : LO.FirstOrder.Theory L) (T : LO.FirstOrder.Theory L) [T₀ ≼ T] (β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L) {p : LO.Modal.Standard.Formula α} [β.HBL T₀ T] (h : 𝐍 ⊢! p) {f : LO.Modal.Standard.Provability.realization L α} : T ⊢! LO.Modal.Standard.Provability.interpretation f β p