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 : LO.FirstOrder.Theory L} {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 𝔅 p.box = 𝔅.pr (f.interpret 𝔅 p)
• f.interpret 𝔅 LO.Modal.Formula.falsum = ⊥
• f.interpret 𝔅 (p.imp q) = f.interpret 𝔅 p ➝ f.interpret 𝔅 q

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

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

theorem LO.ProvabilityLogic.ArithmeticalSound.sound {L : LO.FirstOrder.Language} {α : Type u} {T : LO.FirstOrder.Theory L} {U : LO.FirstOrder.Theory L} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] {Λ : LO.Modal.Hilbert α} {𝔅 : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate T U} [self : LO.ProvabilityLogic.ArithmeticalSound Λ 𝔅] {p : LO.Modal.Formula α} : Λ ⊢! p → ∀ {f : LO.ProvabilityLogic.Realization α L}, U ⊢!. f.interpret 𝔅 p

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

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

theorem LO.ProvabilityLogic.ArithmeticalComplete.complete {L : LO.FirstOrder.Language} {α : Type u} {T : LO.FirstOrder.Theory L} {U : LO.FirstOrder.Theory L} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)] {Λ : LO.Modal.Hilbert α} {𝔅 : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate T U} [self : LO.ProvabilityLogic.ArithmeticalComplete Λ 𝔅] {p : LO.Modal.Formula α} : (∀ {f : LO.ProvabilityLogic.Realization α L}, U ⊢!. f.interpret 𝔅 p) → Λ ⊢! p

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

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

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

Equations

• LO.ProvabilityLogic.instArithmeticalSoundGLStandardDP T = { sound := ⋯ }