inductive
LO.FirstOrder.Derivation3
{L : LO.FirstOrder.Language}
[(k : ℕ) → DecidableEq (L.Func k)]
[(k : ℕ) → DecidableEq (L.Rel k)]
(T : LO.FirstOrder.SyntacticTheory 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.SyntacticTheory L} → (Δ : Finset (LO.FirstOrder.SyntacticFormula L)) → (p : LO.FirstOrder.SyntacticFormula L) → p ∈ Δ → ~p ∈ Δ → LO.FirstOrder.Derivation3 T Δ
- root: {L : LO.FirstOrder.Language} → [inst : (k : ℕ) → DecidableEq (L.Func k)] → [inst_1 : (k : ℕ) → DecidableEq (L.Rel k)] → {T : LO.FirstOrder.SyntacticTheory L} → {Δ : Finset (LO.FirstOrder.SyntacticFormula L)} → (p : LO.FirstOrder.SyntacticFormula L) → p ∈ T → p ∈ Δ → LO.FirstOrder.Derivation3 T Δ
- verum: {L : LO.FirstOrder.Language} → [inst : (k : ℕ) → DecidableEq (L.Func k)] → [inst_1 : (k : ℕ) → DecidableEq (L.Rel k)] → {T : LO.FirstOrder.SyntacticTheory L} → {Δ : Finset (LO.FirstOrder.SyntacticFormula L)} → ⊤ ∈ Δ → LO.FirstOrder.Derivation3 T Δ
- and: {L : LO.FirstOrder.Language} → [inst : (k : ℕ) → DecidableEq (L.Func k)] → [inst_1 : (k : ℕ) → DecidableEq (L.Rel k)] → {T : LO.FirstOrder.SyntacticTheory L} → {Δ : Finset (LO.FirstOrder.SyntacticFormula L)} → {p q : LO.FirstOrder.SyntacticFormula L} → p ⋏ q ∈ Δ → LO.FirstOrder.Derivation3 T (insert p Δ) → LO.FirstOrder.Derivation3 T (insert q Δ) → LO.FirstOrder.Derivation3 T Δ
- or: {L : LO.FirstOrder.Language} → [inst : (k : ℕ) → DecidableEq (L.Func k)] → [inst_1 : (k : ℕ) → DecidableEq (L.Rel k)] → {T : LO.FirstOrder.SyntacticTheory L} → {Δ : Finset (LO.FirstOrder.SyntacticFormula L)} → {p q : LO.FirstOrder.SyntacticFormula L} → p ⋎ q ∈ Δ → LO.FirstOrder.Derivation3 T (insert p (insert q Δ)) → LO.FirstOrder.Derivation3 T Δ
- all: {L : LO.FirstOrder.Language} → [inst : (k : ℕ) → DecidableEq (L.Func k)] → [inst_1 : (k : ℕ) → DecidableEq (L.Rel k)] → {T : LO.FirstOrder.SyntacticTheory L} → {Δ : Finset (LO.FirstOrder.SyntacticFormula L)} → {p : LO.FirstOrder.SyntacticSemiformula L 1} → ∀' p ∈ Δ → LO.FirstOrder.Derivation3 T (insert ((LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.free) p) (Finset.image (⇑(LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.shift)) Δ)) → LO.FirstOrder.Derivation3 T Δ
- ex: {L : LO.FirstOrder.Language} → [inst : (k : ℕ) → DecidableEq (L.Func k)] → [inst_1 : (k : ℕ) → DecidableEq (L.Rel k)] → {T : LO.FirstOrder.SyntacticTheory L} → {Δ : Finset (LO.FirstOrder.SyntacticFormula L)} → {p : LO.FirstOrder.SyntacticSemiformula L 1} → ∃' p ∈ Δ → (t : LO.FirstOrder.SyntacticTerm L) → LO.FirstOrder.Derivation3 T (insert ((LO.FirstOrder.Rew.substs ![t]).hom p) Δ) → LO.FirstOrder.Derivation3 T Δ
- wk: {L : LO.FirstOrder.Language} → [inst : (k : ℕ) → DecidableEq (L.Func k)] → [inst_1 : (k : ℕ) → DecidableEq (L.Rel k)] → {T : LO.FirstOrder.SyntacticTheory L} → {Δ Γ : Finset (LO.FirstOrder.SyntacticFormula L)} → LO.FirstOrder.Derivation3 T Δ → Δ ⊆ Γ → LO.FirstOrder.Derivation3 T Γ
- shift: {L : LO.FirstOrder.Language} → [inst : (k : ℕ) → DecidableEq (L.Func k)] → [inst_1 : (k : ℕ) → DecidableEq (L.Rel k)] → {T : LO.FirstOrder.SyntacticTheory L} → {Δ : Finset (LO.FirstOrder.SyntacticFormula L)} → LO.FirstOrder.Derivation3 T Δ → LO.FirstOrder.Derivation3 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.SyntacticTheory L} → {Δ : Finset (LO.FirstOrder.SyntacticFormula L)} → {p : LO.FirstOrder.SyntacticFormula L} → LO.FirstOrder.Derivation3 T (insert p Δ) → LO.FirstOrder.Derivation3 T (insert (~p) Δ) → LO.FirstOrder.Derivation3 T Δ
Instances For
Equations
- LO.FirstOrder.«term_⊢₃_» = Lean.ParserDescr.trailingNode `LO.FirstOrder.term_⊢₃_ 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊢₃ ") (Lean.ParserDescr.cat `term 46))
Instances For
@[reducible, inline]
abbrev
LO.FirstOrder.Derivable3
{L : LO.FirstOrder.Language}
[(k : ℕ) → DecidableEq (L.Func k)]
[(k : ℕ) → DecidableEq (L.Rel k)]
(T : LO.FirstOrder.SyntacticTheory L)
(Γ : Finset (LO.FirstOrder.SyntacticFormula L))
:
Equations
Instances For
Equations
- LO.FirstOrder.«term_⊢₃!_» = Lean.ParserDescr.trailingNode `LO.FirstOrder.term_⊢₃!_ 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊢₃! ") (Lean.ParserDescr.cat `term 46))
Instances For
@[reducible, inline]
abbrev
LO.FirstOrder.Derivable3SingleConseq
{L : LO.FirstOrder.Language}
[(k : ℕ) → DecidableEq (L.Func k)]
[(k : ℕ) → DecidableEq (L.Rel k)]
(T : LO.FirstOrder.SyntacticTheory L)
(p : LO.FirstOrder.SyntacticFormula L)
:
Equations
Instances For
Equations
- LO.FirstOrder.«term_⊢₃.!_» = Lean.ParserDescr.trailingNode `LO.FirstOrder.term_⊢₃.!_ 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊢₃.! ") (Lean.ParserDescr.cat `term 46))
Instances For
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.Derivation2.toDerivation3
{L : LO.FirstOrder.Language}
[(k : ℕ) → DecidableEq (L.Func k)]
[(k : ℕ) → DecidableEq (L.Rel k)]
(T : LO.FirstOrder.SyntacticTheory L)
{Γ : LO.FirstOrder.Sequent L}
:
Equations
- One or more equations did not get rendered due to their size.
- LO.FirstOrder.Derivation2.toDerivation3 T (LO.FirstOrder.Derivation2.closed Δ p) = LO.FirstOrder.Derivation3.closed (p :: ~p :: Δ).toFinset p ⋯ ⋯
- LO.FirstOrder.Derivation2.toDerivation3 T (LO.FirstOrder.Derivation2.root Γ p h) = LO.FirstOrder.Derivation3.root p h ⋯
- LO.FirstOrder.Derivation2.toDerivation3 T (LO.FirstOrder.Derivation2.verum Δ) = LO.FirstOrder.Derivation3.verum ⋯
- LO.FirstOrder.Derivation2.toDerivation3 T dpq.or = LO.FirstOrder.Derivation3.or ⋯ ((LO.FirstOrder.Derivation2.toDerivation3 T dpq).wk ⋯)
- LO.FirstOrder.Derivation2.toDerivation3 T dp.all = LO.FirstOrder.Derivation3.all ⋯ ((LO.FirstOrder.Derivation2.toDerivation3 T dp).wk ⋯)
- LO.FirstOrder.Derivation2.toDerivation3 T (LO.FirstOrder.Derivation2.ex t dp) = LO.FirstOrder.Derivation3.ex ⋯ t ((LO.FirstOrder.Derivation2.toDerivation3 T dp).wk ⋯)
- LO.FirstOrder.Derivation2.toDerivation3 T (d.wk h) = (LO.FirstOrder.Derivation2.toDerivation3 T d).wk ⋯
- LO.FirstOrder.Derivation2.toDerivation3 T (d₁.cut d₂) = ((LO.FirstOrder.Derivation2.toDerivation3 T d₁).wk ⋯).cut ((LO.FirstOrder.Derivation2.toDerivation3 T d₂).wk ⋯)
Instances For
noncomputable def
LO.FirstOrder.Derivation3.toDerivation2
{L : LO.FirstOrder.Language}
[(k : ℕ) → DecidableEq (L.Func k)]
[(k : ℕ) → DecidableEq (L.Rel k)]
[L.ConstantInhabited]
{T : LO.FirstOrder.SyntacticTheory L}
{Γ : Finset (LO.FirstOrder.SyntacticFormula L)}
:
LO.FirstOrder.Derivation3 T Γ → LO.FirstOrder.Derivation2 T Γ.toList
Instances For
theorem
LO.FirstOrder.derivable2_iff_derivable3
{L : LO.FirstOrder.Language}
[(k : ℕ) → DecidableEq (L.Func k)]
[(k : ℕ) → DecidableEq (L.Rel k)]
[L.ConstantInhabited]
{T : LO.FirstOrder.SyntacticTheory L}
{Γ : List (LO.FirstOrder.SyntacticFormula L)}
:
LO.FirstOrder.Derivable2 T Γ ↔ LO.FirstOrder.Derivable3 T Γ.toFinset
def
LO.FirstOrder.provable_iff_derivable3
{L : LO.FirstOrder.Language}
[(k : ℕ) → DecidableEq (L.Func k)]
[(k : ℕ) → DecidableEq (L.Rel k)]
[L.ConstantInhabited]
{T : LO.FirstOrder.SyntacticTheory L}
{σ : LO.FirstOrder.Sentence L}
:
T.close ⊢! σ ↔ LO.FirstOrder.Derivable3SingleConseq T (LO.FirstOrder.Rew.embs.hom σ)
Equations
- ⋯ = ⋯
Instances For
def
LO.FirstOrder.provable_iff_derivable3'
{L : LO.FirstOrder.Language}
[(k : ℕ) → DecidableEq (L.Func k)]
[(k : ℕ) → DecidableEq (L.Rel k)]
[L.ConstantInhabited]
{T : LO.FirstOrder.Theory L}
{σ : LO.FirstOrder.Sentence L}
:
T ⊢! σ ↔ LO.FirstOrder.Derivable3SingleConseq (⇑LO.FirstOrder.Rew.embs.hom '' T) (LO.FirstOrder.Rew.embs.hom σ)
Equations
- ⋯ = ⋯