# Decision procedure for completeness for CPC with arbitrary natural deduction rules

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.

• Interesting question! How are you planning to represent and generate the rules? If you are just picking the standard introduction and elimination rules for each of a given set of connectives, then I think you just need the rules for the connectives used in the problem. But I suspect you may have something different in mind. – Rob Arthan Jan 16 '16 at 18:57
• @RobArthan - As you suspect, I'm hoping to work with more than just the standard introduction/elimination rules, but also impure rules which involve more than one connective (for example: inferring "P nor Q" from falsum, discharging "P or Q"; or inferring "P implies Q" from "Q and R"). I haven't totally figured out how the rules will be generated - I'd probably tinker with the random generation lots so that it makes the most fun problems. – Carralpha Jan 16 '16 at 19:34
• According to arxiv.org/abs/1407.7010 (which also gives references to earlier work on this), recognizing Hilbert-style axiomatizations of propositional logic is undecidable. I think this will lead to a negative answer to your question in general. – Rob Arthan Jan 16 '16 at 21:55
• @RobArthan - Thank you very much for pointing this out! I will go back to the drawing board and see if I can find another way of generating the rules which lets completeness be more easily verified (which might mean sticking a lot closer to classic introduction/elimination). – Carralpha Jan 17 '16 at 18:09