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:

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?

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

6more comments