Basic

def LO.ProvabilityLogic.Realization (L : FirstOrder.Language) : Type u_1

Mapping modal prop vars to first-order sentence

Equations

• LO.ProvabilityLogic.Realization L = (ℕ → LO.FirstOrder.Sentence L)

def LO.ProvabilityLogic.Realization.interpret {L : FirstOrder.Language} [FirstOrder.Semiterm.Operator.GoedelNumber L (FirstOrder.Sentence L)] {T U : FirstOrder.Theory L} (f : Realization L) (𝔅 : FirstOrder.DerivabilityCondition.ProvabilityPredicate T U) : Modal.Formula ℕ → FirstOrder.Sentence L

Mapping modal formulae to first-order sentence

Equations

• f.interpret 𝔅 (LO.Modal.Formula.atom a) = f a
• f.interpret 𝔅 φ.box = ↑𝔅 (f.interpret 𝔅 φ)
• f.interpret 𝔅 LO.Modal.Formula.falsum = ⊥
• f.interpret 𝔅 (φ.imp ψ) = f.interpret 𝔅 φ ==> f.interpret 𝔅 ψ

class LO.ProvabilityLogic.ArithmeticalSound {L : FirstOrder.Language} [FirstOrder.Semiterm.Operator.GoedelNumber L (FirstOrder.Sentence L)] {T U : FirstOrder.Theory L} (Λ : Modal.Logic) (𝔅 : FirstOrder.DerivabilityCondition.ProvabilityPredicate T U) : Prop

Imported declaration from the Incompleteness formalization.

• sound {φ : Modal.Formula ℕ} : φ ∈ Λ → ∀ {f : Realization L}, U ⊢!. f.interpret 𝔅 φ

class LO.ProvabilityLogic.ArithmeticalComplete {L : FirstOrder.Language} [FirstOrder.Semiterm.Operator.GoedelNumber L (FirstOrder.Sentence L)] {T U : FirstOrder.Theory L} (Λ : Modal.Logic) (𝔅 : FirstOrder.DerivabilityCondition.ProvabilityPredicate T U) : Prop

Imported declaration from the Incompleteness formalization.

• complete {φ : Modal.Formula ℕ} : (∀ {f : Realization L}, U ⊢!. f.interpret 𝔅 φ) → φ ∈ Λ

theorem LO.ProvabilityLogic.arithmetical_soundness_N {L : FirstOrder.Language} [FirstOrder.Semiterm.Operator.GoedelNumber L (FirstOrder.Sentence L)] [L.DecidableEq] {T U : FirstOrder.Theory L} [T wkn U] {𝔅 : FirstOrder.DerivabilityCondition.ProvabilityPredicate T U} {φ : Modal.Formula ℕ} (h : Modal.Hilbert.N ⊢! φ) {f : Realization L} : U ⊢!. f.interpret 𝔅 φ

theorem LO.ProvabilityLogic.arithmetical_soundness_GL {L : FirstOrder.Language} [FirstOrder.Semiterm.Operator.GoedelNumber L (FirstOrder.Sentence L)] [L.DecidableEq] {T U : FirstOrder.Theory L} [T wkn U] {𝔅 : FirstOrder.DerivabilityCondition.ProvabilityPredicate T U} {φ : Modal.Formula ℕ} [FirstOrder.DerivabilityCondition.Diagonalization T] [𝔅.HBL] (h : Modal.Hilbert.GL ⊢! φ) {f : Realization L} : U ⊢!. f.interpret 𝔅 φ

instance LO.ProvabilityLogic.instArithmeticalSoundGLStandardDP (T : FirstOrder.Theory ℒₒᵣ) [𝐈Sg1 wkn T] [T.Delta1Definable] : ArithmeticalSound Modal.Logic.GL (T.standardDP T)