Propositional natural deduction

DefinitionTruth-table evaluation#✓fully proved

Given a Boolean valuation \(v\) of the atoms, the truth value of a proposition is computed recursively: an atom \(x\) has value \(v(x)\), \(A \wedge B\) is true iff both \(A\) and \(B\) are, \(A \vee B\) is true iff at least one of them is, and \(A \to B\) is true iff \(A\) is false or \(B\) is true. Falsum \(\bot\), when present, is itself an atom, so its value \(v(\bot)\) is part of the valuation and need not be false.

def Proposition.evalBool (v : Atom → Bool) : Proposition Atom → Bool
  | atom x => v x
  | and A B => A.evalBool v && B.evalBool v
  | or A B => A.evalBool v || B.evalBool v
  | imp A B => !A.evalBool v || B.evalBool v
Used by 38
Used byThe embedding of propositions preserves truth-table semantics · Equal BDDs iff equal truth tables · Satisfiable iff the BDD is not the false leaf · The all-true valuation satisfies every proposition · Satisfiability with one variable fixed to false · Satisfy-one for propositions · Satisfy-one with a variable fixed to false · Satisfiability of a CNF with falsum false · Equivalent CNF · The truth value depends only on the atoms · Truth of a Boolean quantification over a list of atoms · Craig interpolation, semantic form · Craig interpolation for classical natural deduction · The translation into \(\to\) and \(\bot\) preserves and reflects classical derivability · Correctness of the Shannon expansion · The translation into \(\to\) and \(\bot\) preserves truth values · Functional completeness · Functional completeness of → and ⊥ · Truth-table consequence · Satisfiable sets of propositions · Model existence for propositional natural deduction · Compactness · Soundness of natural deduction for truth tables · Completeness for truth tables · Soundness and completeness for classical theories, with ⊥ false · Strong completeness of classical propositional natural deduction · Truth lemma for propositional natural deduction · Truth value of a negation · Classical derivability implies truth under valuations with false falsum · Intuitionistic derivability implies truth under valuations with false falsum · Double-negation elimination is true when falsum is false · Ex falso is true when falsum is false · Classical logic proves no atom · Consistency of classical propositional logic · Value of a proposition read off the atom variables · Equisatisfiability of the Tseitin transformation · Tseitin correctness · Correctness invariant of the Tseitin encoding

TheoremTruth value of a negation#✓fully proved

Suppose the atoms include a distinguished atom \(\bot\), and let \(v\) be a Boolean valuation of the atoms with \(v(\bot) = \mathrm{false}\). Then for every proposition \(A\), the truth-table value under \(v\) of \(\neg A\), defined as \(A \to \bot\), is the Boolean negation of the truth-table value of \(A\) under \(v\).

theorem evalBool_neg [Bot Atom] (hv : v ⊥ = false) :
    (¬A : Proposition Atom).evalBool v = !A.evalBool v
Uses 1 · Used by 2
Statement usesTruth-table evaluation
Used byCorrectness of the Shannon expansion · Strong completeness of classical propositional natural deduction

DefinitionTruth-table consequence#✓fully proved

Let \(T\) be a theory (a set of propositions), \(\Gamma\) a context (a finite set of propositions) and \(A\) a proposition. Then \(A\) is a truth-table consequence of \(\Gamma\) in \(T\) when every Boolean valuation of the atoms under which all members of \(T\) and all members of \(\Gamma\) evaluate to true also makes \(A\) evaluate to true.

def Theory.BoolEntails (T : Theory Atom) (Γ : Ctx Atom) (A : Proposition Atom) : Prop :=
  ∀ v : Atom → Bool, (∀ B ∈ T, B.evalBool v = true) → (∀ B ∈ Γ, B.evalBool v = true) →
    A.evalBool v = true
Uses 1 · Used by 3
Statement usesTruth-table evaluation
Used bySoundness of natural deduction for truth tables · Truth-table soundness of derivability · Soundness and completeness for classical theories

TheoremSoundness of natural deduction for truth tables#✓fully proved

Let \(T\) be a theory, \(\Gamma\) a context and \(A\) a proposition. For every natural-deduction derivation of \(\Gamma \vdash A\) with axioms from \(T\), every Boolean valuation of the atoms that makes all members of \(T\) and of \(\Gamma\) true makes \(A\) true.

theorem Theory.Derivation.boolSound {Γ : Ctx Atom} {A : Proposition Atom}
    (D : T.Derivation Γ A) : T.BoolEntails Γ A
Uses 2 · Used by 1
Statement usesTruth-table consequence
Proof usesTruth-table evaluation
Used byTruth-table soundness of derivability

TheoremTruth-table soundness of derivability#✓fully proved

Let \(T\) be a theory, \(\Gamma\) a context and \(A\) a proposition. If the sequent \(\Gamma \vdash A\) is derivable in natural deduction with axioms from \(T\), then \(A\) is a truth-table consequence of \(\Gamma\) in \(T\): every Boolean valuation of the atoms that makes all members of \(T\) and of \(\Gamma\) true makes \(A\) true.

theorem DerivableIn.boolSound {Γ : Ctx Atom} {A : Proposition Atom}
    (h : DerivableIn T (Γ ⊢ A)) : T.BoolEntails Γ A
Uses 2 · Used by 4
Statement usesTruth-table consequence
Proof usesSoundness of natural deduction for truth tables
Used bySoundness and completeness for classical theories · Soundness and completeness for classical theories, with ⊥ false · Classical derivability implies truth under valuations with false falsum · Intuitionistic derivability implies truth under valuations with false falsum

TheoremEx falso is true when falsum is false#✓fully proved

Suppose the atoms include a distinguished atom \(\bot\), and let \(v\) be a Boolean valuation of the atoms with \(v(\bot) = \mathrm{false}\). Then every instance \(\bot \to B\) of ex falso, that is every axiom of intuitionistic propositional logic, is true under \(v\).

theorem evalBool_of_mem_ipl (hv : v ⊥ = false) {A : Proposition Atom}
    (hA : A ∈ IPL Atom) : A.evalBool v = true
Uses 1 · Used by 1
Statement usesTruth-table evaluation
Used byIntuitionistic derivability implies truth under valuations with false falsum

TheoremDouble-negation elimination is true when falsum is false#✓fully proved

Suppose the atoms include a distinguished atom \(\bot\), and let \(v\) be a Boolean valuation of the atoms with \(v(\bot) = \mathrm{false}\). Then every instance \(\neg\neg B \to B\) of double-negation elimination, that is every axiom of classical propositional logic, is true under \(v\).

theorem evalBool_of_mem_cpl (hv : v ⊥ = false) {A : Proposition Atom}
    (hA : A ∈ CPL Atom) : A.evalBool v = true
Uses 1 · Used by 2
Statement usesTruth-table evaluation
Used byCompleteness for truth tables · Classical derivability implies truth under valuations with false falsum

TheoremClassical derivability implies truth under valuations with false falsum#✓fully proved

Suppose the atoms include a distinguished atom \(\bot\), and let \(v\) be a Boolean valuation of the atoms with \(v(\bot) = \mathrm{false}\). If the sequent \(\Gamma \vdash A\) is derivable in classical propositional logic (natural deduction whose axioms are all instances \(\neg\neg B \to B\) of double-negation elimination) and every member of \(\Gamma\) is true under \(v\), then \(A\) is true under \(v\).

theorem DerivableIn.evalBool_of_cpl {Γ : Ctx Atom} {A : Proposition Atom}
    (h : DerivableIn (CPL Atom) (Γ ⊢ A)) (hv : v ⊥ = false)
    (hΓ : ∀ B ∈ Γ, B.evalBool v = true) : A.evalBool v = true
Uses 3 · Used by 3
Statement usesTruth-table evaluation
Proof usesTruth-table soundness of derivability · Double-negation elimination is true when falsum is false
Used byCompactness · Classical logic proves no atom · Consistency of classical propositional logic

TheoremIntuitionistic derivability implies truth under valuations with false falsum#✓fully proved

Suppose the atoms include a distinguished atom \(\bot\), and let \(v\) be a Boolean valuation of the atoms with \(v(\bot) = \mathrm{false}\). If the sequent \(\Gamma \vdash A\) is derivable in intuitionistic propositional logic (natural deduction whose axioms are all instances \(\bot \to B\) of ex falso) and every member of \(\Gamma\) is true under \(v\), then \(A\) is true under \(v\).

theorem DerivableIn.evalBool_of_ipl {Γ : Ctx Atom} {A : Proposition Atom}
    (h : DerivableIn (IPL Atom) (Γ ⊢ A)) (hv : v ⊥ = false)
    (hΓ : ∀ B ∈ Γ, B.evalBool v = true) : A.evalBool v = true
Uses 3
Statement usesTruth-table evaluation
Proof usesTruth-table soundness of derivability · Ex falso is true when falsum is false

TheoremConsistency of classical propositional logic#✓fully proved

For every type of atoms with a designated atom \(\bot\), the proposition \(\bot\) is not derivable from the empty context in natural deduction over the classical theory, whose axioms are all instances \(\neg\neg A \to A\) of double-negation elimination, where \(\neg A\) abbreviates \(A \to \bot\).

theorem not_derivableIn_cpl_bot : ¬ DerivableIn (CPL Atom) (⊥ : Proposition Atom)
Uses 2
Proof usesClassical derivability implies truth under valuations with false falsum · Truth-table evaluation

TheoremClassical logic proves no atom#✓fully proved

Suppose the atoms include a distinguished atom \(\bot\). For every atom \(x\), including \(\bot\), the proposition \(x\) is not derivable from the empty context in classical propositional logic (natural deduction whose axioms are all instances \(\neg\neg B \to B\) of double-negation elimination).

theorem not_derivableIn_cpl_atom (x : Atom) :
    ¬ DerivableIn (CPL Atom) (atom x : Proposition Atom)
Uses 2
Proof usesClassical derivability implies truth under valuations with false falsum · Truth-table evaluation

DefinitionSatisfiable sets of propositions#✓fully proved

A set \(S\) of propositions is satisfiable when some Boolean valuation \(v\) of the atoms with \(v(\bot) = \mathrm{false}\) makes every member of \(S\) true.

def BoolSatisfiable [Bot Atom] (S : Set (Proposition Atom)) : Prop :=
  ∃ v : Atom → Bool, v ⊥ = false ∧ ∀ A ∈ S, A.evalBool v = true
Uses 1 · Used by 3
Statement usesTruth-table evaluation
Used byModel existence for propositional natural deduction · Compactness · Strong completeness of classical propositional natural deduction

DefinitionConsistency relative to a theory#✓fully proved

Let \(T\) be a theory, that is, a set of propositions. A set \(S\) of propositions is consistent relative to \(T\) when there is no finite set \(\Gamma \subseteq S\) such that the sequent \(\Gamma \vdash \bot\) is derivable in natural deduction from \(T\).

def Theory.ConsistentWith (T : Theory Atom) (S : Set (Proposition Atom)) : Prop :=
  ∀ Γ : Ctx Atom, (Γ : Set (Proposition Atom)) ⊆ S → ¬ DerivableIn T (Γ ⊢ ⊥)
Used by 9
Used byModel existence for propositional natural deduction · Compactness · Strong completeness of classical propositional natural deduction · Truth lemma for propositional natural deduction · Lindenbaum's lemma for propositional natural deduction · Propositions outside a maximal consistent set are refuted by it · Maximal consistent sets are deductively closed in propositional natural deduction · Each proposition or its negation lies in a maximal consistent set · A maximal consistent set contains its theory

TheoremLindenbaum's lemma for propositional natural deduction#✓fully proved

Let \(T\) be a theory. Every set \(S\) of propositions that is consistent relative to \(T\) is contained in a set \(M\) that is consistent relative to \(T\) and not properly contained in any other set consistent relative to \(T\).

theorem Theory.exists_maximal_consistentWith {S : Set (Proposition Atom)}
    (hS : T.ConsistentWith S) : ∃ M, S ⊆ M ∧ Maximal T.ConsistentWith M
Uses 1 · Used by 1
Statement usesConsistency relative to a theory
Used byModel existence for propositional natural deduction

TheoremPropositions outside a maximal consistent set are refuted by it#✓fully proved

Let \(T\) be a theory and \(M\) a maximal set of propositions consistent relative to \(T\). If a proposition \(A\) is not in \(M\), then there is a finite set \(\Gamma \subseteq M\) such that the sequent \(\Gamma \cup \{A\} \vdash \bot\) is derivable in natural deduction from \(T\).

theorem exists_refutation {A : Proposition Atom} (hA : A ∉ M) :
    ∃ Γ : Ctx Atom, (Γ : Set (Proposition Atom)) ⊆ M ∧ DerivableIn T (insert A Γ ⊢ ⊥)
Uses 1 · Used by 2
Statement usesConsistency relative to a theory
Used byMaximal consistent sets are deductively closed in propositional natural deduction · Each proposition or its negation lies in a maximal consistent set

TheoremMaximal consistent sets are deductively closed in propositional natural deduction#✓fully proved

Let \(T\) be a theory and \(M\) a maximal set of propositions consistent relative to \(T\). If \(\Gamma\) is a finite subset of \(M\) and the sequent \(\Gamma \vdash A\) is derivable in natural deduction from \(T\), then \(A \in M\).

theorem mem_of_derivableIn {Γ : Ctx Atom} {A : Proposition Atom}
    (hΓ : (Γ : Set (Proposition Atom)) ⊆ M) (hder : DerivableIn T (Γ ⊢ A)) : A ∈ M
Uses 2 · Used by 3
Statement usesConsistency relative to a theory
Proof usesPropositions outside a maximal consistent set are refuted by it
Used byTruth lemma for propositional natural deduction · Each proposition or its negation lies in a maximal consistent set · A maximal consistent set contains its theory

TheoremA maximal consistent set contains its theory#✓fully proved

Let \(T\) be a theory and \(M\) a maximal set of propositions consistent relative to \(T\). Then every proposition of \(T\) belongs to \(M\), that is, \(T \subseteq M\).

theorem subset_theory : T ⊆ M
Uses 2 · Used by 1
Statement usesConsistency relative to a theory
Proof usesMaximal consistent sets are deductively closed in propositional natural deduction
Used byModel existence for propositional natural deduction

TheoremEach proposition or its negation lies in a maximal consistent set#✓fully proved

Let \(T\) be a theory and \(M\) a maximal set of propositions consistent relative to \(T\). Then for every proposition \(A\), either \(A \in M\) or \(\neg A \in M\), where \(\neg A\) is the proposition \(A \to \bot\).

theorem mem_or_neg_mem (A : Proposition Atom) : A ∈ M ∨ (¬A : Proposition Atom) ∈ M
Uses 3 · Used by 1
Statement usesConsistency relative to a theory
Proof usesPropositions outside a maximal consistent set are refuted by it · Maximal consistent sets are deductively closed in propositional natural deduction
Used byTruth lemma for propositional natural deduction

TheoremTruth lemma for propositional natural deduction#✓fully proved

Let \(T\) be an intuitionistic theory, that is, one that derives \(\bot \to B\) for every proposition \(B\). Let \(M\) be a set of propositions that is consistent relative to \(T\) and not properly contained in any other set consistent relative to \(T\), and let \(v_M\) be the valuation that makes an atom \(x\) true exactly when the atomic proposition \(x\) belongs to \(M\). Then a proposition \(A\) evaluates to true under \(v_M\) iff \(A \in M\).

theorem evalBool_eq_true_iff [IsIntuitionistic Atom T] (A : Proposition Atom) :
    A.evalBool (fun x ↦ @decide (atom x ∈ M) (Classical.dec _)) = true ↔ A ∈ M
Uses 4 · Used by 1
Statement usesTruth-table evaluation · Consistency relative to a theory
Proof usesMaximal consistent sets are deductively closed in propositional natural deduction · Each proposition or its negation lies in a maximal consistent set
Used byModel existence for propositional natural deduction

TheoremModel existence for propositional natural deduction#✓fully proved

Let \(T\) be an intuitionistic theory, that is, one that derives \(\bot \to B\) for every proposition \(B\). If a set \(S\) of propositions is consistent relative to \(T\), then \(T \cup S\) is satisfiable: some Boolean valuation \(v\) of the atoms with \(v(\bot) = \mathrm{false}\) makes every member of \(T\) and every member of \(S\) true.

theorem Theory.ConsistentWith.boolSatisfiable [IsIntuitionistic Atom T]
    {S : Set (Proposition Atom)} (hS : T.ConsistentWith S) : BoolSatisfiable (T ∪ S)
Uses 6 · Used by 2
Statement usesSatisfiable sets of propositions · Consistency relative to a theory
Proof usesTruth lemma for propositional natural deduction · A maximal consistent set contains its theory · Truth-table evaluation · Lindenbaum's lemma for propositional natural deduction
Used byCompactness · Strong completeness of classical propositional natural deduction

TheoremStrong completeness of classical propositional natural deduction#✓fully proved

Let \(T\) be a classical theory, that is, one that derives \(\neg\neg B \to B\) for every proposition \(B\), where \(\neg B\) abbreviates \(B \to \bot\). Let \(\Gamma\) be a finite set of propositions and \(A\) a proposition. If every Boolean valuation \(v\) of the atoms with \(v(\bot) = \mathrm{false}\) that makes every member of \(T\) and every member of \(\Gamma\) true also makes \(A\) true, then the sequent \(\Gamma \vdash A\) is derivable from \(T\).

theorem Theory.derivableIn_of_forall_evalBool [IsClassical Atom T] {Γ : Ctx Atom}
    {A : Proposition Atom}
    (h : ∀ v : Atom → Bool, v ⊥ = false → (∀ B ∈ T, B.evalBool v = true) →
      (∀ B ∈ Γ, B.evalBool v = true) → A.evalBool v = true) :
    DerivableIn T (Γ ⊢ A)
Uses 5 · Used by 2
Statement usesTruth-table evaluation
Proof usesSatisfiable sets of propositions · Truth value of a negation · Consistency relative to a theory · Model existence for propositional natural deduction
Used bySoundness and completeness for classical theories · Soundness and completeness for classical theories, with ⊥ false

TheoremSoundness and completeness for classical theories, with ⊥ false#✓fully proved

Let \(T\) be a classical theory, that is, one that derives \(\neg\neg B \to B\) for every proposition \(B\), where \(\neg B\) abbreviates \(B \to \bot\). For every finite set \(\Gamma\) of propositions and every proposition \(A\), the sequent \(\Gamma \vdash A\) is derivable from \(T\) iff every Boolean valuation \(v\) of the atoms with \(v(\bot) = \mathrm{false}\) that makes every member of \(T\) and every member of \(\Gamma\) true also makes \(A\) true.

theorem Theory.derivableIn_iff_forall_evalBool [IsClassical Atom T] {Γ : Ctx Atom}
    {A : Proposition Atom} :
    DerivableIn T (Γ ⊢ A) ↔ ∀ v : Atom → Bool, v ⊥ = false →
      (∀ B ∈ T, B.evalBool v = true) → (∀ B ∈ Γ, B.evalBool v = true) → A.evalBool v = true
Uses 3 · Used by 1
Statement usesTruth-table evaluation
Proof usesTruth-table soundness of derivability · Strong completeness of classical propositional natural deduction
Used byCompleteness for truth tables

TheoremSoundness and completeness for classical theories#✓fully proved

Let \(T\) be a classical theory, that is, one that derives \(\neg\neg B \to B\) for every proposition \(B\), where \(\neg B\) abbreviates \(B \to \bot\). For every finite set \(\Gamma\) of propositions and every proposition \(A\), the sequent \(\Gamma \vdash A\) is derivable from \(T\) iff every Boolean valuation of the atoms that makes every member of \(T\) and every member of \(\Gamma\) true also makes \(A\) true.

Here \(\bot\) is a distinguished atom, and these valuations may make it true or false.

theorem Theory.derivableIn_iff_boolEntails [IsClassical Atom T] {Γ : Ctx Atom}
    {A : Proposition Atom} : DerivableIn T (Γ ⊢ A) ↔ T.BoolEntails Γ A
Uses 3
Statement usesTruth-table consequence
Proof usesTruth-table soundness of derivability · Strong completeness of classical propositional natural deduction

TheoremCompleteness for truth tables#✓fully proved

Let \(\Gamma\) be a finite set of propositions and \(A\) a proposition. The sequent \(\Gamma \vdash A\) is derivable in classical propositional logic (natural deduction with every instance of \(\neg\neg B \to B\) as an axiom, where \(\neg B\) abbreviates \(B \to \bot\)) iff every Boolean valuation \(v\) of the atoms with \(v(\bot) = \mathrm{false}\) that makes every member of \(\Gamma\) true also makes \(A\) true.

theorem derivableIn_cpl_iff {Γ : Ctx Atom} {A : Proposition Atom} :
    DerivableIn (CPL Atom) (Γ ⊢ A) ↔
      ∀ v : Atom → Bool, v ⊥ = false → (∀ B ∈ Γ, B.evalBool v = true) →
        A.evalBool v = true
Uses 3 · Used by 2
Statement usesTruth-table evaluation
Proof usesSoundness and completeness for classical theories, with ⊥ false · Double-negation elimination is true when falsum is false
Used byCraig interpolation for classical natural deduction · The translation into \(\to\) and \(\bot\) preserves and reflects classical derivability

TheoremCompactness#✓fully proved

A set of propositions is satisfiable, with ⊥ false, iff each of its finite subsets is.

theorem boolSatisfiable_iff_forall_finset {S : Set (Proposition Atom)} :
    BoolSatisfiable S ↔
      ∀ F : Finset (Proposition Atom), (F : Set (Proposition Atom)) ⊆ S →
        BoolSatisfiable (F : Set (Proposition Atom))
Uses 5
Statement usesSatisfiable sets of propositions
Proof usesClassical derivability implies truth under valuations with false falsum · Truth-table evaluation · Consistency relative to a theory · Model existence for propositional natural deduction
25 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.