Is determining derivability in propositional logic decidable?

Question

I know that determining (semantic) entailment in propositional logic is decidable by the truth table method. For instance, let:

$\phi = b \rightarrow a \\ \psi = b \lor c \rightarrow a$

Then we can use the truth table method to determine whether $\phi$ entails $\sigma$, which is this case is true.

We can also (syntactically) derive $\psi$ from $\phi$, for instance by using natural deduction. However, is determining derivability decidable in propositional logic?

Answer 1

For systems that are both sound and complete (which for propositional logic is pretty much any system, that's out there ... it would be embarrassing for a logician to propose a proof system for propositional logic that would be not be both sound and complete), this is trivial: we would have $\Gamma \vdash \phi$ iff $\Gamma \vDash \phi$, and since the latter is decidable, the former is decidable as well.

If a proof system is not both sound and complete .... well, if a system is not sound and is in fact able to derive any statement from nothing, then derivability is also trivially decidable: everything is derivable!

For other systems yet ... Hmmm, I am actually unsure of the answer ... though I wonder if you could have some kind of bizarre propositional logic with which you can encode claims about Turing-machines and their behavior, and thus generate some kind of undecidability result ...