inductive LO.FirstOrder.Derivation.Code (L : LO.FirstOrder.Language) : Type u

• axL: {L : LO.FirstOrder.Language} → {k : ℕ} → L.Rel k → (Fin k → LO.FirstOrder.SyntacticTerm L) → LO.FirstOrder.Derivation.Code L
• verum: {L : LO.FirstOrder.Language} → LO.FirstOrder.Derivation.Code L
• and: {L : LO.FirstOrder.Language} → LO.FirstOrder.SyntacticFormula L → LO.FirstOrder.SyntacticFormula L → LO.FirstOrder.Derivation.Code L
• or: {L : LO.FirstOrder.Language} → LO.FirstOrder.SyntacticFormula L → LO.FirstOrder.SyntacticFormula L → LO.FirstOrder.Derivation.Code L
• all: {L : LO.FirstOrder.Language} → LO.FirstOrder.SyntacticSemiformula L 1 → LO.FirstOrder.Derivation.Code L
• ex: {L : LO.FirstOrder.Language} → LO.FirstOrder.SyntacticSemiformula L 1 → LO.FirstOrder.SyntacticTerm L → LO.FirstOrder.Derivation.Code L
• wk: {L : LO.FirstOrder.Language} → List (LO.FirstOrder.SyntacticFormula L) → LO.FirstOrder.Derivation.Code L

def LO.FirstOrder.Derivation.Code.equiv (L : LO.FirstOrder.Language) : LO.FirstOrder.Derivation.Code L ≃ (k : ℕ) × L.Rel k × (Fin k → LO.FirstOrder.SyntacticTerm L) ⊕ Unit ⊕ LO.FirstOrder.SyntacticFormula L × LO.FirstOrder.SyntacticFormula L ⊕ LO.FirstOrder.SyntacticFormula L × LO.FirstOrder.SyntacticFormula L ⊕ LO.FirstOrder.SyntacticSemiformula L 1 ⊕ LO.FirstOrder.SyntacticSemiformula L 1 × LO.FirstOrder.SyntacticTerm L ⊕ List (LO.FirstOrder.SyntacticFormula L)

Equations

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

instance LO.FirstOrder.Derivation.instPrimcodableCode {L : LO.FirstOrder.Language} [(k : ℕ) → Primcodable (L.Func k)] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Func] [UniformlyPrimcodable L.Rel] : Primcodable (LO.FirstOrder.Derivation.Code L)

Equations

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

@[reducible, inline]

abbrev LO.FirstOrder.Derivation.ProofList (L : LO.FirstOrder.Language) : Type u

Equations

• LO.FirstOrder.Derivation.ProofList L = List (LO.FirstOrder.Derivation.Code L × List (LO.FirstOrder.SyntacticFormula L))

def LO.FirstOrder.Derivation.ProofList.sequents {L : LO.FirstOrder.Language} : LO.FirstOrder.Derivation.ProofList L → List (List (LO.FirstOrder.SyntacticFormula L))

Equations

• LO.FirstOrder.Derivation.ProofList.sequents = List.map Prod.snd

def LO.FirstOrder.Derivation.ProofList.isProper {L : LO.FirstOrder.Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] : LO.FirstOrder.Derivation.ProofList L → Bool

Equations

• One or more equations did not get rendered due to their size.
• LO.FirstOrder.Derivation.ProofList.isProper [] = true
• LO.FirstOrder.Derivation.ProofList.isProper ((LO.FirstOrder.Derivation.Code.verum, Γ) :: l) = (LO.FirstOrder.Derivation.ProofList.isProper l && decide (⊤ ∈ Γ))

instance LO.FirstOrder.Derivation.ProofList.instPrimcodableProdListSyntacticFormulaCodeSumUnitSyntacticSemiformulaOfNatNatSyntacticTerm {L : LO.FirstOrder.Language} [(k : ℕ) → Primcodable (L.Func k)] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Func] [UniformlyPrimcodable L.Rel] : Primcodable ((((List (LO.FirstOrder.SyntacticFormula L) × List (List (LO.FirstOrder.SyntacticFormula L))) × LO.FirstOrder.Derivation.Code L) × (Unit ⊕ LO.FirstOrder.SyntacticFormula L × LO.FirstOrder.SyntacticFormula L ⊕ LO.FirstOrder.SyntacticFormula L × LO.FirstOrder.SyntacticFormula L ⊕ LO.FirstOrder.SyntacticSemiformula L 1 ⊕ LO.FirstOrder.SyntacticSemiformula L 1 × LO.FirstOrder.SyntacticTerm L ⊕ List (LO.FirstOrder.SyntacticFormula L))) × (LO.FirstOrder.SyntacticFormula L × LO.FirstOrder.SyntacticFormula L ⊕ LO.FirstOrder.SyntacticFormula L × LO.FirstOrder.SyntacticFormula L ⊕ LO.FirstOrder.SyntacticSemiformula L 1 ⊕ LO.FirstOrder.SyntacticSemiformula L 1 × LO.FirstOrder.SyntacticTerm L ⊕ List (LO.FirstOrder.SyntacticFormula L)))

Equations

• LO.FirstOrder.Derivation.ProofList.instPrimcodableProdListSyntacticFormulaCodeSumUnitSyntacticSemiformulaOfNatNatSyntacticTerm = Primcodable.prod

theorem LO.FirstOrder.Derivation.ProofList.isProper_primrec {L : LO.FirstOrder.Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Primcodable (L.Func k)] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Func] [UniformlyPrimcodable L.Rel] : Primrec LO.FirstOrder.Derivation.ProofList.isProper

@[simp]

theorem LO.FirstOrder.Derivation.ProofList.sequents_append {L : LO.FirstOrder.Language} {l₁ : LO.FirstOrder.Derivation.ProofList L} {l₂ : LO.FirstOrder.Derivation.ProofList L} : (l₁ ++ l₂).sequents = l₁.sequents ++ l₂.sequents

theorem LO.FirstOrder.Derivation.ProofList.isProper_append {L : LO.FirstOrder.Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] {l₁ : LO.FirstOrder.Derivation.ProofList L} {l₂ : LO.FirstOrder.Derivation.ProofList L} (h₁ : l₁.isProper = true) (h₂ : l₂.isProper = true) : (l₁ ++ l₂).isProper = true

theorem LO.FirstOrder.Derivation.ProofList.derivation_of_isProper {L : LO.FirstOrder.Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] (l : LO.FirstOrder.Derivation.ProofList L) : l.isProper = true → ∀ Γ ∈ l.sequents, Nonempty (⊢¹ Γ)

@[irreducible]

noncomputable def LO.FirstOrder.Derivation.ProofList.ofDerivation {L : LO.FirstOrder.Language} {Γ : LO.FirstOrder.Sequent L} : { d : ⊢¹ Γ // LO.FirstOrder.Derivation.CutFree d } → LO.FirstOrder.Derivation.ProofList L

Equations

• One or more equations did not get rendered due to their size.
• LO.FirstOrder.Derivation.ProofList.ofDerivation ⟨LO.FirstOrder.Derivation.verum Γ, property⟩ = [(LO.FirstOrder.Derivation.Code.verum, ⊤ :: Γ)]
• LO.FirstOrder.Derivation.ProofList.ofDerivation ⟨b.wk a, H⟩ = (LO.FirstOrder.Derivation.Code.wk Γ, x) :: LO.FirstOrder.Derivation.ProofList.ofDerivation ⟨b, ⋯⟩

theorem LO.FirstOrder.Derivation.ProofList.mem_ofDerivation {L : LO.FirstOrder.Language} {Γ : LO.FirstOrder.Sequent L} (b : { d : ⊢¹ Γ // LO.FirstOrder.Derivation.CutFree d }) : Γ ∈ (LO.FirstOrder.Derivation.ProofList.ofDerivation b).sequents

theorem LO.FirstOrder.Derivation.ProofList.iff_mem_sequents {L : LO.FirstOrder.Language} {Γ : List (LO.FirstOrder.SyntacticFormula L)} {l : LO.FirstOrder.Derivation.ProofList L} : (∃ (c : LO.FirstOrder.Derivation.Code L), (c, Γ) ∈ l) ↔ Γ ∈ l.sequents

@[simp]

theorem LO.FirstOrder.Derivation.ProofList.sequents_cons {L : LO.FirstOrder.Language} {c : LO.FirstOrder.Derivation.Code L} {Γ : List (LO.FirstOrder.SyntacticFormula L)} {l : LO.FirstOrder.Derivation.ProofList L} : LO.FirstOrder.Derivation.ProofList.sequents ((c, Γ) :: l) = Γ :: l.sequents

theorem LO.FirstOrder.Derivation.ProofList.List.mem_cons_cons {α : Type u_1} (l : List α) (a : α) (b : α) : l ⊆ a :: b :: l

theorem LO.FirstOrder.Derivation.ProofList.Finset.mem_cons_cons {α : Type u_1} [DecidableEq α] (s : Finset α) (a : α) (b : α) : s ⊆ insert a (insert b s)

theorem LO.FirstOrder.Derivation.ProofList.Finset.toList_subset_toList {α : Type u_1} {s₁ : Finset α} {s₂ : Finset α} : s₁.toList ⊆ s₂.toList ↔ s₁ ⊆ s₂

@[irreducible]

theorem LO.FirstOrder.Derivation.ProofList.isProper_ofDerivation {L : LO.FirstOrder.Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] {Γ : LO.FirstOrder.Sequent L} (b : { d : ⊢¹ Γ // LO.FirstOrder.Derivation.CutFree d }) : (LO.FirstOrder.Derivation.ProofList.ofDerivation b).isProper = true

theorem LO.FirstOrder.Derivation.ProofList.derivable_iff_isProper {L : LO.FirstOrder.Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] {Γ : LO.FirstOrder.Sequent L} : Nonempty (⊢¹ Γ) ↔ ∃ (l : LO.FirstOrder.Derivation.ProofList L), l.isProper = true ∧ Γ ∈ l.sequents

theorem LO.FirstOrder.Derivation.ProofList.provable_iff {L : LO.FirstOrder.Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] {T : LO.FirstOrder.Theory L} [DecidablePred T] {σ : LO.FirstOrder.Sentence L} : T ⊢! σ ↔ ∃ (l : LO.FirstOrder.Derivation.ProofList L) (U : List (LO.FirstOrder.Sentence L)), (U.all fun (x : LO.FirstOrder.Sentence L) => decide (T x)) = true ∧ List.map (⇑LO.FirstOrder.Rew.emb.hom) (σ :: List.map (fun (x : LO.FirstOrder.Sentence L) => ~x) U) ∈ l.sequents ∧ l.isProper = true

def LO.FirstOrder.isProofFn {L : LO.FirstOrder.Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Primcodable (L.Func k)] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Func] [UniformlyPrimcodable L.Rel] (T : LO.FirstOrder.Theory L) [DecidablePred T] : LO.FirstOrder.Sentence L → ℕ → Bool

Equations

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

def LO.FirstOrder.Bool.toOpt : Bool → Option Unit

Equations

• LO.FirstOrder.Bool.toOpt b = bif b then some () else none

@[simp]

theorem LO.FirstOrder.isSome_bool_to_opt (b : Bool) : (LO.FirstOrder.Bool.toOpt b).isSome = b

@[simp]

theorem LO.FirstOrder.to_opt_eq_some_iff (b : Bool) : LO.FirstOrder.Bool.toOpt b = some () ↔ b = true

def LO.FirstOrder.provableFn {L : LO.FirstOrder.Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Primcodable (L.Func k)] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Func] [UniformlyPrimcodable L.Rel] (T : LO.FirstOrder.Theory L) [DecidablePred T] : LO.FirstOrder.Sentence L →. Unit

Equations

• LO.FirstOrder.provableFn T x = Nat.rfindOpt fun (e : ℕ) => LO.FirstOrder.Bool.toOpt (LO.FirstOrder.isProofFn T x e)

theorem LO.FirstOrder.provable_iff_isProofFn {L : LO.FirstOrder.Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Primcodable (L.Func k)] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Func] [UniformlyPrimcodable L.Rel] {T : LO.FirstOrder.Theory L} [DecidablePred T] {σ : LO.FirstOrder.Sentence L} : T ⊢! σ ↔ ∃ (e : ℕ), LO.FirstOrder.isProofFn T σ e = true

theorem LO.FirstOrder.provable_iff_provableFn {L : LO.FirstOrder.Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Primcodable (L.Func k)] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Func] [UniformlyPrimcodable L.Rel] {T : LO.FirstOrder.Theory L} [DecidablePred T] {σ : LO.FirstOrder.Sentence L} {u : Unit} : T ⊢! σ ↔ u ∈ LO.FirstOrder.provableFn T σ

class LO.FirstOrder.Theory.Computable {L : LO.FirstOrder.Language} [(k : ℕ) → Primcodable (L.Func k)] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Func] [UniformlyPrimcodable L.Rel] (T : LO.FirstOrder.Theory L) [DecidablePred T] : Type

• comp : Computable fun (x : LO.FirstOrder.Sentence L) => decide (T x)

theorem LO.FirstOrder.Theory.Computable.comp {L : LO.FirstOrder.Language} [(k : ℕ) → Primcodable (L.Func k)] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Func] [UniformlyPrimcodable L.Rel] {T : LO.FirstOrder.Theory L} [DecidablePred T] [self : T.Computable] : Computable fun (x : LO.FirstOrder.Sentence L) => decide (T x)

theorem LO.FirstOrder.isProofFn_computable {L : LO.FirstOrder.Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Primcodable (L.Func k)] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Func] [UniformlyPrimcodable L.Rel] (T : LO.FirstOrder.Theory L) [DecidablePred T] [T.Computable] : Computable₂ (LO.FirstOrder.isProofFn T)

theorem LO.FirstOrder.provableFn_partrec {L : LO.FirstOrder.Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Primcodable (L.Func k)] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Func] [UniformlyPrimcodable L.Rel] (T : LO.FirstOrder.Theory L) [DecidablePred T] [T.Computable] : Partrec (LO.FirstOrder.provableFn T)

theorem LO.FirstOrder.provable_RePred {L : LO.FirstOrder.Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Primcodable (L.Func k)] [(k : ℕ) → Primcodable (L.Rel k)] [UniformlyPrimcodable L.Func] [UniformlyPrimcodable L.Rel] (T : LO.FirstOrder.Theory L) [DecidablePred T] [T.Computable] : RePred fun (x : LO.FirstOrder.Sentence L) => T ⊢! x