# Decidability of completeness in propositional logic

Propositional logic can be presented as in Mendelson’s book, with the sole inference rule of modus ponens, and with the following three axioms: $$B \Rightarrow (C \Rightarrow B)$$ $$(B \Rightarrow (C \Rightarrow D)) \Rightarrow ((B \Rightarrow C) \Rightarrow (B \Rightarrow D))$$ $$((\neg C) \Rightarrow (\neg B)) \Rightarrow (((\neg C) \Rightarrow B) \Rightarrow C)$$ This is a sound and complete theory, as are several other theories for propositional logic.

I have questions about similar theories for propositional logic:

1. Given a complete set of logical connectives and a finite set of sound axioms and inference rules, can we algorithmically determine if the resulting theory is complete?

2. Given a finite set of axioms and inference rules $$X$$ (not necessarily sound) and a formula $$\alpha$$ in the underlying language of propositional connectives, can we algorithmically determine if $$\alpha$$ can be derived from $$X$$?

• @MattF. I wish to allow arbitrary substitutions of formulas in for the variables (which means there are say infinitely many proofs of a given length). In the case of say $L$ above, this would always yield tautologies, whereas with an arbitrary $X$, we will just get a whole bunch of formulas (many of which are not tautologies if the original axioms/inference rules aren't sound). Apr 17 at 0:24
• This question seems most interesting for logics with infinitely many distinct sentences — like intuitionist propositional logic with the Rieger-Nishimura lattice: en.wikipedia.org/wiki/Intuitionistic_logic#Syntax Apr 17 at 0:38
• Q2 is undecidable, as one can take for $X$ an axiomatization of an undecidable propositional logic such as one of the relevance logics considered by Urquhart: The undecidability of entailment and relevant implication. Q1 is most likely undecidable as well, but this requires a different argument. Apr 18 at 8:07
• @EmilJeřábek Thank you - that reference is very helpful! Do you happen to know if any of these undecidable propositional logics every have the property that for a fixed formula $A$ and positive integer $k$, we can determine if there is a proof of $A$ in $k$ steps? Apr 19 at 0:06
• It was shown already by Post and Linial that the question whether a set of propositional formulae together with the rule of modus ponens axiomatizes exactly the classical propositional logic is algorithmically undecidable. Apr 19 at 9:41