Natural deduction for propositional logic

We define, for minimal logic, deduction trees (a Type) and derivability (a Prop) relative to a Theory (set of propositions).

Main definitions

• Sequent : a pair of a context and conclusion.
• Derivation : natural deduction derivation, done in "sequent style", ie with explicit hypotheses at each step. Contexts are Finset's of propositions, which avoids explicit contraction and exchange, and the axiom rule derives Γ ⊢ A for any context Γ with A ∈ Γ, allowing weakening to be a derived rule. The derivation may appeal to hypotheses from the Theory T. This defines an instance of InferenceSystem T Sequent.
• Theory.equiv : Type-valued equivalence of propositions.
• Theory.Equiv : Prop-valued equivalence of propositions.

Main results

• Derivation.weak : weakening as a derived rule.
• Derivation.cut, Derivation.subs : replace a hypothesis in a derivation — the two versions differ in the construction of the relevant derivation.
• Theory.equiv_equivalence : equivalence of propositions is an equivalence relation.

Notation

The sequent ⟨Γ, A⟩ is notated Γ ⊢ A, so that a derivation using axioms from a theory T is noted T⇓(Γ ⊢ A). We define also an InferenceSystem T (Proposition Atom), so that T⇓A abbreviates a derivation of A in the empty context: T⇓(∅ ⊢ A).

Implementation notes

We formalise here a single type of derivations, meaning there is a single collection of inference rules (those for minimal logic). The extension to intuitionistic and classical logic are modelled by adding axioms --- for instance, intuitionistic derivations are allowed to appeal to axioms of the form ⊥ → A for any proposition A. This differs from many on-paper presentations, which add that principle as a deduction rule: from Γ ⊢ ⊥ derive Γ ⊢ A. Discussion on proper way to capture such developments in cslib is ongoing, see the following zulip discussion.

References

• Dag Prawitz, Natural Deduction: a proof-theoretical study.
• The sequent-style natural deduction I present here doesn't seem to be common, but it is tersely presented in §10.4 of Troelstra & van Dalen's Constructivism in Mathematics: an introduction, and in §2.2 of Sorensen & Urzyczyn's Lectures on the Curry-Howard Isomorphism. (Suggestions of better references welcome!)

@[reducible, inline]

abbrev Cslib.Logic.PL.Ctx (Atom : Type u_1) : Type u_1

Contexts are finsets of propositions.

Equations

• Cslib.Logic.PL.Ctx Atom = Finset (Cslib.Logic.PL.Proposition Atom)

def Cslib.Logic.PL.Ctx.subst {Atom Atom' : Type u} [DecidableEq Atom'] (f : Atom → Proposition Atom') : Ctx Atom → Ctx Atom'

Map a context along a substitution.

Equations

• Cslib.Logic.PL.Ctx.subst f = Finset.image fun (x : Cslib.Logic.PL.Proposition Atom) => x >>= f

@[reducible, inline]

abbrev Cslib.Logic.PL.Sequent {Atom : Type u_1} : Type u_1

Sequents {A₁, ..., Aₙ} ⊢ B.

Equations

• Cslib.Logic.PL.Sequent = (Cslib.Logic.PL.Ctx Atom × Cslib.Logic.PL.Proposition Atom)

def Cslib.Logic.PL.«term_⊢_» : Lean.TrailingParserDescr

Sequents {A₁, ..., Aₙ} ⊢ B.

Equations

• Cslib.Logic.PL.«term_⊢_» = Lean.ParserDescr.trailingNode `Cslib.Logic.PL.«term_⊢_» 1022 60 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊢ ") (Lean.ParserDescr.cat `term 0))

inductive Cslib.Logic.PL.Theory.Derivation {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} : Ctx Atom → Proposition Atom → Type u

A T-derivation of {A₁, ..., Aₙ} ⊢ B demonstrates B using (undischarged) assumptions among Aᵢ, possibly appealing to axioms from T.

• ax {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} {Γ : Ctx Atom} {A : Proposition Atom} : A ∈ T → Derivation Γ A

  Axiom

• ass {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} {Γ : Ctx Atom} {A : Proposition Atom} : A ∈ Γ → Derivation Γ A

  Assumption

• andI {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation Γ A → Derivation Γ B → Derivation Γ (A.and B)

  Conjunction introduction

• andE₁ {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation Γ (A.and B) → Derivation Γ A

  Conjunction elimination left

• andE₂ {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation Γ (A.and B) → Derivation Γ B

  Conjunction elimination right

• orI₁ {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation Γ A → Derivation Γ (A.or B)

  Disjunction introduction left

• orI₂ {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation Γ B → Derivation Γ (A.or B)

  Disjunction introduction right

• orE {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} {Γ : Ctx Atom} {A B C : Proposition Atom} : Derivation Γ (A.or B) → Derivation (insert A Γ) C → Derivation (insert B Γ) C → Derivation Γ C

  Disjunction elimination

• implI {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} {A B : Proposition Atom} (Γ : Ctx Atom) : Derivation (insert A Γ) B → Derivation Γ (A.impl B)

  Implication introduction

• implE {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation Γ (A.impl B) → Derivation Γ A → Derivation Γ B

  Implication elimination

@[implicit_reducible]

instance Cslib.Logic.PL.instInferenceSystemElemPropositionSequent {Atom : Type u} [DecidableEq Atom] (T : Theory Atom) : InferenceSystem (↑T) Sequent

Inference system for derivations under the theory T.

Equations

• Cslib.Logic.PL.instInferenceSystemElemPropositionSequent T = { derivation := fun (S : Cslib.Logic.PL.Sequent) => Cslib.Logic.PL.Theory.Derivation S.1 S.2 }

@[implicit_reducible]

instance Cslib.Logic.PL.instInferenceSystemElemProposition {Atom : Type u} [DecidableEq Atom] (T : Theory Atom) : InferenceSystem (↑T) (Proposition Atom)

Inference system for propositions (using the empty context).

Equations

• Cslib.Logic.PL.instInferenceSystemElemProposition T = { derivation := fun (A : Cslib.Logic.PL.Proposition Atom) => Cslib.Logic.PL.Theory.Derivation ∅ A }

theorem Cslib.Logic.PL.Theory.Derivation.emptySequent_eq {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} {A : Proposition Atom} : InferenceSystem.derivation (↑T) A = InferenceSystem.derivation ↑T (∅, A)

theorem Cslib.Logic.PL.DerivableIn.iff_derivableIn_empty {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} {A : Proposition Atom} : InferenceSystem.DerivableIn (↑T) A ↔ InferenceSystem.DerivableIn ↑T (∅, A)

def Cslib.Logic.PL.Theory.equiv {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} (A B : Proposition Atom) : Type u

An equivalence between A and B is a derivation of B from A and vice-versa.

Equations

• Cslib.Logic.PL.Theory.equiv A B = (Cslib.Logic.InferenceSystem.derivation ↑T ({A}, B) × Cslib.Logic.InferenceSystem.derivation ↑T ({B}, A))

def Cslib.Logic.PL.Theory.equiv.mp {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} {A B : Proposition Atom} (e : equiv A B) : InferenceSystem.derivation ↑T ({A}, B)

Forward direction of an equivalence.

Equations

• e.mp = e.1

def Cslib.Logic.PL.Theory.equiv.mpr {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} {A B : Proposition Atom} (e : equiv A B) : InferenceSystem.derivation ↑T ({B}, A)

Reverse direction of an equivalence.

Equations

• e.mpr = e.2

def Cslib.Logic.PL.Theory.Equiv {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} (A B : Proposition Atom) : Prop

A and B are T-equivalent if T.equiv A B is nonempty.

Equations

• Cslib.Logic.PL.Theory.Equiv A B = Nonempty (Cslib.Logic.PL.Theory.equiv A B)

def Cslib.Logic.PL.«term_≡[_]_» : Lean.TrailingParserDescr

A and B are T-equivalent if T.equiv A B is nonempty.

Equations

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

theorem Cslib.Logic.PL.Theory.Equiv.mp {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} {A B : Proposition Atom} (h : Equiv A B) : InferenceSystem.DerivableIn ↑T ({A}, B)

theorem Cslib.Logic.PL.Theory.Equiv.mpr {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} {A B : Proposition Atom} (h : Equiv A B) : InferenceSystem.DerivableIn ↑T ({B}, A)

theorem Cslib.Logic.PL.Theory.equiv_iff {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} {A B : Proposition Atom} : Equiv A B ↔ InferenceSystem.DerivableIn ↑T ({A}, B) ∧ InferenceSystem.DerivableIn ↑T ({B}, A)

@[reducible, inline]

abbrev Cslib.Logic.PL.Equiv {Atom : Type u} [DecidableEq Atom] : Proposition Atom → Proposition Atom → Prop

Minimally equivalent propositions.

Equations

• Cslib.Logic.PL.Equiv = Cslib.Logic.PL.Theory.Equiv

def Cslib.Logic.PL.«term_≡_» : Lean.TrailingParserDescr

Minimally equivalent propositions.

Equations

• Cslib.Logic.PL.«term_≡_» = Lean.ParserDescr.trailingNode `Cslib.Logic.PL.«term_≡_» 29 30 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≡ ") (Lean.ParserDescr.cat `term 30))

Operations on derivations

def Cslib.Logic.PL.Theory.Derivation.weak {Atom : Type u} [DecidableEq Atom] {T T' : Theory Atom} {Γ Δ : Ctx Atom} {A : Proposition Atom} (hTheory : T ⊆ T') (hCtx : Γ ⊆ Δ) : Derivation Γ A → Derivation Δ A

Weakening is a derived rule.

Equations

• One or more equations did not get rendered due to their size.
• Cslib.Logic.PL.Theory.Derivation.weak hTheory hCtx (Cslib.Logic.PL.Theory.Derivation.ax hA) = Cslib.Logic.PL.Theory.Derivation.ax ⋯
• Cslib.Logic.PL.Theory.Derivation.weak hTheory hCtx (Cslib.Logic.PL.Theory.Derivation.ass hA) = Cslib.Logic.PL.Theory.Derivation.ass ⋯
• Cslib.Logic.PL.Theory.Derivation.weak hTheory hCtx (D.andI D') = (Cslib.Logic.PL.Theory.Derivation.weak hTheory hCtx D).andI (Cslib.Logic.PL.Theory.Derivation.weak hTheory hCtx D')
• Cslib.Logic.PL.Theory.Derivation.weak hTheory hCtx D.andE₁ = (Cslib.Logic.PL.Theory.Derivation.weak hTheory hCtx D).andE₁
• Cslib.Logic.PL.Theory.Derivation.weak hTheory hCtx D.andE₂ = (Cslib.Logic.PL.Theory.Derivation.weak hTheory hCtx D).andE₂
• Cslib.Logic.PL.Theory.Derivation.weak hTheory hCtx D.orI₁ = (Cslib.Logic.PL.Theory.Derivation.weak hTheory hCtx D).orI₁
• Cslib.Logic.PL.Theory.Derivation.weak hTheory hCtx D.orI₂ = (Cslib.Logic.PL.Theory.Derivation.weak hTheory hCtx D).orI₂
• Cslib.Logic.PL.Theory.Derivation.weak hTheory hCtx (Cslib.Logic.PL.Theory.Derivation.implI Γ D) = Cslib.Logic.PL.Theory.Derivation.implI Δ (Cslib.Logic.PL.Theory.Derivation.weak hTheory ⋯ D)
• Cslib.Logic.PL.Theory.Derivation.weak hTheory hCtx (D.implE D') = (Cslib.Logic.PL.Theory.Derivation.weak hTheory hCtx D).implE (Cslib.Logic.PL.Theory.Derivation.weak hTheory hCtx D')

def Cslib.Logic.PL.Theory.Derivation.weak_theory {Atom : Type u} [DecidableEq Atom] {T T' : Theory Atom} {Γ : Ctx Atom} {A : Proposition Atom} (hTheory : T ⊆ T') : InferenceSystem.derivation ↑T (Γ, A) → InferenceSystem.derivation ↑T' (Γ, A)

Weakening the theory only.

Equations

• Cslib.Logic.PL.Theory.Derivation.weak_theory hTheory = Cslib.Logic.PL.Theory.Derivation.weak hTheory ⋯

def Cslib.Logic.PL.Theory.Derivation.weak_ctx {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} {Γ Δ : Ctx Atom} {A : Proposition Atom} (hCtx : Γ ⊆ Δ) : InferenceSystem.derivation ↑T (Γ, A) → InferenceSystem.derivation ↑T (Δ, A)

Weakening the context only.

Equations

• Cslib.Logic.PL.Theory.Derivation.weak_ctx hCtx = Cslib.Logic.PL.Theory.Derivation.weak ⋯ hCtx

theorem Cslib.Logic.PL.DerivableIn.weak {Atom : Type u} [DecidableEq Atom] {T T' : Theory Atom} {Γ Δ : Ctx Atom} {A : Proposition Atom} (hTheory : T ⊆ T') (hCtx : Γ ⊆ Δ) : InferenceSystem.DerivableIn ↑T (Γ, A) → InferenceSystem.DerivableIn ↑T' (Δ, A)

Proof irrelevant weakening.

theorem Cslib.Logic.PL.DerivableIn.weak_theory {Atom : Type u} [DecidableEq Atom] {T T' : Theory Atom} {Γ : Ctx Atom} {A : Proposition Atom} (hTheory : T ⊆ T') : InferenceSystem.DerivableIn ↑T (Γ, A) → InferenceSystem.DerivableIn ↑T' (Γ, A)

Proof irrelevant weakening of the theory.

theorem Cslib.Logic.PL.DerivableIn.weak_ctx {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} {Γ Δ : Ctx Atom} {A : Proposition Atom} (hCtx : Γ ⊆ Δ) : InferenceSystem.DerivableIn ↑T (Γ, A) → InferenceSystem.DerivableIn ↑T (Δ, A)

Proof irrelevant weakening of the context.

def Cslib.Logic.PL.Theory.Derivation.cut {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} {Γ Δ : Ctx Atom} {A B : Proposition Atom} (D : InferenceSystem.derivation ↑T (Γ, A)) (E : InferenceSystem.derivation ↑T (insert A Δ, B)) : InferenceSystem.derivation ↑T (Γ ∪ Δ, B)

Implement the cut rule, removing a hypothesis A from E using a derivation D. This is not substitution, which would replace appeals to A in E by the whole derivation D.

Equations

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

theorem Cslib.Logic.PL.DerivableIn.cut {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} {Γ Δ : Ctx Atom} {A B : Proposition Atom} : InferenceSystem.DerivableIn ↑T (Γ, A) → InferenceSystem.DerivableIn ↑T (insert A Δ, B) → InferenceSystem.DerivableIn ↑T (Γ ∪ Δ, B)

Proof irrelevant cut rule.

theorem Cslib.Logic.PL.DerivableIn.cut_away {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} {Γ Γ' : Ctx Atom} {B : Proposition Atom} (hΔ : ∀ A ∈ Γ', InferenceSystem.DerivableIn ↑T (Γ, A)) (hDer : InferenceSystem.DerivableIn ↑T (Γ ∪ Γ', B)) : InferenceSystem.DerivableIn ↑T (Γ, B)

Remove unnecessary hypotheses. This can't be computable because it requires picking an order on the finset Δ.

def Cslib.Logic.PL.Theory.Derivation.subs {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} {Γ Γ' Δ : Ctx Atom} {B : Proposition Atom} (Ds : (A : Proposition Atom) → A ∈ Γ' → InferenceSystem.derivation ↑T (Δ, A)) : Derivation Γ B → Derivation (Γ \ Γ' ∪ Δ) B

Substitution of a family of derivations D for hypotheses in the context Γ of E. TODO: this implementation is not capture avoiding.

Equations

• One or more equations did not get rendered due to their size.
• Cslib.Logic.PL.Theory.Derivation.subs Ds (Cslib.Logic.PL.Theory.Derivation.ax hB) = Cslib.Logic.PL.Theory.Derivation.ax hB
• Cslib.Logic.PL.Theory.Derivation.subs Ds (E.andI E') = (Cslib.Logic.PL.Theory.Derivation.subs Ds E).andI (Cslib.Logic.PL.Theory.Derivation.subs Ds E')
• Cslib.Logic.PL.Theory.Derivation.subs Ds E.andE₁ = (Cslib.Logic.PL.Theory.Derivation.subs Ds E).andE₁
• Cslib.Logic.PL.Theory.Derivation.subs Ds E.andE₂ = (Cslib.Logic.PL.Theory.Derivation.subs Ds E).andE₂
• Cslib.Logic.PL.Theory.Derivation.subs Ds E.orI₁ = (Cslib.Logic.PL.Theory.Derivation.subs Ds E).orI₁
• Cslib.Logic.PL.Theory.Derivation.subs Ds E.orI₂ = (Cslib.Logic.PL.Theory.Derivation.subs Ds E).orI₂
• Cslib.Logic.PL.Theory.Derivation.subs Ds (E.implE E') = (Cslib.Logic.PL.Theory.Derivation.subs Ds E).implE (Cslib.Logic.PL.Theory.Derivation.subs Ds E')

def Cslib.Logic.PL.Theory.Derivation.substAtom {Atom Atom' : Type u} [DecidableEq Atom] [DecidableEq Atom'] {T : Theory Atom} (f : Atom → Proposition Atom') {Γ : Ctx Atom} {B : Proposition Atom} : Derivation Γ B → Derivation (Ctx.subst f Γ) (B >>= f)

Transport a derivation along a substitution of atoms.

Equations

• One or more equations did not get rendered due to their size.
• Cslib.Logic.PL.Theory.Derivation.substAtom f (Cslib.Logic.PL.Theory.Derivation.ax hB) = Cslib.Logic.PL.Theory.Derivation.ax ⋯
• Cslib.Logic.PL.Theory.Derivation.substAtom f (Cslib.Logic.PL.Theory.Derivation.ass hB) = Cslib.Logic.PL.Theory.Derivation.ass ⋯
• Cslib.Logic.PL.Theory.Derivation.substAtom f (E.andI E') = (Cslib.Logic.PL.Theory.Derivation.substAtom f E).andI (Cslib.Logic.PL.Theory.Derivation.substAtom f E')
• Cslib.Logic.PL.Theory.Derivation.substAtom f E.andE₁ = (Cslib.Logic.PL.Theory.Derivation.substAtom f E).andE₁
• Cslib.Logic.PL.Theory.Derivation.substAtom f E.andE₂ = (Cslib.Logic.PL.Theory.Derivation.substAtom f E).andE₂
• Cslib.Logic.PL.Theory.Derivation.substAtom f E.orI₁ = (Cslib.Logic.PL.Theory.Derivation.substAtom f E).orI₁
• Cslib.Logic.PL.Theory.Derivation.substAtom f E.orI₂ = (Cslib.Logic.PL.Theory.Derivation.substAtom f E).orI₂
• Cslib.Logic.PL.Theory.Derivation.substAtom f (E.implE E') = (Cslib.Logic.PL.Theory.Derivation.substAtom f E).implE (Cslib.Logic.PL.Theory.Derivation.substAtom f E')

theorem Cslib.Logic.PL.DerivableIn.substAtom {Atom Atom' : Type u} [DecidableEq Atom] [DecidableEq Atom'] {T : Theory Atom} (f : Atom → Proposition Atom') {Γ : Ctx Atom} {B : Proposition Atom} : InferenceSystem.DerivableIn ↑T (Γ, B) → InferenceSystem.DerivableIn ↑(T.subst f) (Ctx.subst f Γ, B >>= f)

Properties of equivalence

def Cslib.Logic.PL.Theory.derivationTop {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} [Inhabited Atom] : InferenceSystem.derivation ↑T ⊤

A derivation of the canonical tautology.

Equations

• Cslib.Logic.PL.Theory.derivationTop = Cslib.Logic.PL.Theory.Derivation.implI ∅ (Cslib.Logic.PL.Theory.Derivation.ass ⋯)

theorem Cslib.Logic.PL.derivableIn_top {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} [Inhabited Atom] : InferenceSystem.DerivableIn ↑T ⊤

theorem Cslib.Logic.PL.derivable_iff_equiv_top {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} [Inhabited Atom] (A : Proposition Atom) : InferenceSystem.DerivableIn (↑T) A ↔ Theory.Equiv A ⊤

def Cslib.Logic.PL.Theory.mapEquivConclusion {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} (Γ : Ctx Atom) {A B : Proposition Atom} (e : equiv A B) (D : InferenceSystem.derivation ↑T (Γ, A)) : InferenceSystem.derivation ↑T (Γ, B)

Change the conclusion along an equivalence.

Equations

• Cslib.Logic.PL.Theory.mapEquivConclusion Γ e D = ⋯ ▸ Cslib.Logic.PL.Theory.Derivation.cut D e.1

def Cslib.Logic.PL.Theory.mapEquivHypothesis {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} (Γ : Ctx Atom) {A B : Proposition Atom} (e : equiv A B) (C : Proposition Atom) (D : InferenceSystem.derivation ↑T (insert A Γ, C)) : InferenceSystem.derivation ↑T (insert B Γ, C)

Replace a hypothesis along an equivalence.

Equations

• Cslib.Logic.PL.Theory.mapEquivHypothesis Γ e C D = ⋯ ▸ Cslib.Logic.PL.Theory.Derivation.cut e.2 D

def Cslib.Logic.PL.Theory.equiv.refl {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} (A : Proposition Atom) : equiv A A

An equivalence of a proposition with itself.

Equations

• Cslib.Logic.PL.Theory.equiv.refl A = (Cslib.Logic.PL.Theory.Derivation.ass ⋯, Cslib.Logic.PL.Theory.Derivation.ass ⋯)

def Cslib.Logic.PL.Theory.equiv.symm {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} {A B : Proposition Atom} (e : equiv A B) : equiv B A

Reverse an equivalence.

Equations

• e.symm = (e.mpr, e.mp)

def Cslib.Logic.PL.Theory.equiv.trans {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} {A B C : Proposition Atom} (eAB : equiv A B) (eBC : equiv B C) : equiv A C

Compose two equivalences.

Equations

• eAB.trans eBC = (Cslib.Logic.PL.Theory.mapEquivConclusion {A} eBC eAB.mp, Cslib.Logic.PL.Theory.mapEquivConclusion {C} eAB.symm eBC.mpr)

theorem Cslib.Logic.PL.Theory.equiv_iff_equiv_derivableIn {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} {A B : Proposition Atom} : Equiv A B ↔ ∀ (Γ : Ctx Atom), InferenceSystem.DerivableIn ↑T (Γ, A) ↔ InferenceSystem.DerivableIn ↑T (Γ, B)

A and B are equivalent (in T) iff they are provable from the same contexts.

theorem Cslib.Logic.PL.Theory.equiv_iff_equiv_derivableIn_hypothesis {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} {A B : Proposition Atom} : Equiv A B ↔ ∀ (Γ : Ctx Atom) (C : Proposition Atom), InferenceSystem.DerivableIn ↑T (insert A Γ, C) ↔ InferenceSystem.DerivableIn ↑T (insert B Γ, C)

A and B are equivalent (in T) iff they have the same strength as hypotheses.

theorem Cslib.Logic.PL.Theory.Equiv.refl {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} (A : Proposition Atom) : Equiv A A

theorem Cslib.Logic.PL.Theory.Equiv.symm {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} {A B : Proposition Atom} : Equiv A B → Equiv B A

theorem Cslib.Logic.PL.Theory.Equiv.trans {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} {A B C : Proposition Atom} : Equiv A B → Equiv B C → Equiv A C

theorem Cslib.Logic.PL.Theory.equiv_equivalence {Atom : Type u} [DecidableEq Atom] (T : Theory Atom) : Equivalence Equiv

Equivalence is indeed an equivalence relation.

def Cslib.Logic.PL.Theory.propositionSetoid {Atom : Type u} [DecidableEq Atom] (T : Theory Atom) : Setoid (Proposition Atom)

The setoid of propositions under equivalence.

Equations

• T.propositionSetoid = { r := Cslib.Logic.PL.Theory.Equiv, iseqv := ⋯ }