# How to do decide a necessary truth for greater formulae complexity than $\Delta_{0}$

How does one determine if a sentence in predicate logic is a theorem? That is to say, for sentences with a greater complexity hierarchy than $\Delta_{0}$, what general methods can I use to decide if a sentence is a necessary truth?

For example consider the following sentence, $$\forall x (P(x) \rightarrow C(x)) \rightarrow \forall x (C(x) \rightarrow P(x))$$

Where $P$ and $C$ are unary relations. What methodology can be used to determine if this sentence is a theorem (provable from no premises, necessary truth, whatever your flavour of terminology is).

Thank you.

-
I assume you used unary predicates because you know that when there is a binary predicate, there is no algorithm. That does not necessarily mean there is no methodology, there are general theorem provers after all. It's just that they do not always work. For unary predicates, a variant of truth tables works universally. – André Nicolas Mar 15 '12 at 7:03

I'm not sure about the answer to this question in higher-order logics, but in first order logic, you can use the Completeness Theorem. In other words, something is provable from the empty theory if and only if it holds in every model of the empty theory. Thus, you can appeal to a semantic argument to show that a sentence is a necessary truth. For example, consider the first-order statement

$((P \to Q) \to P) \to P$

often known as Pierce's law. Proving this directly is unpleasant. However, let us prove it semantically using the above argument.

(1) $P$ is true and $Q$ is true. Then $P \to Q$ is true, and so $(P \to Q) \to P$ is true, and hence $((P \to Q) \to P) \to P)$ is true.

(2) $P$ is true and $Q$ is false. Then $P \to Q$ is false. Then $(P \to Q) \to P$ is true, and hence $((P \to Q) \to P) \to P)$ is true.

(3) $P$ is false. Then $P \to Q$ is true, and so $(P \to Q) \to P$ is false, and hence $((P \to Q) \to P) \to P$ is true.

We have exhausted all possibilities, and in each one, the statement is true. Then the statement holds in every model, and hence every model of the empty theory. By Completeness, it is provable from the empty theory. As my logic professor liked to say, this is the "coward's approach".

-
So, if there are quantifiers we can just pretend they are not there and use the technique you've suggested? – Samuel Reid Mar 15 '12 at 6:49
If it's a first-order statement, the complexity is irrelevant. You can use the above technique and take the quantifiers into account. For example, consider $\forall x \forall y(x = y \vee x \neq y)$. Take any model, and pick any two elements. Then those elements are either equal, or they are not. Thus this statement is true in every model, and hence is provable from the empty theory. – Isaac Solomon Mar 15 '12 at 6:52
@IsaacSolomon: In the presence of quantifiers and predicates other than equality, "take any model" doesn't sound like something that could be used in a decision procedure. The fact that in simple cases you can use this argument is that the model doesn't really matter, you're just tabulating possibilities for isolated propositions or single variables. See the comment by André Nicolas to the original question: with binary predicates there is no decision procedure. – Marc van Leeuwen Mar 15 '12 at 12:50
@MarcvanLeeuwen: I interpreted the question "what general methods can I use" to be a statement about how to approach a homework problem about proving if something is a tautology, rather than a question about whether the set of tautologies is recursive, or efficiently computable. – Isaac Solomon Mar 15 '12 at 14:32
@IsaacSolomon: OK, I see. The question is not very clear on this indeed. – Marc van Leeuwen Mar 15 '12 at 17:59

There is no decision procedure for predicate logic. If there where (and the procedure would have some measure of efficiency), then mathematics would have a lot fewer open problems. This is because every statement in a theory that can be formulated in first order language is equivalent to a formula of first order predicate logic, which has the form of an implication with the conjunction of all the axioms of the theory as its left (hypothesis) part.

There exists a semi-decision procedure though, one that will tell you when a given formula is a theorem (but it won't tell you anything if it's not). In some sense this may seem good enough, since for formulas that are not theorems, nor are their negation (so that they could equally well be true or flase), who cares? However this semi-decision procedure simply consists of searching for a deduction of the formula, which will (tautologically) exist if it is provable. This is so extremely inefficient a method for proving theorems however that it is of no practical use.

-