@[reducible, inline]

abbrev LO.Propositional.SubformulaOf (φ : Formula ℕ) : Type

Equations

• LO.Propositional.SubformulaOf φ = { ψ : LO.Propositional.Formula ℕ // ψ ∈ φ.subformulas }

instance LO.Propositional.instFintypeSubformulaOf {φ : Formula ℕ} : Fintype (SubformulaOf φ)

Equations

• LO.Propositional.instFintypeSubformulaOf = { elems := Finset.univ, complete := ⋯ }

@[reducible, inline]

abbrev LO.Propositional.SubformulaSubsets (φ : Formula ℕ) : Type

Equations

• LO.Propositional.SubformulaSubsets φ = Finset (LO.Propositional.SubformulaOf φ)

@[reducible, inline]

abbrev LO.Propositional.HintikkaPair (φ : Formula ℕ) : Type

Equations

• LO.Propositional.HintikkaPair φ = (LO.Propositional.SubformulaSubsets φ × LO.Propositional.SubformulaSubsets φ)

def LO.Propositional.HintikkaPair.Consistent {φ : Formula ℕ} (L : Logic ℕ) (H : HintikkaPair φ) : Prop

Equations

• LO.Propositional.HintikkaPair.Consistent L H = (L ⊬ (⩕ (x : LO.Propositional.SubformulaOf φ) ∈ H.1, ↑x) ➝ ⩖ (x : LO.Propositional.SubformulaOf φ) ∈ H.2, ↑x)

theorem LO.Propositional.HintikkaPair.iff_consistent {φ : Formula ℕ} {L : Logic ℕ} {H : HintikkaPair φ} : Consistent L H ↔ ¬L ⊢ (⩕ (x : SubformulaOf φ) ∈ H.1, ↑x) ➝ ⩖ (x : SubformulaOf φ) ∈ H.2, ↑x

theorem LO.Propositional.HintikkaPair.iff_not_consistent {φ : Formula ℕ} {L : Logic ℕ} {H : HintikkaPair φ} : ¬Consistent L H ↔ L ⊢ (⩕ (x : SubformulaOf φ) ∈ H.1, ↑x) ➝ ⩖ (x : SubformulaOf φ) ∈ H.2, ↑x

def LO.Propositional.HintikkaPair.Saturated {φ : Formula ℕ} (H : HintikkaPair φ) : Prop

Equations

• H.Saturated = (H.1 ∪ H.2 = Finset.univ)

theorem LO.Propositional.HintikkaPair.mem₁_of_not_mem₂_of_saturated {φ : Formula ℕ} {H : HintikkaPair φ} {ψ : SubformulaOf φ} (h : H.Saturated) : ψ ∉ H.2 → ψ ∈ H.1

theorem LO.Propositional.HintikkaPair.mem₂_of_not_mem₁_of_saturated {φ : Formula ℕ} {H : HintikkaPair φ} {ψ : SubformulaOf φ} (h : H.Saturated) : ψ ∉ H.1 → ψ ∈ H.2

def LO.Propositional.HintikkaPair.insert₁ {φ : Formula ℕ} (H : HintikkaPair φ) (ψ : { ψ : Formula ℕ // ψ ∈ φ.subformulas }) : HintikkaPair φ

Equations

• H.insert₁ ψ = (insert ψ H.1, H.2)

def LO.Propositional.HintikkaPair.insert₂ {φ : Formula ℕ} (H : HintikkaPair φ) (ψ : { ψ : Formula ℕ // ψ ∈ φ.subformulas }) : HintikkaPair φ

Equations

• H.insert₂ ψ = (H.1, insert ψ H.2)

theorem LO.Propositional.HintikkaPair.either_consistent_insert {φ : Formula ℕ} {L : Logic ℕ} {H : HintikkaPair φ} [Entailment.VF L] (H_consis : Consistent L H) (ψ : { ψ : Formula ℕ // ψ ∈ φ.subformulas }) : Consistent L (H.insert₁ ψ) ∨ Consistent L (H.insert₂ ψ)

noncomputable def LO.Propositional.HintikkaPair.lindenbaum.next {φ : Formula ℕ} (L : Logic ℕ) (ψ : SubformulaOf φ) (H : HintikkaPair φ) : HintikkaPair φ

Equations

• LO.Propositional.HintikkaPair.lindenbaum.next L ψ H = if LO.Propositional.HintikkaPair.Consistent L (H.insert₁ ψ) then H.insert₁ ψ else H.insert₂ ψ

theorem LO.Propositional.HintikkaPair.lindenbaum.next_consistent {L : Logic ℕ} {φ : Formula ℕ} {H : HintikkaPair φ} [Entailment.VF L] {ψ : SubformulaOf φ} (H_consis : Consistent L H) : Consistent L (next L ψ H)

theorem LO.Propositional.HintikkaPair.lindenbaum.next_monotone₁ {L : Logic ℕ} {φ : Formula ℕ} {H : HintikkaPair φ} [Entailment.VF L] {ψ : SubformulaOf φ} : H.1 ⊆ (next L ψ H).1

theorem LO.Propositional.HintikkaPair.lindenbaum.next_monotone₂ {L : Logic ℕ} {φ : Formula ℕ} {H : HintikkaPair φ} [Entailment.VF L] {ψ : SubformulaOf φ} : H.2 ⊆ (next L ψ H).2

theorem LO.Propositional.HintikkaPair.lindenbaum.next_either_mem {L : Logic ℕ} {φ : Formula ℕ} {H : HintikkaPair φ} [Entailment.VF L] (ψ : SubformulaOf φ) : ψ ∈ (next L ψ H).1 ∨ ψ ∈ (next L ψ H).2

noncomputable def LO.Propositional.HintikkaPair.lindenbaum.enum {φ : Formula ℕ} (L : Logic ℕ) (H : HintikkaPair φ) : List (SubformulaOf φ) → HintikkaPair φ

Equations

• LO.Propositional.HintikkaPair.lindenbaum.enum L H [] = H
• LO.Propositional.HintikkaPair.lindenbaum.enum L H (ψ :: Δ) = LO.Propositional.HintikkaPair.lindenbaum.next L ψ (LO.Propositional.HintikkaPair.lindenbaum.enum L H Δ)

theorem LO.Propositional.HintikkaPair.lindenbaum.enum_consistent {L : Logic ℕ} {φ : Formula ℕ} {H : HintikkaPair φ} [Entailment.VF L] (H_consis : Consistent L H) (Γ : List (SubformulaOf φ)) : Consistent L (enum L H Γ)

theorem LO.Propositional.HintikkaPair.lindenbaum.enum_monotone₁ {L : Logic ℕ} {φ : Formula ℕ} {H : HintikkaPair φ} [Entailment.VF L] {Γ : List (SubformulaOf φ)} : H.1 ⊆ (enum L H Γ).1

theorem LO.Propositional.HintikkaPair.lindenbaum.enum_monotone₂ {L : Logic ℕ} {φ : Formula ℕ} {H : HintikkaPair φ} [Entailment.VF L] {Γ : List (SubformulaOf φ)} : H.2 ⊆ (enum L H Γ).2

theorem LO.Propositional.HintikkaPair.lindenbaum.enum_of_mem {L : Logic ℕ} {φ : Formula ℕ} {H : HintikkaPair φ} [Entailment.VF L] {Γ : List (SubformulaOf φ)} {ψ : SubformulaOf φ} (hψ : ψ ∈ Γ) : ψ ∈ (enum L H Γ).1 ∨ ψ ∈ (enum L H Γ).2

noncomputable def LO.Propositional.HintikkaPair.lindenbaum.sat {φ : Formula ℕ} (L : Logic ℕ) (H : HintikkaPair φ) : HintikkaPair φ

Equations

• LO.Propositional.HintikkaPair.lindenbaum.sat L H = LO.Propositional.HintikkaPair.lindenbaum.enum L H Finset.univ.toList

theorem LO.Propositional.HintikkaPair.lindenbaum.sat_saturated {L : Logic ℕ} {φ : Formula ℕ} {H : HintikkaPair φ} [Entailment.VF L] : (sat L H).Saturated

theorem LO.Propositional.HintikkaPair.lindenbaum {φ : Formula ℕ} {L : Logic ℕ} [Entailment.VF L] (H : HintikkaPair φ) (H_consis : Consistent L H) : ∃ (H' : HintikkaPair φ), H.1 ⊆ H'.1 ∧ H.2 ⊆ H'.2 ∧ Consistent L H' ∧ H'.Saturated

@[reducible, inline]

abbrev LO.Propositional.ConsistentSaturatedHintikkaPair (L : Logic ℕ) (φ : Formula ℕ) : Type

Equations

• LO.Propositional.ConsistentSaturatedHintikkaPair L φ = { H : LO.Propositional.HintikkaPair φ // LO.Propositional.HintikkaPair.Consistent L H ∧ H.Saturated }

theorem LO.Propositional.ConsistentSaturatedHintikkaPair.lindenbaum {φ : Formula ℕ} {L : Logic ℕ} [Entailment.VF L] (H : HintikkaPair φ) (H_consis : HintikkaPair.Consistent L H) : ∃ (H' : ConsistentSaturatedHintikkaPair L φ), H.1 ⊆ (↑H').1 ∧ H.2 ⊆ (↑H').2

@[simp]

theorem LO.Propositional.ConsistentSaturatedHintikkaPair.consistent {φ : Formula ℕ} {L : Logic ℕ} [Entailment.VF L] (H : ConsistentSaturatedHintikkaPair L φ) : HintikkaPair.Consistent L ↑H

@[simp]

theorem LO.Propositional.ConsistentSaturatedHintikkaPair.saturated {φ : Formula ℕ} {L : Logic ℕ} [Entailment.VF L] (H : ConsistentSaturatedHintikkaPair L φ) : (↑H).Saturated

theorem LO.Propositional.ConsistentSaturatedHintikkaPair.not_mem_both {φ : Formula ℕ} {L : Logic ℕ} {H : ConsistentSaturatedHintikkaPair L φ} [Entailment.VF L] {ψ : SubformulaOf φ} : ¬(ψ ∈ (↑H).1 ∧ ψ ∈ (↑H).2)

theorem LO.Propositional.ConsistentSaturatedHintikkaPair.iff_mem₁_not_mem₂ {φ : Formula ℕ} {L : Logic ℕ} {H : ConsistentSaturatedHintikkaPair L φ} [Entailment.VF L] {ψ : SubformulaOf φ} : ψ ∈ (↑H).1 ↔ ψ ∉ (↑H).2

theorem LO.Propositional.ConsistentSaturatedHintikkaPair.iff_mem₂_not_mem₁ {φ : Formula ℕ} {L : Logic ℕ} {H : ConsistentSaturatedHintikkaPair L φ} [Entailment.VF L] {ψ : SubformulaOf φ} : ψ ∈ (↑H).2 ↔ ψ ∉ (↑H).1

theorem LO.Propositional.ConsistentSaturatedHintikkaPair.imp_closed {φ : Formula ℕ} {L : Logic ℕ} {H : ConsistentSaturatedHintikkaPair L φ} [Entailment.VF L] {ψ χ : Formula ℕ} (hSψ : ψ ∈ φ.subformulas) (hSχ : χ ∈ φ.subformulas) : L ⊢ ψ ➝ χ → ⟨ψ, hSψ⟩ ∈ (↑H).1 → ⟨χ, hSχ⟩ ∈ (↑H).1

@[simp]

theorem LO.Propositional.ConsistentSaturatedHintikkaPair.no_bot {φ : Formula ℕ} {L : Logic ℕ} {H : ConsistentSaturatedHintikkaPair L φ} [Entailment.VF L] (h : ⊥ ∈ φ.subformulas) : ⟨⊥, h⟩ ∉ (↑H).1

@[simp]

theorem LO.Propositional.ConsistentSaturatedHintikkaPair.mem_top {φ : Formula ℕ} {L : Logic ℕ} {H : ConsistentSaturatedHintikkaPair L φ} [Entailment.VF L] (h : ⊤ ∈ φ.subformulas) : ⟨⊤, h⟩ ∈ (↑H).1

theorem LO.Propositional.ConsistentSaturatedHintikkaPair.iff_mem_and {φ : Formula ℕ} {L : Logic ℕ} {H : ConsistentSaturatedHintikkaPair L φ} [Entailment.VF L] {ψ χ : Formula ℕ} (hSub : ψ ⋏ χ ∈ φ.subformulas) : ⟨ψ ⋏ χ, hSub⟩ ∈ (↑H).1 ↔ ⟨ψ, ⋯⟩ ∈ (↑H).1 ∧ ⟨χ, ⋯⟩ ∈ (↑H).1

theorem LO.Propositional.ConsistentSaturatedHintikkaPair.iff_mem_or {φ : Formula ℕ} {L : Logic ℕ} {H : ConsistentSaturatedHintikkaPair L φ} [Entailment.VF L] {ψ χ : Formula ℕ} (hSub : ψ ⋎ χ ∈ φ.subformulas) : ⟨ψ ⋎ χ, hSub⟩ ∈ (↑H).1 ↔ ⟨ψ, ⋯⟩ ∈ (↑H).1 ∨ ⟨χ, ⋯⟩ ∈ (↑H).1

noncomputable def LO.Propositional.FMT.HintikkaModel (L : Logic ℕ) [Entailment.VF L] [Entailment.Consistent L] [Entailment.Disjunctive L] (φ : Formula ℕ) : Model

Equations

• One or more equations did not get rendered due to their size.

theorem LO.Propositional.FMT.HintikkaModel.truthlemma {L : Logic ℕ} [Entailment.VF L] [Entailment.Disjunctive L] [Entailment.Consistent L] {φ ψ : Formula ℕ} {H : (HintikkaModel L φ).World} (hsub : ψ ∈ φ.subformulas) : ⟨ψ, hsub⟩ ∈ (↑H).1 ↔ H ⊩ ψ

theorem LO.Propositional.FMT.provable_of_validOnHintikkaModel {L : Logic ℕ} [Entailment.VF L] [Entailment.Disjunctive L] [Entailment.Consistent L] {φ : Formula ℕ} : HintikkaModel L φ ⊧ φ → L ⊢ φ