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

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

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

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

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

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

instance LO.ProvabilityLogic.instArithmeticalSoundGLStandardDP {α : Type u} (T : LO.FirstOrder.Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] [T.Delta1Definable] : LO.ProvabilityLogic.ArithmeticalSound (LO.Modal.Hilbert.GL α) (T.standardDP T)

Equations

• ⋯ = ⋯