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$?

  • $\begingroup$ @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). $\endgroup$
    – l_frost
    Apr 17 at 0:24
  • $\begingroup$ 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 $\endgroup$
    – Matt F.
    Apr 17 at 0:38
  • $\begingroup$ 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. $\endgroup$ Apr 18 at 8:07
  • $\begingroup$ @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? $\endgroup$
    – l_frost
    Apr 19 at 0:06
  • 1
    $\begingroup$ 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. $\endgroup$ Apr 19 at 9:41

1 Answer 1


It is undecidable, because it is even undecidable to recognize whether a finite set of axioms together with the rule of modus ponens axiomatizes exactly classical propositional logic by the Post-Linial theorem. This was shown in 1948 by Linial and Post, see their announcement (p. 50), but the first published proof is by Yntema. There are many similar results for other propositional logics.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.