Skip to content

Functional completeness

8 fully proved

Proposition

DefinitionShannon expansion#✓fully proved

Let \(f\) assign a truth value to every valuation of the atoms. The Shannon expansion \(S(\ell, f)\) of \(f\) over a list \(\ell\) of atoms is defined by recursion on \(\ell\). For the empty list it is \(\bot \to \bot\) if \(f\) is true at the valuation that makes every atom false, and \(\bot\) otherwise. For the list \(x \cdot \ell\) with head \(x\) and tail \(\ell\),

\[ S(x \cdot \ell, f) = (x \wedge S(\ell, f_1)) \vee (\neg x \wedge S(\ell, f_0)), \]

where \(\neg x\) is \(x \to \bot\), and \(f_1(v) = f(v[x \mapsto \mathrm{true}])\) and \(f_0(v) = f(v[x \mapsto \mathrm{false}])\), with \(v[x \mapsto b]\) the valuation \(v\) changed at \(x\) to \(b\).

def shannon : List Atom → ((Atom → Bool) → Bool) → Proposition Atom
  | [], f => if f (fun _ ↦ false) then (⊥ → ⊥ : Proposition Atom) else ⊥
  | x :: xs, f =>
    or (and (atom x) (shannon xs fun v ↦ f (Function.update v x true)))
      (and (¬(atom x) : Proposition Atom) (shannon xs fun v ↦ f (Function.update v x false)))
Used by 3
Used byCorrectness of the Shannon expansion · Functional completeness · Functional completeness of → and ⊥

TheoremCorrectness of the Shannon expansion#✓fully proved

Let \(x_1, \dots, x_n\) be a list of atoms and let \(f\) assign a truth value to every valuation of the atoms, such that \(f(v) = f(w)\) whenever \(v\) and \(w\) agree on \(x_1, \dots, x_n\). Then for every valuation \(v\) that makes \(\bot\) false, the Shannon expansion of \(f\) over \(x_1, \dots, x_n\) has truth value \(f(v)\) under \(v\).

theorem evalBool_shannon {xs : List Atom} {f : (Atom → Bool) → Bool}
    (hf : ∀ v w : Atom → Bool, (∀ a ∈ xs, v a = w a) → f v = f w) {v : Atom → Bool}
    (hv : v ⊥ = false) : (shannon xs f).evalBool v = f v
Uses 3 · Used by 2
Statement usesTruth-table evaluation · Shannon expansion
Proof usesTruth value of a negation
Used byFunctional completeness · Functional completeness of → and ⊥

PL

TheoremFunctional completeness#✓fully proved

Every Boolean function of the atoms in a finite list is the truth table, on valuations with ⊥ false, of some proposition.

theorem exists_evalBool_eq (xs : List Atom) (f : (Atom → Bool) → Bool)
    (hf : ∀ v w : Atom → Bool, (∀ a ∈ xs, v a = w a) → f v = f w) :
    ∃ A : Proposition Atom, ∀ v : Atom → Bool, v ⊥ = false → A.evalBool v = f v
Uses 3
Statement usesTruth-table evaluation
Proof usesCorrectness of the Shannon expansion · Shannon expansion

Proposition

DefinitionPropositions built from \(\to\) and \(\bot\)#✓fully proved

A proposition is built from \(\to\) and \(\bot\) when it contains no conjunction and no disjunction: every atom (including \(\bot\), which is an atom) is, and \(A \to B\) is exactly when both \(A\) and \(B\) are.

def IsImpBot : Proposition Atom → Prop
  | atom _ => True
  | and _ _ => False
  | or _ _ => False
  | imp A B => IsImpBot A ∧ IsImpBot B
Used by 1
Used byFunctional completeness of → and ⊥

DefinitionTranslation into \(\to\) and \(\bot\)#✓fully proved

The translation \(A^*\) of a proposition \(A\) is defined by recursion on \(A\): each atom is unchanged, \((A \to B)^* = A^* \to B^*\), \((A \wedge B)^* = (A^* \to (B^* \to \bot)) \to \bot\) and \((A \vee B)^* = (A^* \to \bot) \to B^*\).

def toImpBot : Proposition Atom → Proposition Atom
  | atom a => atom a
  | and A B => imp (imp (toImpBot A) (imp (toImpBot B) ⊥)) ⊥
  | or A B => imp (imp (toImpBot A) ⊥) (toImpBot B)
  | imp A B => imp (toImpBot A) (toImpBot B)
Used by 3
Used byThe translation into \(\to\) and \(\bot\) preserves and reflects classical derivability · The translation into \(\to\) and \(\bot\) preserves truth values · Functional completeness of → and ⊥

TheoremThe translation into \(\to\) and \(\bot\) preserves truth values#✓fully proved

For every proposition \(A\) and every valuation \(v\) that makes \(\bot\) false, the translation of \(A\) into \(\to\) and \(\bot\) has the same truth value under \(v\) as \(A\).

theorem evalBool_toImpBot (A : Proposition Atom) {v : Atom → Bool} (hv : v ⊥ = false) :
    (toImpBot A).evalBool v = A.evalBool v
Uses 2 · Used by 2
Statement usesTruth-table evaluation · Translation into \(\to\) and \(\bot\)
Used byThe translation into \(\to\) and \(\bot\) preserves and reflects classical derivability · Functional completeness of → and ⊥

PL

TheoremFunctional completeness of → and ⊥#✓fully proved

Every Boolean function of the atoms in a finite list is the truth table, on valuations with ⊥ false, of a proposition built with → alone.

theorem exists_isImpBot_evalBool_eq [DecidableEq Atom] (xs : List Atom) (f : (Atom → Bool) → Bool)
    (hf : ∀ v w : Atom → Bool, (∀ a ∈ xs, v a = w a) → f v = f w) :
    ∃ A : Proposition Atom, A.IsImpBot ∧
      ∀ v : Atom → Bool, v ⊥ = false → A.evalBool v = f v
Uses 6
Statement usesPropositions built from \(\to\) and \(\bot\) · Truth-table evaluation
Proof usesCorrectness of the Shannon expansion · The translation into \(\to\) and \(\bot\) preserves truth values · Shannon expansion · Translation into \(\to\) and \(\bot\)

TheoremThe translation into \(\to\) and \(\bot\) preserves and reflects classical derivability#✓fully proved

For every proposition \(A\), let \(A^*\) be its translation into \(\to\) and \(\bot\), which keeps atoms and implications and recursively replaces each \(B \wedge C\) by \((B \to (C \to \bot)) \to \bot\) and each \(B \vee C\) by \((B \to \bot) \to C\). Then \(A^*\) is derivable from no hypotheses in classical propositional logic if and only if \(A\) is.

theorem derivableIn_cpl_toImpBot_iff [DecidableEq Atom] (A : Proposition Atom) :
    DerivableIn (CPL Atom) A.toImpBot ↔ DerivableIn (CPL Atom) A
Uses 4
Statement usesTranslation into \(\to\) and \(\bot\)
Proof usesTruth-table evaluation · The translation into \(\to\) and \(\bot\) preserves truth values · Completeness for truth tables

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.