In propositional logic, given a set of logical connectives, axiom schemas and deduction rules, is it decidable whether the logic system is complete?
Is it decidable for the special case of $\{\to, \lnot\}$ and modus ponens?
Is either the general problem or the special case decidable under some reasonable assumptions, such as the axioms being tautologies and closed under uniform substitution? Under some more narrow assumptions, such as a bound on the number of axioms and/or variables in each axiom?
I know that $\{{\bf K}, {\bf S}, (\lnot q \to \lnot p) \to (p \to q)\}$ is complete; doing computer-aided search for other complete sets of axiom schemas would be interesting to me.
No, this cannot be decidable even for the special case of $\{{\to},{\neg}\}$ and modus ponens.
Specifically, if we have a Turing machine and want to know whether it halts on the empty tape, we can construct a set of axioms that are complete if and only if the machine halts.
First we need to devise some way to encode Turing machine configuration (tape and states) as well-formed formulae. This is easily done, because we can completely ignore the meaning of the formulae -- just having some binary connective is enough to represent tree-shaped data.
Then, we can create axioms that allow us to prove $\neg\neg(\sigma\to(A\to A))$ whenever the machine reaches the configuration represented by $\sigma$. Here the $A\to A$ is there to make sure all of these formulas are tautologies, such the system doesn't become unsound no matter what the machine does, and wrapping everything in a double negation makes the internal structure of the formula invisible to MP until we unlock more axioms later.
These axioms have the form $$ \neg\neg(\cdots\to(A\to A)) \to \neg\neg(\cdots\to(A\to A)) $$ for each transition of the Turing machine, where the "$\cdots$" parts represent configurations that move to each other in one step. If our representation of configurations is halfway reasonable, we can generalize over the left and right ends of the tape so we can do with one axiom per transition (and probably a few helper axioms to extend the tape representation when we reach the end of it).
Then also have the axioms $$ \neg\neg(\sigma_0\to(A\to A)) $$ where $\sigma_0$ is a description of the initial configuration, as well as $$ \neg\neg(\cdots\to(A\to A)) \to \mathbf K \\ \neg\neg(\cdots\to(A\to A)) \to \mathbf S \\ \neg\neg(\cdots\to(A\to A)) \to ((\neg q\to \neg p)\to(p \to q)) $$ where in each of these cases the "$\cdots$" is a pattern that matches a configuration in a terminating state.
(The precise details of the translation would be simplest if we start out with a two-counter machine instead of a Turing machine, but the difference is not really material at the level of abstraction I'm describing here).
On the other hand, if you have modus ponens and all of your axioms and rules of inference are closed under substitution, then completeness will be semi-decidable because such a system is complete iff it proves each of $\mathbf K,\mathbf S,(\neg q\to\neg p)\to(p\to q)$, and you can just start searching for proofs of those.