Skip to content

Craig interpolation

8 fully proved

Proposition

DefinitionAtoms of a proposition#✓fully proved

The atoms of a proposition \(A\) form the finite set of atoms occurring in \(A\): an atom \(x\) has the single atom \(x\), and the atoms of \(B \wedge C\), \(B \vee C\) and \(B \to C\) are the atoms of \(B\) together with the atoms of \(C\).

def atoms : Proposition Atom → Finset Atom
  | atom x => {x}
  | and A B => A.atoms ∪ B.atoms
  | or A B => A.atoms ∪ B.atoms
  | imp A B => A.atoms ∪ B.atoms
Used by 3
Used byThe truth value depends only on the atoms · Craig interpolation, semantic form · Craig interpolation for classical natural deduction

TheoremThe truth value depends only on the atoms#✓fully proved

If two Boolean valuations \(v\) and \(w\) agree on every atom of a proposition \(A\), then \(A\) has the same truth-table value under \(v\) as under \(w\).

theorem evalBool_congr {A : Proposition Atom} {v w : Atom → Bool}
    (h : ∀ x ∈ A.atoms, v x = w x) : A.evalBool v = A.evalBool w
Uses 2 · Used by 1
Statement usesAtoms of a proposition · Truth-table evaluation
Used byCraig interpolation, semantic form

DefinitionSubstituting a truth value for an atom#✓fully proved

For an atom \(p\), a Boolean \(b\) and a proposition \(A\), the proposition \(A[p := b]\) is obtained from \(A\) by replacing every occurrence of the atom \(p\) by the constant \(\top\), written \(\bot \to \bot\), if \(b\) is true, and by \(\bot\) if \(b\) is false.

def fixAtom (p : Atom) (b : Bool) : Proposition Atom → Proposition Atom
  | atom x => if x = p then (if b then (⊥ → ⊥ : Proposition Atom) else ⊥) else atom x
  | and A B => and (fixAtom p b A) (fixAtom p b B)
  | or A B => or (fixAtom p b A) (fixAtom p b B)
  | imp A B => imp (fixAtom p b A) (fixAtom p b B)
Used by 3
Used byBoolean quantification over an atom · Truth of a Boolean quantification over a list of atoms · Craig interpolation, semantic form

DefinitionBoolean quantification over an atom#✓fully proved

For an atom \(p\) and a proposition \(A\), the Boolean quantification \(\exists p.\, A\) is the disjunction \(A[p := \top] \vee A[p := \bot]\), where \(A[p := \top]\) and \(A[p := \bot]\) replace the atom \(p\) in \(A\) by the constant \(\top = (\bot \to \bot)\) and by \(\bot\) respectively.

def elimAtom (p : Atom) (A : Proposition Atom) : Proposition Atom :=
  or (A.fixAtom p true) (A.fixAtom p false)
Uses 1 · Used by 2
Statement usesSubstituting a truth value for an atom
Used byBoolean quantification over a list of atoms · Truth of a Boolean quantification over a list of atoms

DefinitionBoolean quantification over a list of atoms#✓fully proved

For a list of atoms \(p_1, \dots, p_n\) and a proposition \(A\), the iterated Boolean quantification \(\exists p_1 \cdots p_n.\, A\) is \(\exists p_1.\, \exists p_2.\, \cdots \exists p_n.\, A\): \(A\) is quantified over \(p_n\) first and over \(p_1\) last, and for the empty list the result is \(A\) itself.

def elimAtoms : List Atom → Proposition Atom → Proposition Atom
  | [], A => A
  | p :: ps, A => (elimAtoms ps A).elimAtom p
Uses 1 · Used by 2
Statement usesBoolean quantification over an atom
Used byTruth of a Boolean quantification over a list of atoms · Craig interpolation, semantic form

TheoremTruth of a Boolean quantification over a list of atoms#✓fully proved

Let \(p_1, \dots, p_n\) be a list of atoms that does not contain \(\bot\), let \(A\) be a proposition and let \(v\) be a Boolean valuation with \(v(\bot)\) false. Then the iterated Boolean quantification \(\exists p_1 \cdots p_n.\, A\) is true under \(v\) if and only if \(A\) is true under some valuation \(w\) that agrees with \(v\) on every atom not in the list.

theorem evalBool_elimAtoms {ps : List Atom} (hps : ⊥ ∉ ps) (A : Proposition Atom)
    {v : Atom → Bool} (hv : v ⊥ = false) :
    (elimAtoms ps A).evalBool v = true ↔
      ∃ w : Atom → Bool, (∀ x, x ∉ ps → w x = v x) ∧ A.evalBool w = true
Uses 4 · Used by 1
Statement usesBoolean quantification over a list of atoms · Truth-table evaluation
Proof usesBoolean quantification over an atom · Substituting a truth value for an atom
Used byCraig interpolation, semantic form

PL

TheoremCraig interpolation, semantic form#✓fully proved

Let \(A\) and \(B\) be propositions such that every Boolean valuation \(v\) with \(v(\bot)\) false that makes \(A\) true also makes \(B\) true. Then there is a proposition \(I\) whose atoms all lie among the atoms common to \(A\) and \(B\) together with \(\bot\), such that every valuation \(v\) with \(v(\bot)\) false that makes \(A\) true makes \(I\) true, and every valuation \(v\) with \(v(\bot)\) false that makes \(I\) true makes \(B\) true.

theorem exists_interpolant {A B : Proposition Atom}
    (h : ∀ v : Atom → Bool, v ⊥ = false → A.evalBool v = true → B.evalBool v = true) :
    ∃ I : Proposition Atom, I.atoms ⊆ insert ⊥ (A.atoms ∩ B.atoms) ∧
      (∀ v : Atom → Bool, v ⊥ = false → A.evalBool v = true → I.evalBool v = true) ∧
      (∀ v : Atom → Bool, v ⊥ = false → I.evalBool v = true → B.evalBool v = true)
Uses 6 · Used by 1
Statement usesAtoms of a proposition · Truth-table evaluation
Proof usesBoolean quantification over a list of atoms · The truth value depends only on the atoms · Truth of a Boolean quantification over a list of atoms · Substituting a truth value for an atom
Used byCraig interpolation for classical natural deduction

TheoremCraig interpolation for classical natural deduction#✓fully proved

Let \(A\) and \(B\) be propositions such that \(A \to B\) is derivable without assumptions in classical propositional logic \(\mathrm{CPL}\) (natural deduction with the axioms \(\neg\neg C \to C\)). Then there is a proposition \(I\) whose atoms all lie among the atoms common to \(A\) and \(B\) together with \(\bot\), such that \(A \to I\) and \(I \to B\) are both derivable without assumptions in \(\mathrm{CPL}\).

theorem exists_interpolant_cpl {A B : Proposition Atom}
    (h : DerivableIn (CPL Atom) (A → B : Proposition Atom)) :
    ∃ I : Proposition Atom, I.atoms ⊆ insert ⊥ (A.atoms ∩ B.atoms) ∧
      DerivableIn (CPL Atom) (A → I : Proposition Atom) ∧
      DerivableIn (CPL Atom) (I → B : Proposition Atom)
Uses 4
Statement usesAtoms of a proposition
Proof usesTruth-table evaluation · Completeness for truth tables · Craig interpolation, semantic form

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.