Foundation.IntProp.Kripke.Basic

source

structure LO.IntProp.Kripke.Frame :

Type 1

World : Type
Rel : _root_.Rel self.World self.World
world_nonempty : Nonempty self.World
rel_po : IsPartialOrder self.World self.Rel

Instances For

source

instance LO.IntProp.Kripke.instCoeSortFrameType :

CoeSort Frame Type

Equations

LO.IntProp.Kripke.instCoeSortFrameType = { coe := LO.IntProp.Kripke.Frame.World }

source

instance LO.IntProp.Kripke.instCoeFunFrameForallWorldForallProp :

CoeFun Frame fun (F : Frame) => F.World → F.World → Prop

Equations

LO.IntProp.Kripke.instCoeFunFrameForallWorldForallProp = { coe := LO.IntProp.Kripke.Frame.Rel }

source

instance LO.IntProp.Kripke.instNonemptyWorld {F : Frame} :

Nonempty F.World

source

instance LO.IntProp.Kripke.instIsPartialOrderWorldRel {F : Frame} :

IsPartialOrder F.World F.Rel

source

@[reducible, inline]

abbrev LO.IntProp.Kripke.Frame.Rel' {F : Frame} (x y : F.World) :

Prop

Equations

(x ≺ y) = F.Rel x y

Instances For

source

def LO.IntProp.Kripke.«term_≺_» :

Lean.TrailingParserDescr

Equations

LO.IntProp.Kripke.«term_≺_» = Lean.ParserDescr.trailingNode `LO.IntProp.Kripke.«term_≺_» 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≺ ") (Lean.ParserDescr.cat `term 46))

Instances For

source

theorem LO.IntProp.Kripke.Frame.rel_trans {F : Frame} {x y z : F.World} :

x ≺ y → y ≺ z → x ≺ z

source

theorem LO.IntProp.Kripke.Frame.rel_trans' {F : Frame} :

Transitive F.Rel

source

@[simp]

theorem LO.IntProp.Kripke.Frame.rel_refl {F : Frame} {x : F.World} :

x ≺ x

source

theorem LO.IntProp.Kripke.Frame.rel_refl' {F : Frame} :

Reflexive F.Rel

source

@[simp]

theorem LO.IntProp.Kripke.Frame.rel_antisymm {F : Frame} {x y : F.World} :

x ≺ y → y ≺ x → x = y

source

theorem LO.IntProp.Kripke.Frame.rel_antisymm' {F : Frame} :

AntiSymmetric F.Rel

source

@[reducible, inline]

abbrev LO.IntProp.Kripke.pointFrame :

Frame

Equations

LO.IntProp.Kripke.pointFrame = LO.IntProp.Kripke.Frame.mk Unit fun (x x : Unit) => True

Instances For

source

@[reducible, inline]

abbrev LO.IntProp.Kripke.FrameClass :

Type 1

Equations

LO.IntProp.Kripke.FrameClass = Set LO.IntProp.Kripke.Frame

Instances For

source

@[reducible, inline]

abbrev LO.IntProp.Kripke.AllFrameClass :

FrameClass

Equations

LO.IntProp.Kripke.AllFrameClass = Set.univ

Instances For

source

@[reducible, inline]

abbrev LO.IntProp.Kripke.SymmetricFrameClass :

FrameClass

Equations

LO.IntProp.Kripke.SymmetricFrameClass = {F : LO.IntProp.Kripke.Frame | Symmetric F.Rel}

Instances For

source

@[reducible, inline]

abbrev LO.IntProp.Kripke.ConfluentFrameClass :

FrameClass

Equations

LO.IntProp.Kripke.ConfluentFrameClass = {F : LO.IntProp.Kripke.Frame | Confluent F.Rel}

Instances For

source

@[reducible, inline]

abbrev LO.IntProp.Kripke.ConnectedFrameClass :

FrameClass

Equations

LO.IntProp.Kripke.ConnectedFrameClass = {F : LO.IntProp.Kripke.Frame | Connected F.Rel}

Instances For

source

@[reducible, inline]

abbrev LO.IntProp.Kripke.EuclideanFrameClass :

FrameClass

Equations

LO.IntProp.Kripke.EuclideanFrameClass = {F : LO.IntProp.Kripke.Frame | Euclidean F.Rel}

Instances For

source

structure LO.IntProp.Kripke.Valuation (F : Frame) :

Type

Val : F.World → ℕ → Prop
hereditary {w₁ w₂ : F.World} : w₁ ≺ w₂ → ∀ {a : ℕ}, self.Val w₁ a → self.Val w₂ a

Instances For

source

instance LO.IntProp.Kripke.instCoeFunValuationForallWorldForallNatProp {F : Frame} :

CoeFun (Valuation F) fun (x : Valuation F) => F.World → ℕ → Prop

Equations

LO.IntProp.Kripke.instCoeFunValuationForallWorldForallNatProp = { coe := LO.IntProp.Kripke.Valuation.Val }

source

structure LO.IntProp.Kripke.Modelextends LO.IntProp.Kripke.Frame :

Type 1

World : Type
Rel : _root_.Rel self.World self.World
world_nonempty : Nonempty self.World
rel_po : IsPartialOrder self.World self.Rel
Val : Valuation self.toFrame

Instances For

source

instance LO.IntProp.Kripke.instCoeFunModelForallWorldForallNatProp :

CoeFun Model fun (M : Model) => M.World → ℕ → Prop

Equations

LO.IntProp.Kripke.instCoeFunModelForallWorldForallNatProp = { coe := fun (m : LO.IntProp.Kripke.Model) => m.Val.Val }

source

def LO.IntProp.Formula.Kripke.Satisfies (M : Kripke.Model) (w : M.World) :

Formula ℕ → Prop

Equations

LO.IntProp.Formula.Kripke.Satisfies M w (LO.IntProp.Formula.atom a) = M.Val.Val w a
LO.IntProp.Formula.Kripke.Satisfies M w LO.IntProp.Formula.verum = True
LO.IntProp.Formula.Kripke.Satisfies M w LO.IntProp.Formula.falsum = False
LO.IntProp.Formula.Kripke.Satisfies M w (φ.and ψ) = (LO.IntProp.Formula.Kripke.Satisfies M w φ ∧ LO.IntProp.Formula.Kripke.Satisfies M w ψ)
LO.IntProp.Formula.Kripke.Satisfies M w (φ.or ψ) = (LO.IntProp.Formula.Kripke.Satisfies M w φ ∨ LO.IntProp.Formula.Kripke.Satisfies M w ψ)
LO.IntProp.Formula.Kripke.Satisfies M w φ.neg = ∀ {w' : M.World}, w ≺ w' → ¬LO.IntProp.Formula.Kripke.Satisfies M w' φ
LO.IntProp.Formula.Kripke.Satisfies M w (φ.imp ψ) = ∀ {w' : M.World}, w ≺ w' → LO.IntProp.Formula.Kripke.Satisfies M w' φ → LO.IntProp.Formula.Kripke.Satisfies M w' ψ

Instances For

source

instance LO.IntProp.Formula.Kripke.Satisfies.semantics (M : Kripke.Model) :

Semantics (Formula ℕ) M.World

Equations

LO.IntProp.Formula.Kripke.Satisfies.semantics M = { Realize := fun (w : M.World) => LO.IntProp.Formula.Kripke.Satisfies M w }

source

@[simp]

theorem LO.IntProp.Formula.Kripke.Satisfies.iff_models {M : Kripke.Model} {w : M.World} {φ : Formula ℕ} :

w ⊧ φ ↔ Satisfies M w φ

source

@[simp]

theorem LO.IntProp.Formula.Kripke.Satisfies.atom_def {M : Kripke.Model} {w : M.World} {a : ℕ} :

w ⊧ atom a ↔ M.Val.Val w a

source

@[simp]

theorem LO.IntProp.Formula.Kripke.Satisfies.top_def {M : Kripke.Model} {w : M.World} :

w ⊧ ⊤ ↔ True

source

@[simp]

theorem LO.IntProp.Formula.Kripke.Satisfies.bot_def {M : Kripke.Model} {w : M.World} :

w ⊧ ⊥ ↔ False

source

@[simp]

theorem LO.IntProp.Formula.Kripke.Satisfies.and_def {M : Kripke.Model} {w : M.World} {φ ψ : Formula ℕ} :

w ⊧ φ ⋏ ψ ↔ w ⊧ φ ∧ w ⊧ ψ

source

@[simp]

theorem LO.IntProp.Formula.Kripke.Satisfies.or_def {M : Kripke.Model} {w : M.World} {φ ψ : Formula ℕ} :

w ⊧ φ ⋎ ψ ↔ w ⊧ φ ∨ w ⊧ ψ

source

@[simp]

theorem LO.IntProp.Formula.Kripke.Satisfies.imp_def {M : Kripke.Model} {w : M.World} {φ ψ : Formula ℕ} :

w ⊧ φ ➝ ψ ↔ ∀ {w' : M.World}, w ≺ w' → w' ⊧ φ → w' ⊧ ψ

source

@[simp]

theorem LO.IntProp.Formula.Kripke.Satisfies.neg_def {M : Kripke.Model} {w : M.World} {φ : Formula ℕ} :

w ⊧ ∼φ ↔ ∀ {w' : M.World}, w ≺ w' → ¬w' ⊧ φ

source

instance LO.IntProp.Formula.Kripke.Satisfies.instTopWorldNat {M : Kripke.Model} :

Semantics.Top M.World

source

instance LO.IntProp.Formula.Kripke.Satisfies.instBotWorldNat {M : Kripke.Model} :

Semantics.Bot M.World

source

instance LO.IntProp.Formula.Kripke.Satisfies.instAndWorldNat {M : Kripke.Model} :

Semantics.And M.World

source

instance LO.IntProp.Formula.Kripke.Satisfies.instOrWorldNat {M : Kripke.Model} :

Semantics.Or M.World

source

theorem LO.IntProp.Formula.Kripke.Satisfies.formula_hereditary {M : Kripke.Model} {w w' : M.World} {φ : Formula ℕ} (hw : w ≺ w') :

w ⊧ φ → w' ⊧ φ

source

theorem LO.IntProp.Formula.Kripke.Satisfies.neg_equiv {M : Kripke.Model} {w : M.World} {φ : Formula ℕ} :

w ⊧ ∼φ ↔ w ⊧ φ ➝ ⊥

source

def LO.IntProp.Formula.Kripke.ValidOnModel (M : Kripke.Model) (φ : Formula ℕ) :

Prop

Equations

LO.IntProp.Formula.Kripke.ValidOnModel M φ = ∀ (w : M.World), w ⊧ φ

Instances For

source

instance LO.IntProp.Formula.Kripke.ValidOnModel.semantics :

Semantics (Formula ℕ) Kripke.Model

Equations

LO.IntProp.Formula.Kripke.ValidOnModel.semantics = { Realize := fun (M : LO.IntProp.Kripke.Model) => LO.IntProp.Formula.Kripke.ValidOnModel M }

source

@[simp]

theorem LO.IntProp.Formula.Kripke.ValidOnModel.iff_models {M : Kripke.Model} {φ : Formula ℕ} :

M ⊧ φ ↔ ValidOnModel M φ

source

theorem LO.IntProp.Formula.Kripke.ValidOnModel.verum {M : Kripke.Model} :

M ⊧ ⊤

source

theorem LO.IntProp.Formula.Kripke.ValidOnModel.andElim₁ {M : Kripke.Model} {φ ψ : Formula ℕ} :

M ⊧ φ ⋏ ψ ➝ φ

source

theorem LO.IntProp.Formula.Kripke.ValidOnModel.andElim₂ {M : Kripke.Model} {φ ψ : Formula ℕ} :

M ⊧ φ ⋏ ψ ➝ ψ

source

theorem LO.IntProp.Formula.Kripke.ValidOnModel.andInst₃ {M : Kripke.Model} {φ ψ : Formula ℕ} :

M ⊧ φ ➝ ψ ➝ φ ⋏ ψ

source

theorem LO.IntProp.Formula.Kripke.ValidOnModel.orInst₁ {M : Kripke.Model} {φ ψ : Formula ℕ} :

M ⊧ φ ➝ φ ⋎ ψ

source

theorem LO.IntProp.Formula.Kripke.ValidOnModel.orInst₂ {M : Kripke.Model} {φ ψ : Formula ℕ} :

M ⊧ ψ ➝ φ ⋎ ψ

source

theorem LO.IntProp.Formula.Kripke.ValidOnModel.orElim {M : Kripke.Model} {φ ψ χ : Formula ℕ} :

M ⊧ (φ ➝ χ) ➝ (ψ ➝ χ) ➝ φ ⋎ ψ ➝ χ

source

theorem LO.IntProp.Formula.Kripke.ValidOnModel.imply₁ {M : Kripke.Model} {φ ψ : Formula ℕ} :

M ⊧ φ ➝ ψ ➝ φ

source

theorem LO.IntProp.Formula.Kripke.ValidOnModel.imply₂ {M : Kripke.Model} {φ ψ χ : Formula ℕ} :

M ⊧ (φ ➝ ψ ➝ χ) ➝ (φ ➝ ψ) ➝ φ ➝ χ

source

theorem LO.IntProp.Formula.Kripke.ValidOnModel.mdp {M : Kripke.Model} {φ ψ : Formula ℕ} (hpq : M ⊧ φ ➝ ψ) (hp : M ⊧ φ) :

M ⊧ ψ

source

theorem LO.IntProp.Formula.Kripke.ValidOnModel.bot {M : Kripke.Model} :

¬M ⊧ ⊥

source

instance LO.IntProp.Formula.Kripke.ValidOnModel.instBotModelNat :

Semantics.Bot Kripke.Model

source

theorem LO.IntProp.Formula.Kripke.ValidOnModel.efq {M : Kripke.Model} {φ : Formula ℕ} :

M ⊧ Axioms.EFQ φ

source

theorem LO.IntProp.Formula.Kripke.ValidOnModel.neg_equiv {M : Kripke.Model} {φ : Formula ℕ} :

M ⊧ Axioms.NegEquiv φ

source

theorem LO.IntProp.Formula.Kripke.ValidOnModel.lem {M : Kripke.Model} {φ : Formula ℕ} :

Symmetric M.Rel → M ⊧ Axioms.LEM φ

source

theorem LO.IntProp.Formula.Kripke.ValidOnModel.dum {M : Kripke.Model} {φ ψ : Formula ℕ} :

Connected M.Rel → M ⊧ Axioms.Dummett φ ψ

source

theorem LO.IntProp.Formula.Kripke.ValidOnModel.wlem {M : Kripke.Model} {φ : Formula ℕ} :

Confluent M.Rel → M ⊧ Axioms.WeakLEM φ

source

def LO.IntProp.Formula.Kripke.ValidOnFrame (F : Kripke.Frame) (φ : Formula ℕ) :

Prop

Equations

LO.IntProp.Formula.Kripke.ValidOnFrame F φ = ∀ {V : LO.IntProp.Kripke.Valuation F}, { toFrame := F, Val := V } ⊧ φ

Instances For

source

instance LO.IntProp.Formula.Kripke.ValidOnFrame.semantics :

Semantics (Formula ℕ) Kripke.Frame

Equations

LO.IntProp.Formula.Kripke.ValidOnFrame.semantics = { Realize := fun (F : LO.IntProp.Kripke.Frame) => LO.IntProp.Formula.Kripke.ValidOnFrame F }

source

@[simp]

theorem LO.IntProp.Formula.Kripke.ValidOnFrame.models_iff {F : Kripke.Frame} {φ : Formula ℕ} :

F ⊧ φ ↔ ValidOnFrame F φ

source

theorem LO.IntProp.Formula.Kripke.ValidOnFrame.verum {F : Kripke.Frame} :

F ⊧ ⊤

source

theorem LO.IntProp.Formula.Kripke.ValidOnFrame.andElim₁ {F : Kripke.Frame} {φ ψ : Formula ℕ} :

F ⊧ φ ⋏ ψ ➝ φ

source

theorem LO.IntProp.Formula.Kripke.ValidOnFrame.andElim₂ {F : Kripke.Frame} {φ ψ : Formula ℕ} :

F ⊧ φ ⋏ ψ ➝ ψ

source

theorem LO.IntProp.Formula.Kripke.ValidOnFrame.andInst₃ {F : Kripke.Frame} {φ ψ : Formula ℕ} :

F ⊧ φ ➝ ψ ➝ φ ⋏ ψ

source

theorem LO.IntProp.Formula.Kripke.ValidOnFrame.orInst₁ {F : Kripke.Frame} {φ ψ : Formula ℕ} :

F ⊧ φ ➝ φ ⋎ ψ

source

theorem LO.IntProp.Formula.Kripke.ValidOnFrame.orInst₂ {F : Kripke.Frame} {φ ψ : Formula ℕ} :

F ⊧ ψ ➝ φ ⋎ ψ

source

theorem LO.IntProp.Formula.Kripke.ValidOnFrame.orElim {F : Kripke.Frame} {φ ψ χ : Formula ℕ} :

F ⊧ (φ ➝ χ) ➝ (ψ ➝ χ) ➝ φ ⋎ ψ ➝ χ

source

theorem LO.IntProp.Formula.Kripke.ValidOnFrame.imply₁ {F : Kripke.Frame} {φ ψ : Formula ℕ} :

F ⊧ φ ➝ ψ ➝ φ

source

theorem LO.IntProp.Formula.Kripke.ValidOnFrame.imply₂ {F : Kripke.Frame} {φ ψ χ : Formula ℕ} :

F ⊧ (φ ➝ ψ ➝ χ) ➝ (φ ➝ ψ) ➝ φ ➝ χ

source

theorem LO.IntProp.Formula.Kripke.ValidOnFrame.mdp {F : Kripke.Frame} {φ ψ : Formula ℕ} (hpq : F ⊧ φ ➝ ψ) (hp : F ⊧ φ) :

F ⊧ ψ

source

theorem LO.IntProp.Formula.Kripke.ValidOnFrame.efq {F : Kripke.Frame} {φ : Formula ℕ} :

F ⊧ Axioms.EFQ φ

source

theorem LO.IntProp.Formula.Kripke.ValidOnFrame.neg_equiv {F : Kripke.Frame} {φ : Formula ℕ} :

F ⊧ Axioms.NegEquiv φ

source

theorem LO.IntProp.Formula.Kripke.ValidOnFrame.lem {F : Kripke.Frame} {φ : Formula ℕ} (F_symm : Symmetric F.Rel) :

F ⊧ Axioms.LEM φ

source

theorem LO.IntProp.Formula.Kripke.ValidOnFrame.dum {F : Kripke.Frame} {φ ψ : Formula ℕ} (F_conn : Connected F.Rel) :

F ⊧ Axioms.Dummett φ ψ

source

theorem LO.IntProp.Formula.Kripke.ValidOnFrame.wlem {F : Kripke.Frame} {φ : Formula ℕ} (F_conf : Confluent F.Rel) :

F ⊧ Axioms.WeakLEM φ

source

theorem LO.IntProp.Formula.Kripke.ValidOnFrame.top {F : Kripke.Frame} :

F ⊧ ⊤

source

instance LO.IntProp.Formula.Kripke.ValidOnFrame.instTopFrameNat :

Semantics.Top Kripke.Frame

source

theorem LO.IntProp.Formula.Kripke.ValidOnFrame.bot {F : Kripke.Frame} :

¬F ⊧ ⊥

source

instance LO.IntProp.Formula.Kripke.ValidOnFrame.instBotFrameNat :

Semantics.Bot Kripke.Frame

source

def LO.IntProp.Formula.Kripke.ValidOnFrameClass (C : Kripke.FrameClass) (φ : Formula ℕ) :

Prop

Equations

LO.IntProp.Formula.Kripke.ValidOnFrameClass C φ = ∀ F ∈ C, F ⊧ φ

Instances For

source

instance LO.IntProp.Formula.Kripke.ValidOnFrameClass.semantics :

Semantics (Formula ℕ) Kripke.FrameClass

Equations

LO.IntProp.Formula.Kripke.ValidOnFrameClass.semantics = { Realize := fun (C : LO.IntProp.Kripke.FrameClass) => LO.IntProp.Formula.Kripke.ValidOnFrameClass C }

source

@[simp]

theorem LO.IntProp.Formula.Kripke.ValidOnFrameClass.models_iff {C : Kripke.FrameClass} {φ : Formula ℕ} :

C ⊧ φ ↔ ValidOnFrameClass C φ

source

theorem LO.IntProp.Formula.Kripke.ValidOnFrameClass.bot {C : Kripke.FrameClass} (h_nonempty : Set.Nonempty C) :

¬C ⊧ ⊥

source

def LO.IntProp.Kripke.Frame.theorems (F : Frame) :

Set (Formula ℕ)

A set of formula that valid on frame F.

Equations

F.theorems = {φ : LO.IntProp.Formula ℕ | F ⊧ φ}

Instances For

source

def LO.IntProp.Kripke.FrameClass.DefinedBy (C : FrameClass) (T : Set (Formula ℕ)) :

Prop

Equations

C.DefinedBy T = ∀ (F : LO.IntProp.Kripke.Frame), F ∈ C ↔ F ⊧* T

Instances For

source

theorem LO.IntProp.Hilbert.Kripke.sound_hilbert_of_frameclass {φ : Formula ℕ} {C : Kripke.FrameClass} {T : Set (Formula ℕ)} (definedBy : C.DefinedBy T) :

{ axioms := 𝗘𝗙𝗤 ∪ T } ⊢! φ → C ⊧ φ

source

theorem LO.IntProp.Hilbert.Kripke.sound_of_equiv_frameclass_hilbert {H : Hilbert ℕ} {φ : Formula ℕ} {C : Kripke.FrameClass} {T : Set (Formula ℕ)} (definedBy : C.DefinedBy T) (heq : { axioms := 𝗘𝗙𝗤 ∪ T } =ₛ H) :

H ⊢! φ → C ⊧ φ

source

instance LO.IntProp.Hilbert.Kripke.instSound {H : Hilbert ℕ} {C : Kripke.FrameClass} {T : Set (Formula ℕ)} (definedBy : C.DefinedBy T) (heq : { axioms := 𝗘𝗙𝗤 ∪ T } =ₛ H) :

Sound H C

source

theorem LO.IntProp.Hilbert.Kripke.unprovable_bot {H : Hilbert ℕ} {C : Kripke.FrameClass} [sound : Sound H C] (hNonempty : Set.Nonempty C) :

H ⊬ ⊥

source

theorem LO.IntProp.Hilbert.Kripke.consistent {H : Hilbert ℕ} {C : Kripke.FrameClass} [Sound H C] (h_nonempty : Set.Nonempty C) :

H.Consistent

source

instance LO.IntProp.Hilbert.Int.Kripke.sound :

Sound (Hilbert.Int ℕ) Kripke.AllFrameClass

source

instance LO.IntProp.Hilbert.Int.instConsistentNat :

(Hilbert.Int ℕ).Consistent

source

instance LO.IntProp.Hilbert.KC.Kripke.sound :

Sound (Hilbert.KC ℕ) Kripke.ConfluentFrameClass

source

instance LO.IntProp.Hilbert.KC.instConsistentNat :

(Hilbert.KC ℕ).Consistent

source

instance LO.IntProp.Hilbert.LC.Kripke.sound :

Sound (Hilbert.LC ℕ) Kripke.ConnectedFrameClass

source

instance LO.IntProp.Hilbert.LC.instConsistentNat :

(Hilbert.LC ℕ).Consistent

source

instance LO.IntProp.Hilbert.Cl.Kripke.sound :

Sound (Hilbert.Cl ℕ) Kripke.EuclideanFrameClass

source

instance LO.IntProp.Hilbert.Cl.instConsistentNat :

(Hilbert.Cl ℕ).Consistent