# What are techniques for proving undecidability or unprovability of a sentence?

I asked a question the other day on how to form logical equivalence between a sentence $\phi$ and two other sentences $\psi$ and $\chi$, such that neither $\psi$ nor $\chi$ were on their own as 'strong' as $\phi$. Eventually the answer was provided in the form:

$\vdash\phi\leftrightarrow{(\psi\wedge\chi)}$, and $\not\vdash\chi\rightarrow{\phi}$ and $\not\vdash\psi\rightarrow{\phi}$

Now, I know how to prove provability of the first part semidecidably. I can prove $\vdash\phi\leftrightarrow{(\psi\wedge\chi)}$ by just following proof calculus if $\phi\leftrightarrow{(\psi\wedge\chi)}$ is a decidable sentence. I expect that $\not\vdash\chi\rightarrow{\phi}$ or generally $\not\vdash\phi$ can't be proved for the general case, because then it would seem that would solve the halting problem. But there are methods to prove $\not\vdash\phi$ for specific sentences $\phi$ (or in specific models of a specific theory?) or we wouldn't have independence proofs.

What are some techniques that are used to prove a sentence is undecidable and is there any way to prove $\vdash\phi\leftrightarrow{(\psi\wedge\chi)}$, $\not\vdash\chi\rightarrow{\phi}$ and $\not\vdash\psi\rightarrow{\phi}$ specifically, at least for some instances or models?

• As you said, first-order logic is undecidable; thus the only way to show unprovability of a formula $\varphi$ is to show that it is not valid; i.e. to find a counterexample. – Mauro ALLEGRANZA Jul 4 '14 at 19:47
• Finding a counterexample proves its negation, not its undecidability. You have to prove its undecidability outside the system. – dezakin Jul 4 '14 at 19:55

You use soundness: Let $L$ be a language and let $T$ be an $L$-theory. Now let $\theta$ be an $L$ sentence. Then;

$T\vdash{\theta}\rightarrow{\forall{M},(M\models{T}\implies{M\models{\theta}})}$

We use this idea:

If you trace through the example I gave here Can a statement in FOL be equivalent to two separate independent statements?; you can see these elements all playing apart.

Let $L=\{\cdot\}$. Let $T=\text{group axioms}\cup \text{there are only twelve distinct elements}$. Now Let $\phi$ say that "I'm is abelian and I'm not cyclic" (i.e. $\forall a,b, a\cdot b = b\cdot a$ and a fairly long sentence that says $\neg{\exists{x}\forall{b}, x=b \lor x^2=b \lor\ldots }$). Then let $\psi$ say that "I'm abelian" and let $\chi$ say that "I'm not cyclic".

Now as you say, $T\vdash\phi\leftrightarrow{(\psi\wedge\chi)}$. But how do we say that and $T\not\vdash\chi\rightarrow{\phi}$ or $T\not\vdash\psi\rightarrow{\phi}$? Well for the first one we would have to show that there is some abelian group with twelve elements that is cyclic, which is easily done by talking about $\mathbb{Z}_{12}$.

But how does this help us? Assume that $T\vdash\chi\rightarrow\phi$. Now all models of $T$ model $\chi\rightarrow\phi$ . However then $(\mathbb{Z}_{12},\cdot)$ models that it is not cyclic. This is a contradiction.

For the second staement we need to show the existence of a group with 12 elements that is not cyclic and is not abelian. For this we can use $A_{4}$.

Edit: To answer the second part of your question, forcing is probably one of the more well known tools for this. But it also has its roots in the above argument.

• @dezakin: My previous answer was kind of misleading. I've fixed it. Also in general, I don't think there is a way. But for the example I gave this is the argument. – UserB1234 Jul 4 '14 at 19:24
• That's helpful... is there any way to implement such a technique for mechanized reasoning? Do I have to model T as a theory in a metatheory to prove these sorts of things? provability seems easier than unprovability as I don't need a metatheory. And is there a reason you use entailment $\vDash$ instead of provability $\vdash$ ? – dezakin Jul 4 '14 at 19:39
• @dezakin: I'm kind of confused by your question. There is always a meta theory in the background lurking around. I'm not a proof theorist, so there might be techniques for what you want but none that I'm aware of. – UserB1234 Jul 4 '14 at 19:47
• I want to write a program that looks at a statement in a particular theory, say the axiom of choice, and look for two sentences that joined together are logically equivalent. Then I want to prove that each sentence is 'weaker' on its own. Apparently I need to find some metatheory for modeling the sentence for the second part. I don't need a metatheory to prove equivalence, just following the proof calculus works. If I could do this with any first order statement, that would be great, but I think that solves the halting problem, so I think I can't do that generally. – dezakin Jul 4 '14 at 20:01
• I already asked about mechanizing forcing a while ago; Apparently its awfully domain specific and difficult to mechanize. math.stackexchange.com/questions/476924/… – dezakin Jul 4 '14 at 20:05