Documentation

This algorithm turns a judgement \(g \vdash a\) in full propositional logic into a judgement \(g^* \vdash a^*\) in just the implicational fragment of propositional logic such that \(g \vdash a\) is provable if and only if the judgement \(g^* \vdash a^*\) is provable. The latter judgement's provability can then be checked using proveImp.

The transformation from \(g \vdash a\) to \(g^* \vdash a^*\) involves two steps:

1. For each propositional formula \(b\), introduce a new propositional variable \(x_b\). Take \(a^* = x_a\).

2. Construct the set \(g^*\) as follows.

   1. For each formula \(b \in g\), add \(x_b\) to \(g^*\).
   2. (Truth) Add \(x_\top\) to \(g^*\).

   3. For each subformula \(b\) of either \(a\) or a formula in \(g\), do the following.

      1. (Falsity elimination and truth introduction) Add the following formulas to \(g^*\). \[ \begin{gathered} x_\bot \rightarrow x_b \\ x_b \rightarrow x_\top \end{gathered} \]
      2. (Negation introduction and elimination) If \(b = \lnot c\), then add the following formulas to \(g^*\). \[ \begin{gathered} (x_c \rightarrow x_\bot) \rightarrow x_{\lnot c} \\ x_{\lnot c} \rightarrow (x_c \rightarrow x_\bot) \end{gathered} \]
      3. (Implication introduction and elimination) If \(b = c \rightarrow d\), then add the following formulas to \(g^*\). \[ \begin{gathered} (x_c \rightarrow x_d) \rightarrow x_{c \rightarrow d} \\ x_{c \rightarrow d} \rightarrow (x_c \rightarrow x_d) \end{gathered} \]
      4. (Disjunction introduction and elimination) If \(b = c \lor d\), then for each additional subformula \(e\) of \(a\), add the following formulas to \(g^*\). \[ \begin{gathered} x_c \rightarrow x_{c \lor d} \\ x_d \rightarrow x_{c \lor d} \\ x_{c \lor d} \rightarrow ((x_c \rightarrow x_e) \rightarrow ((x_d \rightarrow x_e) \rightarrow x_e)) \end{gathered} \]
      5. (Conjunction introduction and elimination) If \(b = c \land d\), then add the following formulas to \(g^*\). \[ \begin{gathered} x_c \rightarrow (x_d \rightarrow x_{c \land d}) \\ x_{c \land d} \rightarrow x_c \\ x_{c \land d} \rightarrow x_d \end{gathered} \]
      6. (Equivalence introduction and elimination) If \(b = c \leftrightarrow d\), then add the following formulas to \(g^*\). \[ \begin{gathered} (x_c \rightarrow x_d) \rightarrow ((x_d \rightarrow x_c) \rightarrow x_{c \leftrightarrow d}) \\ x_{c \leftrightarrow d} \rightarrow (x_c \rightarrow x_d) \\ x_{c \leftrightarrow d} \rightarrow (x_d \rightarrow x_c) \end{gathered} \]