Foundation.FirstOrder.NegationTranslation.GoedelGentzen

source

instance LO.FirstOrder.Sequent.instTildeListSemiformula {L : Language} {ξ : Type u_2} {n : ℕ} :

Tilde (List (Semiformula L ξ n))

Equations

LO.FirstOrder.Sequent.instTildeListSemiformula = { tilde := fun (Γ : List (LO.FirstOrder.Semiformula L ξ n)) => List.map (fun (x : LO.FirstOrder.Semiformula L ξ n) => ∼x) Γ }

source

@[simp]

theorem LO.FirstOrder.Sequent.neg_def {L : Language} {ξ : Type u_2} {n : ℕ} (Γ : List (Semiformula L ξ n)) :

∼Γ = List.map (fun (x : Semiformula L ξ n) => ∼x) Γ

source

@[simp]

theorem LO.FirstOrder.Sequent.neg_nil {L : Language} {ξ : Type u_2} {n : ℕ} :

∼[] = []

source

@[simp]

theorem LO.FirstOrder.Sequent.neg_cons {L : Language} {ξ : Type u_2} {n : ℕ} (Γ : List (Semiformula L ξ n)) (φ : Semiformula L ξ n) :

∼(φ :: Γ) = ∼φ :: ∼Γ

source

@[simp]

theorem LO.FirstOrder.Sequent.neg_neg_eq {L : Language} {ξ : Type u_2} {n : ℕ} (Γ : List (Semiformula L ξ n)) :

∼∼Γ = Γ

source

def LO.FirstOrder.Semiformula.doubleNegation {L : Language} {ξ : Type u_2} {n : ℕ} :

Semiformula L ξ n → Semiformulaᵢ L ξ n

Equations

Instances For

source

def LO.FirstOrder.«term_ᴺ» :

Lean.TrailingParserDescr

Equations

LO.FirstOrder.«term_ᴺ» = Lean.ParserDescr.trailingNode `LO.FirstOrder.«term_ᴺ» 1024 1024 (Lean.ParserDescr.symbol "ᴺ")

Instances For

source

@[simp]

theorem LO.FirstOrder.Semiformula.doubleNegation_rel {L : Language} {ξ : Type u_2} {n k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ξ n) :

(rel r v).doubleNegation = ∼∼Semiformulaᵢ.rel r v

source

@[simp]

theorem LO.FirstOrder.Semiformula.doubleNegation_nrel {L : Language} {ξ : Type u_2} {n k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ξ n) :

(nrel r v).doubleNegation = ∼Semiformulaᵢ.rel r v

source

@[simp]

theorem LO.FirstOrder.Semiformula.doubleNegation_verum {L : Language} {ξ : Type u_2} {n : ℕ} :

⊤.doubleNegation = ∼⊥

source

@[simp]

theorem LO.FirstOrder.Semiformula.doubleNegation_falsum {L : Language} {ξ : Type u_2} {n : ℕ} :

⊥.doubleNegation = ⊥

source

@[simp]

theorem LO.FirstOrder.Semiformula.doubleNegation_and {L : Language} {ξ : Type u_2} {n : ℕ} (φ ψ : Semiformula L ξ n) :

(φ ⋏ ψ).doubleNegation = φ.doubleNegation ⋏ ψ.doubleNegation

source

@[simp]

theorem LO.FirstOrder.Semiformula.doubleNegation_or {L : Language} {ξ : Type u_2} {n : ℕ} (φ ψ : Semiformula L ξ n) :

(φ ⋎ ψ).doubleNegation = ∼(∼φ.doubleNegation ⋏ ∼ψ.doubleNegation)

source

@[simp]

theorem LO.FirstOrder.Semiformula.doubleNegation_all {L : Language} {ξ : Type u_2} {n : ℕ} (φ : Semiformula L ξ (n + 1)) :

(∀' φ).doubleNegation = ∀' φ.doubleNegation

source

@[simp]

theorem LO.FirstOrder.Semiformula.doubleNegation_ex {L : Language} {ξ : Type u_2} {n : ℕ} (φ : Semiformula L ξ (n + 1)) :

(∃' φ).doubleNegation = ∼(∀' ∼φ.doubleNegation)

source

theorem LO.FirstOrder.Semiformula.doubleNegation_imply {L : Language} {ξ : Type u_2} {n : ℕ} (φ ψ : Semiformula L ξ n) :

(φ ➝ ψ).doubleNegation = ∼(∼(∼φ).doubleNegation ⋏ ∼ψ.doubleNegation)

source

@[simp]

theorem LO.FirstOrder.Semiformula.doubleNegation_isNegative {L : Language} {ξ : Type u_2} {n : ℕ} (φ : Semiformula L ξ n) :

φ.doubleNegation.IsNegative

source

@[simp]

theorem LO.FirstOrder.Semiformula.doubleNegation_conj₂ {L : Language} {ξ : Type u_2} {n : ℕ} (Γ : List (Semiformula L ξ n)) :

(⋀Γ).doubleNegation = ⋀List.map doubleNegation Γ

source

theorem LO.FirstOrder.Semiformula.doubleNegation_fconj {L : Language} {ξ : Type u_2} {n : ℕ} (s : Finset (Semiformula L ξ n)) :

s.conj.doubleNegation = ⋀List.map doubleNegation s.toList

source

theorem LO.FirstOrder.Semiformula.rew_doubleNegation {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) (φ : Semiformula L ξ₁ n₁) :

(Rewriting.app ω) φ.doubleNegation = ((Rewriting.app ω) φ).doubleNegation

source

theorem LO.FirstOrder.Semiformula.subst_doubleNegation {L : Language} {ξ : Type u_2} {n₁ n₂ : ℕ} (φ : Semiformula L ξ n₁) (v : Fin n₁ → Semiterm L ξ n₂) :

φ.doubleNegation ⇜ v = (φ ⇜ v).doubleNegation

source

theorem LO.FirstOrder.Semiformula.emb_doubleNegation {L : Language} {n₁ : ℕ} {ξ : Type u_2} (φ : Semisentence L n₁) :

↑(doubleNegation φ) = (↑φ).doubleNegation

source

@[reducible, inline]

abbrev LO.FirstOrder.Sequent.doubleNegation {L : Language} {ξ : Type u_2} {n : ℕ} (Γ : List (Semiformula L ξ n)) :

List (Semiformulaᵢ L ξ n)

Equations

LO.FirstOrder.Sequent.doubleNegation Γ = List.map (fun (x : LO.FirstOrder.Semiformula L ξ n) => x.doubleNegation) Γ

Instances For

source

def LO.FirstOrder.«term_ᴺ_1» :

Lean.TrailingParserDescr

Equations

LO.FirstOrder.«term_ᴺ_1» = Lean.ParserDescr.trailingNode `LO.FirstOrder.«term_ᴺ_1» 1024 1024 (Lean.ParserDescr.symbol "ᴺ")

Instances For

source

def LO.FirstOrder.Theory.ToTheoryᵢ {L : Language} (T : Theory L) (Λ : Hilbertᵢ L) :

Theoryᵢ L Λ

Equations

T.ToTheoryᵢ Λ = { theory := LO.FirstOrder.Semiformula.doubleNegation '' T }

Instances For

source

@[simp]

theorem LO.FirstOrder.Theory.ToTheoryᵢ_theory_def {L : Language} (T : Theory L) (Λ : Hilbertᵢ L) :

(T.ToTheoryᵢ Λ).theory = Semiformula.doubleNegation '' T

source

@[irreducible]

noncomputable def LO.FirstOrder.Derivation.negDoubleNegation {L : Language} [L.DecidableEq] {Λ : Hilbertᵢ L} (φ : SyntacticFormula L) :

Λ ⊢! ∼Semiformula.doubleNegation φ ⭤ (∼φ).doubleNegation

Equations

Instances For

source

theorem LO.FirstOrder.Derivation.neg_doubleNegation {L : Language} [L.DecidableEq] {Λ : Hilbertᵢ L} (φ : SyntacticFormula L) :

Λ ⊢ ∼Semiformula.doubleNegation φ ⭤ (∼φ).doubleNegation

source

theorem LO.FirstOrder.Derivation.neg_doubleNegation' {L : Language} [L.DecidableEq] {Λ : Hilbertᵢ L} (φ : SyntacticFormula L) :

Λ ⊢ ∼(∼φ).doubleNegation ⭤ Semiformula.doubleNegation φ

source

theorem LO.FirstOrder.Derivation.imply_doubleNegation {L : Language} [L.DecidableEq] {Λ : Hilbertᵢ L} (φ ψ : SyntacticFormula L) :

Λ ⊢ (Semiformula.doubleNegation φ ➝ Semiformula.doubleNegation ψ) ⭤ (φ ➝ ψ).doubleNegation

source

noncomputable def LO.FirstOrder.Derivation.gödelGentzen {L : Language} [L.DecidableEq] {Λ : Hilbertᵢ L} {Γ : Sequent L} :

⊢ᵀ Γ → Sequent.doubleNegation (∼Γ) ⊢[Λ]! ⊥

Equations

One or more equations did not get rendered due to their size.
(LO.FirstOrder.Derivation.axL Γ_2 r v).gödelGentzen = LO.Entailment.FiniteContext.nthAxm 1 ⋯⨀LO.Entailment.FiniteContext.nthAxm 0 ⋯
(LO.FirstOrder.Derivation.verum Γ_2).gödelGentzen = LO.Entailment.FiniteContext.nthAxm 0 ⋯
(d.wk h).gödelGentzen = LO.Entailment.FiniteContext.weakening ⋯ d.gödelGentzen

Instances For

source

theorem LO.FirstOrder.gödel_gentzen {L : Language} {Λ : Hilbertᵢ L} {T : Theory L} {φ : Sentence L} :

T ⊢ φ → T.ToTheoryᵢ Λ ⊢ Semiformula.doubleNegation φ

Gödel-Gentzen translation of classical first-order logic to intiotionistic first-order logic.