@[simp]

theorem LO.Propositional.NNFormula.ne_neg {α : Type u_1} (φ : NNFormula α) : ∼φ ≠ φ

inductive LO.Propositional.NNFormula.IsAtomic {α : Type u_1} : NNFormula α → Prop

• atom {α : Type u_1} (a : α) : (NNFormula.atom a).IsAtomic
• natom {α : Type u_1} (a : α) : (NNFormula.natom a).IsAtomic

@[simp]

theorem LO.Propositional.NNFormula.IsAtomic.not_cons_verum {α : Type u_1} : ¬⊤.IsAtomic

@[simp]

theorem LO.Propositional.NNFormula.IsAtomic.not_cons_falsum {α : Type u_1} : ¬⊥.IsAtomic

@[simp]

theorem LO.Propositional.NNFormula.IsAtomic.not_cons_and {α : Type u_1} {φ ψ : NNFormula α} : ¬(φ ⋏ ψ).IsAtomic

@[simp]

theorem LO.Propositional.NNFormula.IsAtomic.not_cons_or {α : Type u_1} {φ ψ : NNFormula α} : ¬(φ ⋎ ψ).IsAtomic

instance LO.Propositional.NNFormula.instDecidablePredIsAtomic {α : Type u_1} : DecidablePred IsAtomic

Equations

• (LO.Propositional.NNFormula.atom a).instDecidablePredIsAtomic = isTrue ⋯
• (LO.Propositional.NNFormula.natom a).instDecidablePredIsAtomic = isTrue ⋯
• LO.Propositional.NNFormula.verum.instDecidablePredIsAtomic = isFalse ⋯
• LO.Propositional.NNFormula.falsum.instDecidablePredIsAtomic = isFalse ⋯
• (a.and a_1).instDecidablePredIsAtomic = isFalse ⋯
• (a.or a_1).instDecidablePredIsAtomic = isFalse ⋯

def LO.Propositional.NNFormula.weight {α : Type u_1} : NNFormula α → ℕ

Equations

• (LO.Propositional.NNFormula.atom a).weight = 0
• (LO.Propositional.NNFormula.natom a).weight = 0
• LO.Propositional.NNFormula.verum.weight = 1
• LO.Propositional.NNFormula.falsum.weight = 1
• (a.and a_1).weight = a.weight + a_1.weight + 1
• (a.or a_1).weight = a.weight + a_1.weight + 1

@[simp]

theorem LO.Propositional.NNFormula.weight_atom {α : Type u_1} (a : α) : (atom a).complexity = 0

@[simp]

theorem LO.Propositional.NNFormula.weight_natom {α : Type u_1} (a : α) : (natom a).complexity = 0

@[simp]

theorem LO.Propositional.NNFormula.weight_verum {α : Type u_1} : ⊤.weight = 1

@[simp]

theorem LO.Propositional.NNFormula.weight_falsum {α : Type u_1} : ⊥.weight = 1

@[simp]

theorem LO.Propositional.NNFormula.weight_and {α : Type u_1} (φ ψ : NNFormula α) : (φ ⋏ ψ).weight = φ.weight + ψ.weight + 1

@[simp]

theorem LO.Propositional.NNFormula.weight_or {α : Type u_1} (φ ψ : NNFormula α) : (φ ⋎ ψ).weight = φ.weight + ψ.weight + 1

def LO.Propositional.Sequent.weight {α : Type u_1} (Γ : Sequent α) : ℕ

Equations

• Γ.weight = (List.map LO.Propositional.NNFormula.weight Γ).sum

@[simp]

theorem LO.Propositional.Sequent.weight_nil {α : Type u_1} : weight [] = 0

@[simp]

theorem LO.Propositional.Sequent.weight_cons {α : Type u_1} (φ : NNFormula α) (Γ : Sequent α) : weight (φ :: Γ) = φ.weight + Γ.weight

@[simp]

theorem LO.Propositional.Sequent.weight_append {α : Type u_1} (Γ Δ : Sequent α) : (Γ ++ Δ).weight = Γ.weight + Δ.weight

theorem LO.Propositional.Sequent.weight_le_weight_of_mem {α : Type u_1} {φ : NNFormula α} {Γ : Sequent α} (h : φ ∈ Γ) : φ.weight ≤ Γ.weight

theorem LO.Propositional.Sequent.weight_remove {α : Type u_1} [DecidableEq α] (Γ : Sequent α) (φ : NNFormula α) : weight (List.remove φ Γ) = Γ.weight - List.count φ Γ * φ.weight

theorem LO.Propositional.Sequent.weight_remove_le_of_mem {α : Type u_1} [DecidableEq α] {φ : NNFormula α} {Γ : Sequent α} (h : φ ∈ Γ) : weight (List.remove φ Γ) ≤ Γ.weight - φ.weight

def LO.Propositional.Sequent.IsAtomic {α : Type u_1} (Γ : Sequent α) : Prop

Equations

• Γ.IsAtomic = ∀ φ ∈ Γ, φ.IsAtomic

@[simp]

theorem LO.Propositional.Sequent.IsAtomic.nil {α : Type u_1} : IsAtomic []

instance LO.Propositional.Sequent.instDecidablePredIsAtomic {α : Type u_1} : DecidablePred IsAtomic

Equations

• LO.Propositional.Sequent.instDecidablePredIsAtomic = List.decidableBAll LO.Propositional.NNFormula.IsAtomic

@[simp]

theorem LO.Propositional.Sequent.IsAtomic.cons_atom_iff {α : Type u_1} {Γ : Sequent α} {φ : NNFormula α} : IsAtomic (φ :: Γ) ↔ φ.IsAtomic ∧ Γ.IsAtomic

def LO.Propositional.Sequent.chooseNonAtomic {α : Type u_1} (Γ : Sequent α) (H : ¬Γ.IsAtomic) : NNFormula α

Equations

• Γ.chooseNonAtomic H = List.choose (fun (φ : LO.Propositional.NNFormula α) => ¬φ.IsAtomic) Γ ⋯

@[simp]

theorem LO.Propositional.Sequent.chooseNonAtomic_mem {α : Type u_1} {Γ : Sequent α} (h : ¬Γ.IsAtomic) : Γ.chooseNonAtomic h ∈ Γ

@[simp]

theorem LO.Propositional.Sequent.chooseNonAtomic_property {α : Type u_1} (Γ : Sequent α) (h : ¬Γ.IsAtomic) : ¬(Γ.chooseNonAtomic h).IsAtomic

@[reducible, inline]

abbrev LO.Propositional.Sequents (α : Type u_2) : Type u_2

Equations

• LO.Propositional.Sequents α = List (LO.Propositional.Sequent α)

def LO.Propositional.Sequents.weight {α : Type u_1} (S : Sequents α) : ℕ

Equations

• S.weight = Option.casesOn (List.map LO.Propositional.Sequent.weight S).max? 0 Nat.succ

@[simp]

theorem LO.Propositional.Sequents.weight_nil {α : Type u_1} : weight [] = 0

@[simp]

theorem LO.Propositional.Sequents.weight_eq_zero_iff_eq_nil {α : Type u_1} {S : Sequents α} : S.weight = 0 ↔ S = []

theorem LO.Propositional.Sequents.weight_eq_succ_iff {α : Type u_1} {n : ℕ} {S : Sequents α} : S.weight = n + 1 ↔ ∃ Γ ∈ S, Γ.weight = n ∧ ∀ Δ ∈ S, Δ.weight ≤ n

theorem LO.Propositional.Sequents.weight_eq_of_mem_max {α : Type u_1} {S : Sequents α} {m : ℕ} (hm : m ∈ (List.map Sequent.weight S).max?) : S.weight = m + 1

theorem LO.Propositional.Sequents.weight_lt_weight_of {α : Type u_1} {S₁ S₂ : Sequents α} {Γ : Sequent α} (hΓ : Γ ∈ S₂) (h : ∀ Δ ∈ S₁, Δ.weight < Γ.weight) : S₁.weight < S₂.weight

@[reducible, inline]

abbrev LO.Propositional.Derivations {α : Type u_1} (T : Theory α) (S : Sequents α) : Type u_1

Equations

• LO.Propositional.Derivations T S = ((Γ : LO.Propositional.Sequent α) → Γ ∈ S → T ⟹ Γ)

@[reducible, inline]

abbrev LO.Propositional.Derivations! {α : Type u_1} (T : Theory α) (S : Sequents α) : Prop

Equations

• LO.Propositional.Derivations! T S = ∀ Γ ∈ S, T ⟹! Γ

def LO.Propositional.Derivations.ofSubset {α : Type u_1} {T : Theory α} {S₁ S₂ : Sequents α} (ss : S₁ ⊆ S₂) : Derivations T S₂ → Derivations T S₁

Equations

• LO.Propositional.Derivations.ofSubset ss d Γ hΓ = d Γ ⋯

def LO.Propositional.Derivations.nil {α : Type u_1} {T : Theory α} : Derivations T []

Equations

• LO.Propositional.Derivations.nil x✝ h = ⋯.elim

@[simp]

theorem LO.Propositional.Derivations!.nil {α✝ : Type u_2} {T : Theory α✝} : Derivations! T []

def LO.Propositional.Sequent.IsClosed {α : Type u_1} (Γ : Sequent α) : Prop

Equations

• Γ.IsClosed = ∃ φ ∈ Γ, ∼φ ∈ Γ

theorem LO.Propositional.Sequent.IsClosed.cons_iff {α : Type u_1} {φ : NNFormula α} {Γ : Sequent α} : IsClosed (φ :: Γ) ↔ ∼φ ∈ Γ ∨ Γ.IsClosed

instance LO.Propositional.instDecidablePredSequentIsClosedOfDecidableEq {α : Type u_1} [DecidableEq α] : DecidablePred Sequent.IsClosed

Equations

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

def LO.Propositional.Sequent.IsClosed.choose {α : Type u_1} [DecidableEq α] (Γ : Sequent α) : Γ.IsClosed → { φ : NNFormula α // φ ∈ Γ ∧ ∼φ ∈ Γ }

Equations

• LO.Propositional.Sequent.IsClosed.choose [] h = ⋯.elim
• LO.Propositional.Sequent.IsClosed.choose (φ :: Γ) h = if hn : ∼φ ∈ Γ then ⟨φ, ⋯⟩ else have this := ⋯; match LO.Propositional.Sequent.IsClosed.choose Γ this with | ⟨ψ, hψ⟩ => ⟨ψ, ⋯⟩

def LO.Propositional.Derivation.ofIsClosed {α : Type u_1} [DecidableEq α] {T : Theory α} {Γ : Sequent α} (h : Γ.IsClosed) : T ⟹ Γ

Equations

• LO.Propositional.Derivation.ofIsClosed h = match LO.Propositional.Sequent.IsClosed.choose Γ h with | ⟨φ, ⋯⟩ => LO.Propositional.Derivation.em h hn

@[reducible, inline]

abbrev LO.Propositional.Sequent.IsOpen {α : Type u_1} (Γ : Sequent α) : Prop

Equations

• Γ.IsOpen = (Γ.IsAtomic ∧ ¬Γ.IsClosed)

instance LO.Propositional.instDecidablePredSequentIsOpenOfDecidableEq {α : Type u_1} [DecidableEq α] : DecidablePred Sequent.IsOpen

Equations

• LO.Propositional.instDecidablePredSequentIsOpenOfDecidableEq = inferInstance

theorem LO.Propositional.Sequent.IsOpen.not_tautology {α : Type u_1} {Γ : Sequent α} (h : Γ.IsOpen) : ¬Γ.IsTautology

def LO.Propositional.Sequents.IsClosed {α : Type u_1} (S : Sequents α) : Prop

Equations

• S.IsClosed = ∀ Γ ∈ S, Γ.IsClosed

instance LO.Propositional.instDecidablePredSequentsIsClosedOfDecidableEq {α : Type u_1} [DecidableEq α] : DecidablePred Sequents.IsClosed

Equations

• LO.Propositional.instDecidablePredSequentsIsClosedOfDecidableEq = List.decidableBAll LO.Propositional.Sequent.IsClosed

def LO.Propositional.Sequent.reduction {α : Type u_1} [DecidableEq α] {Γ : Sequent α} (h : ¬Γ.IsAtomic) : Sequents α

Equations

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

theorem LO.Propositional.Sequent.reduction_verum {α : Type u_1} {Γ : Sequent α} [DecidableEq α] {h : ¬Γ.IsAtomic} (H : Γ.chooseNonAtomic h = ⊤) : reduction h = []

theorem LO.Propositional.Sequent.reduction_falsum {α : Type u_1} {Γ : Sequent α} [DecidableEq α] {h : ¬Γ.IsAtomic} (H : Γ.chooseNonAtomic h = ⊥) : reduction h = [List.remove ⊥ Γ]

theorem LO.Propositional.Sequent.reduction_and {α : Type u_1} {Γ : Sequent α} [DecidableEq α] {φ ψ : NNFormula α} {h : ¬Γ.IsAtomic} (H : Γ.chooseNonAtomic h = φ ⋏ ψ) : reduction h = [(List.remove (φ ⋏ ψ) Γ).concat φ, (List.remove (φ ⋏ ψ) Γ).concat ψ]

theorem LO.Propositional.Sequent.reduction_or {α : Type u_1} {Γ : Sequent α} [DecidableEq α] {φ ψ : NNFormula α} {h : ¬Γ.IsAtomic} (H : Γ.chooseNonAtomic h = φ ⋎ ψ) : reduction h = [((List.remove (φ ⋎ ψ) Γ).concat φ).concat ψ]

theorem LO.Propositional.Sequent.weight_lt_weight_of_mem_reduction {α : Type u_1} {Γ Δ : Sequent α} [DecidableEq α] {h : ¬Γ.IsAtomic} : Δ ∈ reduction h → Δ.weight < Γ.weight

def LO.Propositional.Derivation.ofReduction {α : Type u_1} [DecidableEq α] {T : Theory α} {Γ : Sequent α} {hΓ : ¬Γ.IsAtomic} (d : Derivations T (Sequent.reduction hΓ)) : T ⟹ Γ

Equations

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

theorem LO.Propositional.Derivation.toReduction {α : Type u_1} [DecidableEq α] {T : Theory α} {Γ : Sequent α} (hΓ : ¬Γ.IsAtomic) (d : T ⟹! Γ) : Derivations! T (Sequent.reduction hΓ)

@[reducible, inline]

abbrev LO.Propositional.Sequents.Refuted {α : Type u_1} (S : Sequents α) : Prop

Equations

• S.Refuted = ∃ Γ ∈ S, Γ.IsOpen

theorem LO.Propositional.Sequents.Refuted.not_iff {α : Type u_1} {S : Sequents α} : ¬S.Refuted ↔ ∀ Γ ∈ S, Γ.IsAtomic → Γ.IsClosed

instance LO.Propositional.instDecidablePredSequentsRefutedOfDecidableEq {α : Type u_1} [DecidableEq α] : DecidablePred Sequents.Refuted

Equations

• LO.Propositional.instDecidablePredSequentsRefutedOfDecidableEq = List.decidableBEx LO.Propositional.Sequent.IsOpen

def LO.Propositional.Sequents.reduction {α : Type u_1} [DecidableEq α] (S : Sequents α) : Sequents α

Equations

• S.reduction = List.flatMap (fun (Γ : LO.Propositional.Sequent α) => if h : Γ.IsAtomic then [] else LO.Propositional.Sequent.reduction h) S

theorem LO.Propositional.Sequent.reduction_sublist {α : Type u_1} [DecidableEq α] {Γ : Sequent α} (hΓ : ¬Γ.IsAtomic) {S : Sequents α} (h : Γ ∈ S) : List.Sublist (reduction hΓ) S.reduction

def LO.Propositional.Derivations.ofReduction {α : Type u_1} {T : Theory α} [DecidableEq α] {S : Sequents α} (hS : ¬S.Refuted) (d : Derivations T S.reduction) : Derivations T S

Equations

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

theorem LO.Propositional.Derivations.toReduction {α : Type u_1} {T : Theory α} [DecidableEq α] {S : Sequents α} (d : Derivations! T S) : Derivations! T S.reduction

theorem LO.Propositional.Sequents.reduction_weight_lt_weight {α : Type u_1} [DecidableEq α] (S : Sequents α) (h : S ≠ []) : S.reduction.weight < S.weight

inductive LO.Propositional.Derivations.Dec {α : Type u_1} : Sequents α → Type u_1

• provable {α : Type u_1} {S : Sequents α} : Derivations ∅ S → Dec S
• unprovable {α : Type u_1} {S : Sequents α} (Γ : Sequent α) : Γ ∈ S → ¬Γ.IsTautology → Dec S

def LO.Propositional.Derivations.Dec.ofReduction {α : Type u_1} [DecidableEq α] {S : Sequents α} (hS : ¬S.Refuted) : Dec S.reduction → Dec S

Equations

• One or more equations did not get rendered due to their size.
• LO.Propositional.Derivations.Dec.ofReduction hS (LO.Propositional.Derivations.Dec.provable d) = LO.Propositional.Derivations.Dec.provable (LO.Propositional.Derivations.ofReduction hS d)

@[irreducible]

def LO.Propositional.Sequents.dec {α : Type u_1} [DecidableEq α] (S : Sequents α) : Derivations.Dec S

Equations

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

instance LO.Propositional.instDecidablePredSequentIsTautologyOfDecidableEq {α : Type u_1} [DecidableEq α] : DecidablePred fun (Γ : Sequent α) => Γ.IsTautology

Equations

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

instance LO.Propositional.instDecidablePredNNFormulaIsTautologyOfDecidableEq {α : Type u_1} [DecidableEq α] : DecidablePred fun (φ : NNFormula α) => φ.IsTautology

Equations

• LO.Propositional.instDecidablePredNNFormulaIsTautologyOfDecidableEq x✝ = inferInstance