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?

  • $\begingroup$ 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. $\endgroup$ – Mauro ALLEGRANZA Jul 4 '14 at 19:47
  • $\begingroup$ Finding a counterexample proves its negation, not its undecidability. You have to prove its undecidability outside the system. $\endgroup$ – 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;


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.

  • 1
    $\begingroup$ @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. $\endgroup$ – UserB1234 Jul 4 '14 at 19:24
  • $\begingroup$ 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$ ? $\endgroup$ – dezakin Jul 4 '14 at 19:39
  • $\begingroup$ @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. $\endgroup$ – UserB1234 Jul 4 '14 at 19:47
  • $\begingroup$ 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. $\endgroup$ – dezakin Jul 4 '14 at 20:01
  • $\begingroup$ I already asked about mechanizing forcing a while ago; Apparently its awfully domain specific and difficult to mechanize. math.stackexchange.com/questions/476924/… $\endgroup$ – dezakin Jul 4 '14 at 20:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.