Skip to content Skip to navigation

Connexions

You are here: Home » Content » First-Order Logic: equivalences

Navigation

Content Actions
  • Download module PDF
  • Add to ...
    Add the module to:
    • My Favorites
    • A lens
    • An external social bookmarking service
    • My Favorites (What is 'My Favorites'?)
      'My Favorites' is a special kind of lens which you can use to bookmark modules and collections directly in Connexions. 'My Favorites' can only be seen by you, and collections saved in 'My Favorites' can remember the last module you were on. You need a Connexions account to use 'My Favorites'.
    • A lens (What is a lens?)

      Definition of a lens

      Lenses

      A lens is a custom view of Connexions content. You can think of it as a fancy kind of list that will let you see Connexions through the eyes of organizations and people you trust.

      What is in a lens?

      Lens makers point to Connexions materials (modules and collections), creating a guide that includes their own comments and descriptive tags about the content.

      Who can create a lens?

      Any individual Connexions member, a community, or a respected organization.

      What are tags? tag icon

      Tags are descriptors added by lens makers to help label content, attaching a vocabulary that is meaningful in the context of the lens.

    • External bookmarks
  • E-mail the authors
  • Rate this module (How does the rating system work?)

    Rating system

    Ratings

    Ratings allow you to judge the quality of modules. If other users have ranked the module then its average rating is displayed below. Ratings are calculated on a scale from one star (Poor) to five stars (Excellent).

    How to rate a module

    Hover over the star that corresponds to the rating you wish to assign. Click on the star to add your rating. Your rating should be based on the quality of the content. You must have an account and be logged in to rate content.

    		(0 ratings)

Recently Viewed

This feature requires Javascript to be enabled.

First-Order Logic: equivalences

Module by: Ian Barland, John Greiner, Phokion Kolaitis, Moshe Vardi, Matthias Felleisen

Summary: Extend the laws of boolean algebra from propositional logic to first-order logic.

Note: Your browser may not currently support MathML. See our browser support page for additional details. You can always view the correct math in the PDF version.

Now that we can express interesting concepts using the quantifiers “∃∃” (“there exists”) and “∀∀” (“for all”), how can we use them for the problem of determining whether a formula is true? Back in lowly propositional logic, we had three methods:

  • truth tables,
  • equivalences, and
  • formal proofs with inference rules.
How can we adapt these approaches, for first-order logic?

Well, truth tables have no analog approach. With quantifiers, we don't have a finite set of propositions. Furthermore, variables can't refer to specific items in the domain until we try to interpret them. And when we do, the domain may be of any size — possibly even infinite. Using a truth table on an infinite domain is clearly infeasible, but the real problem stems from how we want to be able to discuss reasoning without respect to a particular domain.

However, we can add equivalences and inference rules to cope with quantifiers. After showing how to work with quantifiers, we'll come back to examine our newly-augmented systems for those desirable traits, soundness and completeness.

First-order Equivalences

When we upgrade from propositional logic to first-order logic, what changes do we need to make to the laws of boolean algebra? Well first off, we can keep all the existing propositional equivalences. For example, ∀x:¬φ∧ψ≡∀x:¬φ∨¬ψ x φ ψ x φ ψ . (Technically, we're even making those equivalences stronger, since those meta-variables φφ, ψψ, θθ can now stand for any first-order formula, rather than merely propositional formulas.)

But, we also need additional identities to deal with our new-fangled quantifiers. What should these be? The most interesting are those that relate the two kinds of quantifiers. Universal quantification (∀∀) says that something holds for all members of the domain, and existential quantification (∃∃) says that something holds for at least one member. Clearly, ∀x:φx φ implies ∃x:φx φ , but the other direction doesn't hold, so that is not an equivalence.

Aside:

Wait just a minute! That implication holds only if the domain is non-empty, so that there is at least one member in it. We'll see this restriction appear a few times.

What about ∀x:¬φ x φ ? In English, “for all items xx, φφ(xx) does not hold”. A more natural way to say this is that there is no item xx such that φφ(xx) does hold — that is, ¬∃x:φ x φ . Indeed, this will be one of our new boolean algebra rules.

See a list of equivalences with quantifiers. As before, we can use these to show other pairs of formulas equivalent, as in the following examples.

Example 1

Using these identities, we can simplify formulas such as the following: ∀y:∀x:Rx∧Qxy∧¬∃z:¬Rz y x Rx Qxy z Rz .

Table 1
1∀y:∀x:Rx∧Qxy∧¬∃z:¬Rz y x Rx Qxy z Rz  
2≡∀y:∀x:Rx∧Qxy∧∀z:¬¬Rz≡ y x Rx Qxy z Rz Complementation of ∃∃
3≡∀y:∀x:Rx∧Qxy∧∀z:Rz≡ y x Rx Qxy z Rz Double Complementation
4≡∀x:∀y:Rx∧Qxy∧∀z:Rz≡ x y Rx Qxy z Rz Reordering ∀∀s
5≡∀x:∀y:Rx∧∀y:Qxy∧∀z:Rz≡ x y Rx y Qxy z Rz Distribution of ∀∀ over ∧∧
6≡∀x:Rx∧∀y:Qxy∧∀z:Rz≡ x Rx y Qxy z Rz Simplification of ∀∀ (yy not free in RxRx)
7≡∀x:Rx∧∀y:Qxy∧∀x:Rx≡ x Rx y Qxy x Rx renaming
8≡∀x:Rx∧∀y:Qxy∧Rx≡x Rx y Qxy Rx Distribution of ∀∀ over ∧∧
9≡∀x:∀y:Qxy∧Rx∧Rx≡x y Qxy Rx Rx Commutativity of ∧∧
10≡∀x:∀y:Qxy∧Rx∧Rx≡x y Qxy Rx Rx Associativity of ∧∧
11≡∀x:∀y:Qxy∧Rx≡x y Qxy Rx Idempotency of ∧∧

Admittedly, some of these steps are rather small and obvious (e.g., our use of commutativity and associativity); we include them to illustrate how the identities of propositional logic are also used in first-order logic.

Example 2

An example of ∀x:ψ≡ψ xψ ψ where ψψ doesn't contain xx occurring free: Let ψψ be the formula we've seen before, asserting that a positive integer nn was noncomposite: ∀j:∀k:jk=n⇒j=1∨k=1j k j k n j 1 k 1 . Since nn occurs free, the truth of this formula depends on the value of nn. The formula ∀x:ψxψ really is equivalent to ψψ: It's true for exactly the same values of nn. The use of xx is essentially a bit of a rus, since xx plays no part of the meat of the ψψ.

However, the following formula is certainly not equivalent: ∀n:ψnψ. This formula asserts that all elements of the domain are non-composite (and it doesn't depend on choosing a particular interpretation for nn). Because nn occurred free, we can't use the “simplification of quantifiers” identity on it.

Finally, one more variant: ∀j:ψjψ. This is equivalent to the original, just like ∀x:ψxψ was. Why? The jj that occurs inside ψψ is a local variable, and is different from any enclosing bindings' jj. As we saw, local variables shadow less-local ones, just as in most programming languages.

Exercise 1

The equivalences for distributing implication over equivalences seem counterintuitive at first glance. Show that the following one holds, given all the identities which don't involve both implication and quantifiers.

Assuming that ψψ does not have any free occurrences of variable xx, ∀x:φ⇒ψ≡∃x:φ⇒ψ x φ ψ x φ ψ .

Solution

Table 2
1∀x:φ⇒ψx φ ψ  
2≡∀x:¬φ∨ψ≡x φ ψ Definition of ⇒⇒
3≡∀x:¬φ∨ψ≡ x φ ψ Distribution of ∀∀ over ∨∨
4≡¬∃x:φ∨ψ≡ x φ ψ Complementation of ∃∃
5≡∃x:φ⇒ψ≡ x φ ψ Definition of ⇒⇒

Are the following two sentences true?

  • “All flying pigs wear top hats.” ∀p:wears_top_hatpp wears_top_hatp (over the domain of flying pigs).
  • “All numbers in the empty set are even.” ∀x:evenxx evenx (over the empty domain).
  • “Every Pulitzer prize winner I've met thinks I'm smart, and cute, too!” ∀x:thinksImSmartAndCutexx thinksImSmartAndCutex (over the empty, since I haven't met any Pulitzer prize winners).
Each sentence states that some property holds for every member of some set (flying pigs or the empty set), but there are no such members. Such sentences are considered vacuously true.

Okay, maybe you believe that the sentences aren't false, but you still want some reason to consider them true. Well, think of their negations:

  • “There exists a flying pig not wearing a top hat.” ∃p:¬wears_top_hatp wears_top_hatp , over the (empty) domain of flying pigs. You can't go off and find a flying pig which contradicts this, since you can't find any flying pig at all. (Note that the negation isn't “No flying pigs wear top hats.”)
  • “There exists a number in the empty set that is even.” ∃x:¬evenxevenx, over the empty domain. (The negation isn't “No numbers in the empty set are even.”)
Since these negations are false, the original sentences must be true. This is also similar to the fact that a simple propositional implication, a⇒ba b is true, if aa is in fact false, regardless of the truth of bb; in this crude analogy, aa corresponds to “in the domain”.

Aside:

In boolean algebra, we only allow the values false and true, with no third option. This is sometimes called the law of the excluded middle. Philosophers have developed “trimodal” logics which have a third option, but everything in those logics can be translated into something in traditional logic; such logics might be more convenient in some cases, but they aren't more expressive. ¶ Fuzzy Logic, on the other hand, is a variant where every proposition has a degree of truth (from zero to one). While this is different than propositional logic (and, it is the right way to model many real-world problems), as a logic it hasn't yielded interesting new mathematical results.

Even more silliness can ensue when the domain is empty: For example, not only is every member of the empty set even, but every member is simultaneously odd! That is, ∀x:Rx∧¬Rxx Rx Rx is true (only) when the domain is the empty set. Even more degnerately, ∀xx is a true (only) on the emtpy domain.

Are we done yet?

While equivalences are very useful, we are often interested in implications such as the one mentioned previously: ∀x:φ⇒∃x:φ x φ x φ . We could rephrase that as an equivalence, ∀x:φ⇒∃x:φ≡true x φ x φ . Informally, it should be clear that that is rather awkward, and formally it is as well.

But such implications are exactly what inference rules are good for. So, let's continue and consider what first-order inference rules should be.

Comments, questions, feedback, criticisms?

Send feedback