Documentation

Foundation.InterpretabilityLogic.Veltman.AxiomR

class LO.InterpretabilityLogic.Veltman.Frame.HasAxiomR (F : Frame) :

S_R {x y z u v : F.World} : x ≺ y → y ≺ z → z ≺[x] u → u ≺ v → z ≺[y] v

Instances

@[simp]

theorem LO.InterpretabilityLogic.Veltman.validate_axiomR_of_HasAxiomR {F : Frame} {φ ψ χ : Formula ℕ} [F.IsIL] [F.HasAxiomR] :

F ⊧ Axioms.R φ ψ χ

theorem LO.InterpretabilityLogic.Veltman.Frame.HasAxiomR.of_validate_axiomP₀ {F : Frame} [F.IsIL] (h : F ⊧ Axioms.P₀ (Formula.atom 0) (Formula.atom 1)) :

theorem LO.InterpretabilityLogic.Veltman.validate_axiomP₀_of_validate_axiomR {F : Frame} {φ ψ : Formula ℕ} [F.IsIL] (h : F ⊧ Axioms.R (Formula.atom 0) (Formula.atom 1) (Formula.atom 2)) :

F ⊧ Axioms.P₀ φ ψ

theorem LO.InterpretabilityLogic.Veltman.TFAE_HasAxiomR {F : Frame} [F.IsIL] :

[F.HasAxiomR, F ⊧ Axioms.R (Formula.atom 0) (Formula.atom 1) (Formula.atom 2), F ⊧ Axioms.P₀ (Formula.atom 0) (Formula.atom 1)].TFAE

theorem LO.InterpretabilityLogic.Veltman.Frame.HasAxiomR.of_validate_axiomR {F : Frame} [F.IsIL] (h : F ⊧ Axioms.R (Formula.atom 0) (Formula.atom 1) (Formula.atom 2)) :

@[simp]

theorem LO.InterpretabilityLogic.Veltman.validate_axiomP₀_of_HasAxiomR {F : Frame} {φ ψ : Formula ℕ} [F.IsIL] [F.HasAxiomR] :

F ⊧ Axioms.P₀ φ ψ