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



Decidability of completeness in propositional logic
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)](https://www.ams.org/journals/bull/1949-55-01/S0002-9904-1949-09162-0/S0002-9904-1949-09162-0.pdf), but the first published [proof](https://doi.org/10.1305/ndjfl/1093957737) is by Yntema. There are many similar results for other propositional logics.


