# Is completeness of a propositional axiom set decidable?

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.

• The case of classical PL with $\{\to, \lnot\}$, the usual axioms schemas, and modus ponens is decidable, e.g., by the truth table method: en.wikipedia.org/wiki/Truth_table . It is not clear to me what you are asking in the other parts of the question. Aug 18, 2017 at 21:04
• @orient: The question is, if I understand it correctly, whether a given set of logical axioms are sufficient to prove every propositional tautology. Aug 18, 2017 at 21:20
• @orient He is asking about what happens when you discard the usual axioms and use other axioms instead. Aug 18, 2017 at 21:22
• Yes, @DanielV got it right: I want a function from set-of-axiom-schemas to bool which evaluates to true iff every tautology is provable using only axioms from the given schema. Henning's comment makes sounds like I want the value of this function at a particular axiom schema, which is different from what I want, but his answer demonstrates that he understood my question (by answering it in the negative: no such function exists—or rather, it's not computable by a Turing machine). Aug 18, 2017 at 21:30
• As for the added paragraph, I think it will be hard to narrow down the class of systems so much chat my construction cannot be shoehorned into it -- except by being so restrictive that there's only room for finitely many different systems to test. For example, a variant of my construction would encode a Turing machine as a system with only three axioms each of which with no more than three different variables. (One of these axioms would be very long, basically a conjunction of everything we need, and the two others would just provide machinery for taking the conjunction apart). Aug 18, 2017 at 21:55

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.

• Well done! Some undecidable tar-pit monster will definitely make a concrete construction nicer. I guess the same technique can show soundness to be undecidable: have the axiom $\lnot\lnot(\cdots \to (A \to A)) \to \bot$ for all undecidable outcomes (halting states) $\cdots$, where $\bot = \lnot (A \to A)$, or your favorite falsum under some other choice of connectives. This shows unsoundness to be at most semi-decidable; it's clearly also at least semi-decidable: search for a provable non-tautology, win when you find one. Is completeness decidable for interesting restricted axiom sets? Aug 18, 2017 at 21:49
• @JonasKölker Can't you just determine soundness with truth tables? Aug 18, 2017 at 21:53
• @JonasKölker: That won't work as written: $\neg\neg(\cdots\to(A\to A))\to\bot$ is in itself a contradiction, so having it as an axiom would certainly be unsound. You could make it an inference rule instead of an axiom, though: From $\neg\neg(\cdots\to(A\to A))$ infer $B$. Aug 18, 2017 at 22:02
• @DanielV, I shouldn't try to compute late at night. Yes, one can check soundness of the axioms. One can also check the soundness of inference rules, but one cannot check (as Henning Makholm indicates) whether a given inference rule can never be applied—and soundness can be made dependent on a given rule never applying. Aug 19, 2017 at 10:50
• @DanielV There is no particular truth table which shows that the rule of uniform substitution preserves validity. Aug 19, 2017 at 17:45