def LO.ProvabilityLogic.Realization (α : Type u) (L : FirstOrder.Language) : Type (max u 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} {α : Type u} [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} {α : Type u} {T U : FirstOrder.Theory L} [FirstOrder.Semiterm.Operator.GoedelNumber L (FirstOrder.Sentence L)] (Λ : Modal.Hilbert α) (𝔅 : FirstOrder.DerivabilityCondition.ProvabilityPredicate T U) : Prop

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

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

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

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

theorem LO.ProvabilityLogic.arithmetical_soundness_GL {α : Type u} {L : FirstOrder.Language} [FirstOrder.Semiterm.Operator.GoedelNumber L (FirstOrder.Sentence L)] [L.DecidableEq] {T U : FirstOrder.Theory L} [T ≼ 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 {α : Type u} (T : FirstOrder.Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] [T.Delta1Definable] : ArithmeticalSound (Modal.Hilbert.GL α) (T.standardDP T)