Mapping modal prop vars to first-order sentence
Equations
- LO.ProvabilityLogic.Realization α L = (α → LO.FirstOrder.Sentence L)
Instances For
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)
:
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 𝔅 ψ
Instances For
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)
:
- sound {φ : Modal.Formula α} : Λ ⊢! φ → ∀ {f : Realization α L}, U ⊢!. f.interpret 𝔅 φ
Instances
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)
:
- complete {φ : Modal.Formula α} : (∀ {f : Realization α L}, U ⊢!. f.interpret 𝔅 φ) → Λ ⊢! φ
Instances
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)