Decision procedure for completeness for CPC with arbitrary natural deduction rules

103 Views Asked by At

I'm wondering if there's an algorithmic way of determining whether a particular set of Natural Deduction-style rules is complete for classical propositional logic.

Two examples - you would use the procedure to verify that the following set of rules is complete for classical logic with $\{ \wedge , \uparrow, \bot \} $, but that none of its proper subsets is complete:

$\begin{array}{c} [\phi \uparrow \psi ] \\ \vdots \\ \bot \\ \hline \phi \end{array}$ $\begin{array}{c} [\phi \uparrow \psi ] \\ \vdots \\ \bot \\ \hline \psi \end{array}$ $\begin{array}{c} \phi \hspace{2em} \psi \\ \hline \phi \wedge \psi \end{array}$ $\begin{array}{c} \phi \wedge \psi \hspace{1em} \phi \uparrow \psi \\ \hline \bot \end{array}$

Similarly you would verify that the following set is complete for classical logic with $ \{ \to , \neg , \bot \} $, but no proper subset is:

$\begin{array}{c} [\phi] \\ \vdots \\ \psi \\ \hline \phi \to \psi \end{array}$ $\begin{array}{c} [\neg \phi] \\ \vdots \\ \bot \\ \hline \phi \end{array}$ $\begin{array}{c} \phi \hspace{1em} \neg \psi \hspace{1em} \phi \to \psi \\ \hline \bot \end{array}$

My motivation for asking this: I'm hoping to make a computer program that spits out random Natural Deduction problems for classical propositional logic, but where not just the premises and conclusions are randomised but the rules you're allowed to use are randomised as well. For this, a computer program would need to know if the random rules it's giving you are a complete set of rules.