def
LO.Modal.Standard.Provability.realization
(L : LO.FirstOrder.Language)
(α : Type u)
:
Type (max u u_2)
Mapping modal prop vars to first-order sentence
Equations
Instances For
def
LO.Modal.Standard.Provability.interpretation
{α : Type u_1}
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)]
(f : LO.Modal.Standard.Provability.realization L α)
(β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L)
:
Mapping modal formulae to first-order sentence
Equations
- LO.Modal.Standard.Provability.interpretation f β (LO.Modal.Standard.Formula.atom a) = f a
- LO.Modal.Standard.Provability.interpretation f β p.box = ⦍β⦎LO.Modal.Standard.Provability.interpretation f β p
- LO.Modal.Standard.Provability.interpretation f β LO.Modal.Standard.Formula.falsum = ⊥
- LO.Modal.Standard.Provability.interpretation f β (p.imp q) = LO.Modal.Standard.Provability.interpretation f β p ⟶ LO.Modal.Standard.Provability.interpretation f β q
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Modal.Standard.Provability.interpretation.imp_def
{L : LO.FirstOrder.Language}
{α : Type u_1}
[LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)]
{f : LO.Modal.Standard.Provability.realization L α}
{β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L}
{p : LO.Modal.Standard.Formula α}
{q : LO.Modal.Standard.Formula α}
:
theorem
LO.Modal.Standard.Provability.interpretation.box_def
{L : LO.FirstOrder.Language}
{α : Type u_1}
[LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)]
{f : LO.Modal.Standard.Provability.realization L α}
{β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L}
{p : LO.Modal.Standard.Formula α}
:
theorem
LO.Modal.Standard.Provability.interpretation.neg_def
{L : LO.FirstOrder.Language}
{α : Type u_1}
[LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)]
{f : LO.Modal.Standard.Provability.realization L α}
{β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L}
{p : LO.Modal.Standard.Formula α}
:
theorem
LO.Modal.Standard.Provability.arithmetical_soundness_K4Loeb
{α : Type u_1}
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)]
[DecidableEq (LO.FirstOrder.Sentence L)]
(T₀ : LO.FirstOrder.Theory L)
(T : LO.FirstOrder.Theory L)
[T₀ ≼ T]
[LO.FirstOrder.DerivabilityCondition.Diagonalization T₀]
(β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L)
{p : LO.Modal.Standard.Formula α}
[β.HBL T₀ T]
(h : 𝐊𝟒(𝐋) ⊢! p)
{f : LO.Modal.Standard.Provability.realization L α}
:
theorem
LO.Modal.Standard.Provability.arithmetical_soundness_GL
{α : Type u_1}
[DecidableEq α]
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)]
[DecidableEq (LO.FirstOrder.Sentence L)]
(T₀ : LO.FirstOrder.Theory L)
(T : LO.FirstOrder.Theory L)
[T₀ ≼ T]
[LO.FirstOrder.DerivabilityCondition.Diagonalization T₀]
(β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L)
{p : LO.Modal.Standard.Formula α}
[β.HBL T₀ T]
(h : 𝐆𝐋 ⊢! p)
{f : LO.Modal.Standard.Provability.realization L α}
:
theorem
LO.Modal.Standard.Provability.arithmetical_soundness_N
{α : Type u_1}
{L : LO.FirstOrder.Language}
[LO.FirstOrder.Semiterm.Operator.GoedelNumber L (LO.FirstOrder.Sentence L)]
[DecidableEq (LO.FirstOrder.Sentence L)]
(T₀ : LO.FirstOrder.Theory L)
(T : LO.FirstOrder.Theory L)
[T₀ ≼ T]
(β : LO.FirstOrder.DerivabilityCondition.ProvabilityPredicate L L)
{p : LO.Modal.Standard.Formula α}
[β.HBL T₀ T]
(h : 𝐍 ⊢! p)
{f : LO.Modal.Standard.Provability.realization L α}
: