$$ 1) \forall z \ C(z,y) \ → B(t) \iff \forall z \ ( C(z,y) → B(t)) $$ $$ 2) \forall z \forall u \ (\forall x \ A(x,u) → \forall x \ B(x,z)) \iff \forall x \forall u \ A(x,u) → \forall z \forall x \ B(x,z) $$ $$ 3) ¬ \exists x \ P(x) \iff \forall x \ ¬P(x) $$ $$ 4) \exists x \ P(x) \& \exists y \ B(y) \iff \exists y \ (\exists x \ P(x) \& B(y)) $$ Is it right that to check whether an equivalence is wrong or not, I have to prove that both $A→B$ and $B→ A$ holds or not.
According to my attempt of solving this problem the wrong one is $2$, but I'm not sure, as I'm new to first-order logic.
For the second one I've got: $$ \underline{ ∀x∀u A(x,u)→∀z∀x B(x,z) , ⊢ ∀z∀u (∀x A(x,u)→∀x B(x,z)) }$$ $$ \underline{ \forall z \forall x \ B(x,z), ⊢ ∀z∀u (∀x A(x,u)→∀x B(x,z)) , ⊢ \forall x \forall u A(x,u) } $$ $$ \underline{ \forall z \forall x \ B(x,z), ⊢ \forall x \ A(x,t) → \forall x \ B(x,r), ⊢ \forall x \forall u \ A(x,u) } $$ $$ \underline{ \forall z \forall x \ B(x,z), ⊢ \forall x \ B(x,r), ...} $$ $$ \underline{ B(p,q), ⊢ \forall x B(x,r) } $$ $$ B(p,q), ⊢ B(p,r) \ $$

  • 2
    $\begingroup$ According to what attempt? It is difficult to check something that isn't shown. $\endgroup$ Jul 27 '18 at 22:05
  • $\begingroup$ I think you should consider what distributes and what does not. $\endgroup$
    – smokeypeat
    Jul 28 '18 at 12:13

Note, that since FOL is undecidable, there is no general way of answering such questions. In other words, the fact that you couldn't prove some formula does not entail that it is unprovable. Or, in yet other and more technically correct words, there are some unprovable first order formulas for which no counter model can be constructed effectively. Fortunately, this is not the case in your task.

Now, we want to "check" whether some of the following formulas are valid. For this task it is better to use analytic tableaux (there are many kinds of tableau calculi, so you may choose whichever you like the most) which are in fact means for constructing models. Putting a formula "into" a tableau and applying rules to it until no more are applicable yields either of the three following answers:

  • formula is invalid (i.e. we failed to construct its model);
  • formula is satisfiable (i.e. we constructed its model);
  • the tableau does not end (we have come to neither of the previeous two conclusions because there is still and will always be a way to implement a rule, i.e. "until no more are applicable" is not the case).

Indeed, if you run the second formula through your tableaux caclulus of choice, you'll see that your tableau might not end (at least, it does not end in the version I've been taught).

But this alone does not prove that the fomula is falsifiable. What does, then? A countermodel does! So, let us build one.

Assume, our universe consists of five objects: $a$, $b$, $c$, $d$ and $e$ such that $\forall x A(x,b)$, $\neg A(c,e)$ and $\neg B(d,a)$. Under this interpretation LHS is false (think, why) but RHS is true (again, think, why).

All other formulas can be easily proved in either a Hilbert style calculus or again using tableaux method.


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