How do I check if these expressions are equivalent?

  • ∀a,b [P(a) ∧ ¬R(a) ∧ S(b)] → G(a,b)

  • ∀a [(P(a) ∧ ¬R(a)) → (∀b [S(b) → G(a,b)])]

  • 1
    Do you now how to check equivalence of formulas in general? If yes, where exactly do you get stuck applying it to the example in question? If not, did you make sure you understood the definition of logical equivalence on your textbook and went through some examples? If not, clarifying what logical equivalence means is where to start, afterwards you can go about applying it to this exercise. Aug 13, 2019 at 12:25

2 Answers 2


Expressions are equivalent if they can be related with an if and only if connection.

One way to check if they are equivalent is to use a tree proof generator. Putting these expressions into such a tool will also require one to write a well-formed formula eliminating any ambiguity.

Here is the result of the tool showing that the expressions are equivalent as I entered them:

enter image description here

A tree proof attempts to prove the result by negating it, transform the negated statement using equivalences and explore all available branches. If one of the branches did not lead to an "x", a contradiction, then that branch could be used to form a countermodel. In this case all branches closed. No contradiction was found and so the original equivalence was valid.

Another way to check that the two statements are equivalent is to find a natural deduction proof of the equivalence.

Tree Proof Generator. https://www.umsu.de/logik/trees/

  • 1
    Could you explain (a) what each line of the "tree proof generator" shows (b) why the branch must lead to "x" and (c) what ambiguity there was in the original statement that needs to be eliminated. So far, this answer is basically just "use a calculator," which isn't exactly productive.
    – jhch
    Aug 13, 2019 at 14:49
  • 1
    @JohnHughes The OP isn't asking for such explanation so I hesitate to go into it in more detail. Briefly, the tree proof attempts to show that the negation of what is desired leads to a countermodel. Each branch leading to "x" means that every attempt to show that negation fails by leading to a contradiction. If every branch leads to failure (contradiction), the original statement succeeds or is valid. However, if a branch does succeed, then one could use that branch to find valuations for a countermodel showing that the original statement is not valid. Aug 13, 2019 at 15:41
  • Thanks for the clarification--I think it'd be valuable to include in your answer. While the OP may not have been explicitly asking for explanation, saying "use this tool" with no context for why or how the tool works seems short of the "fuller explanations are better" ideals of SE.
    – jhch
    Aug 13, 2019 at 16:13
  • 1
    @JohnHughes I added information about how the tree proof works and noted that a natural deduction proof would be another way to show the equivalence. Aug 13, 2019 at 16:36
  • It's the perfect answer I wanted! Thanks.
    – edoardottt
    Aug 13, 2019 at 16:52

The first observation is that moving the ∀b quantifier in the second formula to the front is unproblematic since we can safely move a quantifier from the right-hand side of an implication to the outside provided we don't bind any variables that were free before, which is the case here, so

∀a,b [(P(a) ∧ ¬R(a) ∧ S(b)) → G(a,b)]           (first formula)

is equivalent to

∀a,b [(P(a) ∧ ¬R(a)) → (S(b) → G(a,b))]         (second formula with ∀b moved to the front)

Now we can imagine the quantifers away and also abstract away from the structure of the subformulas -- since the only difference between the two formulas lies in the connectives while the predicates between the connectives are all the same, identity or difference in the truth values of the two formulas does not depend on the predicate logical interpretation of the quantifiers or predications but only on the syntactic structure of the two formulas, so it is permissible for the sake of the equivalence check to replace the predications by simple propositional letters while leaving the general structure intact:

(P ∧ ¬R ∧ S) → G           (first formula with the predications replaced by propositional variables)

(P ∧ ¬R) → (S → G)         (second formula with the predications replaced by propositional variables)

To further simplify, we can turn the identical subformulas P ∧ ¬R into one propositional variable Q so only have the relevant differences:

(Q ∧ S) → G           (first formula further simplified)

Q → (S → G)           (second formula further simplified)

The two formulas have the same syntactic structure as the original ones, just heavily simplified by abstracting away over the parts that are identical anyway -- but this simplification is all we need, as the rest makes no difference to the question of equivalence.

And now that we have two propositional formulas, we can simply put that into a truth table and check whether the respective columns of the two formulas are identical:

G   Q   S   (Q ∧ S) → G    ≡    Q → (S → G)
F   F   F         T        ✓        T
F   F   T         T        ✓        T
F   T   F         T        ✓        T
F   T   T         F        ✓        F
T   F   F         T        ✓        T
T   F   T         T        ✓        T
T   T   F         T        ✓        T
T   T   T         T        ✓        T

As you can say, the two formulas have the same truth values in all rows, so they are equivalent. In general, we have an equivalence between statements of the form (A ∧ B) → C) and A → (B → C): Stating "If A and B hold, then C is true" is equivalent to stating "If A holds, then if B holds, then C is true. Since the two formulas are jut more complex instances of this scheme, they are equilvalent.

Reminder: This procedure -- replacing the predicate logical subformulas by propositional variables and then simply using a truth table -- only works because the two formulas only differ in their syntactic (propositional) structure and not in their predications, so we don't need the complicated ontology of predicate logical interpretation to check their equivalence. We can not in general employ truth tables for predicate logic, as there may be differences in the structure of the predications. But for the particular case of the pair of formulas in question, this way of argumentation works just fine.

  • Thanks for your answer! It was useful!!!!
    – edoardottt
    Aug 13, 2019 at 16:54

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .