Derivation2

Different characterizations of proof.

inductive LO.FirstOrder.Derivation2 {L : LO.FirstOrder.Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] (T : LO.FirstOrder.Theory L) : Finset (LO.FirstOrder.SyntacticFormula L) → Type u_1

• closed: {L : LO.FirstOrder.Language} → [inst : (k : ℕ) → DecidableEq (L.Func k)] → [inst_1 : (k : ℕ) → DecidableEq (L.Rel k)] → {T : LO.FirstOrder.Theory L} → (Δ : Finset (LO.FirstOrder.SyntacticFormula L)) → (p : LO.FirstOrder.SyntacticFormula L) → p ∈ Δ → ∼p ∈ Δ → LO.FirstOrder.Derivation2 T Δ
• root: {L : LO.FirstOrder.Language} → [inst : (k : ℕ) → DecidableEq (L.Func k)] → [inst_1 : (k : ℕ) → DecidableEq (L.Rel k)] → {T : LO.FirstOrder.Theory L} → {Δ : Finset (LO.FirstOrder.SyntacticFormula L)} → (p : LO.FirstOrder.SyntacticFormula L) → p ∈ T → p ∈ Δ → LO.FirstOrder.Derivation2 T Δ
• verum: {L : LO.FirstOrder.Language} → [inst : (k : ℕ) → DecidableEq (L.Func k)] → [inst_1 : (k : ℕ) → DecidableEq (L.Rel k)] → {T : LO.FirstOrder.Theory L} → {Δ : Finset (LO.FirstOrder.SyntacticFormula L)} → ⊤ ∈ Δ → LO.FirstOrder.Derivation2 T Δ
• and: {L : LO.FirstOrder.Language} → [inst : (k : ℕ) → DecidableEq (L.Func k)] → [inst_1 : (k : ℕ) → DecidableEq (L.Rel k)] → {T : LO.FirstOrder.Theory L} → {Δ : Finset (LO.FirstOrder.SyntacticFormula L)} → {p q : LO.FirstOrder.SyntacticFormula L} → p ⋏ q ∈ Δ → LO.FirstOrder.Derivation2 T (insert p Δ) → LO.FirstOrder.Derivation2 T (insert q Δ) → LO.FirstOrder.Derivation2 T Δ
• or: {L : LO.FirstOrder.Language} → [inst : (k : ℕ) → DecidableEq (L.Func k)] → [inst_1 : (k : ℕ) → DecidableEq (L.Rel k)] → {T : LO.FirstOrder.Theory L} → {Δ : Finset (LO.FirstOrder.SyntacticFormula L)} → {p q : LO.FirstOrder.SyntacticFormula L} → p ⋎ q ∈ Δ → LO.FirstOrder.Derivation2 T (insert p (insert q Δ)) → LO.FirstOrder.Derivation2 T Δ
• all: {L : LO.FirstOrder.Language} → [inst : (k : ℕ) → DecidableEq (L.Func k)] → [inst_1 : (k : ℕ) → DecidableEq (L.Rel k)] → {T : LO.FirstOrder.Theory L} → {Δ : Finset (LO.FirstOrder.SyntacticFormula L)} → {p : LO.FirstOrder.SyntacticSemiformula L 1} → ∀' p ∈ Δ → LO.FirstOrder.Derivation2 T (insert ((LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.free) p) (Finset.image (⇑(LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.shift)) Δ)) → LO.FirstOrder.Derivation2 T Δ
• ex: {L : LO.FirstOrder.Language} → [inst : (k : ℕ) → DecidableEq (L.Func k)] → [inst_1 : (k : ℕ) → DecidableEq (L.Rel k)] → {T : LO.FirstOrder.Theory L} → {Δ : Finset (LO.FirstOrder.SyntacticFormula L)} → {p : LO.FirstOrder.SyntacticSemiformula L 1} → ∃' p ∈ Δ → (t : LO.FirstOrder.SyntacticTerm L) → LO.FirstOrder.Derivation2 T (insert ((LO.FirstOrder.Rew.substs ![t]).hom p) Δ) → LO.FirstOrder.Derivation2 T Δ
• wk: {L : LO.FirstOrder.Language} → [inst : (k : ℕ) → DecidableEq (L.Func k)] → [inst_1 : (k : ℕ) → DecidableEq (L.Rel k)] → {T : LO.FirstOrder.Theory L} → {Δ Γ : Finset (LO.FirstOrder.SyntacticFormula L)} → LO.FirstOrder.Derivation2 T Δ → Δ ⊆ Γ → LO.FirstOrder.Derivation2 T Γ
• shift: {L : LO.FirstOrder.Language} → [inst : (k : ℕ) → DecidableEq (L.Func k)] → [inst_1 : (k : ℕ) → DecidableEq (L.Rel k)] → {T : LO.FirstOrder.Theory L} → {Δ : Finset (LO.FirstOrder.SyntacticFormula L)} → LO.FirstOrder.Derivation2 T Δ → LO.FirstOrder.Derivation2 T (Finset.image (⇑(LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.shift)) Δ)
• cut: {L : LO.FirstOrder.Language} → [inst : (k : ℕ) → DecidableEq (L.Func k)] → [inst_1 : (k : ℕ) → DecidableEq (L.Rel k)] → {T : LO.FirstOrder.Theory L} → {Δ : Finset (LO.FirstOrder.SyntacticFormula L)} → {p : LO.FirstOrder.SyntacticFormula L} → LO.FirstOrder.Derivation2 T (insert p Δ) → LO.FirstOrder.Derivation2 T (insert (∼p) Δ) → LO.FirstOrder.Derivation2 T Δ

def LO.FirstOrder.«term_⊢₃_» : Lean.TrailingParserDescr

Equations

• LO.FirstOrder.«term_⊢₃_» = Lean.ParserDescr.trailingNode `LO.FirstOrder.term_⊢₃_ 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊢₃ ") (Lean.ParserDescr.cat `term 46))

@[reducible, inline]

abbrev LO.FirstOrder.Derivable3 {L : LO.FirstOrder.Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] (T : LO.FirstOrder.Theory L) (Γ : Finset (LO.FirstOrder.SyntacticFormula L)) : Prop

Equations

• LO.FirstOrder.Derivable3 T Γ = Nonempty (LO.FirstOrder.Derivation2 T Γ)

def LO.FirstOrder.«term_⊢₃!_» : Lean.TrailingParserDescr

Equations

• LO.FirstOrder.«term_⊢₃!_» = Lean.ParserDescr.trailingNode `LO.FirstOrder.term_⊢₃!_ 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊢₃! ") (Lean.ParserDescr.cat `term 46))

@[reducible, inline]

abbrev LO.FirstOrder.Derivable3SingleConseq {L : LO.FirstOrder.Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] (T : LO.FirstOrder.Theory L) (p : LO.FirstOrder.SyntacticFormula L) : Prop

Equations

• LO.FirstOrder.Derivable3SingleConseq T p = LO.FirstOrder.Derivable3 T {p}

def LO.FirstOrder.«term_⊢₃.!_» : Lean.TrailingParserDescr

Equations

• LO.FirstOrder.«term_⊢₃.!_» = Lean.ParserDescr.trailingNode `LO.FirstOrder.term_⊢₃.!_ 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊢₃.! ") (Lean.ParserDescr.cat `term 46))

theorem LO.FirstOrder.shifts_toFinset_eq_image_shift {L : LO.FirstOrder.Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] (Δ : LO.FirstOrder.Sequent L) : (LO.FirstOrder.shifts Δ).toFinset = Finset.image (⇑(LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.shift)) (List.toFinset Δ)

def LO.FirstOrder.Derivation.toDerivation2 {L : LO.FirstOrder.Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] (T : LO.FirstOrder.Theory L) {Γ : LO.FirstOrder.Sequent L} : T ⟹ Γ → LO.FirstOrder.Derivation2 T (List.toFinset Γ)

noncomputable def LO.FirstOrder.Derivation2.toDerivation {L : LO.FirstOrder.Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] {T : LO.FirstOrder.Theory L} {Γ : Finset (LO.FirstOrder.SyntacticFormula L)} : LO.FirstOrder.Derivation2 T Γ → T ⟹ Γ.toList

theorem LO.FirstOrder.derivable_iff_derivable2 {L : LO.FirstOrder.Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] {T : LO.FirstOrder.Theory L} {Γ : List (LO.FirstOrder.SyntacticFormula L)} : T ⟹! Γ ↔ LO.FirstOrder.Derivable3 T Γ.toFinset

def LO.FirstOrder.provable_iff_derivable2 {L : LO.FirstOrder.Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] {T : LO.FirstOrder.Theory L} {p : LO.FirstOrder.SyntacticFormula L} : T ⊢! p ↔ LO.FirstOrder.Derivable3SingleConseq T p

Equations

• ⋯ = ⋯