Skip to content Skip to navigation Skip to collection information

OpenStax-CNX

You are here: Home » Content » Intro to Logic » first-order equivalences

Navigation

Lenses

What is a lens?

Definition of a lens

Lenses

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

What is in a lens?

Lens makers point to 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 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.

This content is ...

Affiliated with (What does "Affiliated with" mean?)

This content is either by members of the organizations listed or about topics related to the organizations listed. Click each link to see a list of all content affiliated with the organization.
  • Rice Digital Scholarship

    This collection is included in aLens by: Digital Scholarship at Rice University

    Click the "Rice Digital Scholarship" link to see all content affiliated with them.

Recently Viewed

This feature requires Javascript to be enabled.
 

first-order equivalences

Module by: Ian Barland, John Greiner, Phokion Kolaitis, Moshe Vardi, Matthias Felleisen. E-mail the authors

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

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:RxQxy¬z:¬Rz y x Rx Qxy z Rz .

Table 1
1y:x:RxQxy¬z:¬Rz y x Rx Qxy z Rz  
2y:x:RxQxyz:¬¬Rz y x Rx Qxy z Rz Complementation of
3y:x:RxQxyz:Rz y x Rx Qxy z Rz Double Complementation
4x:y:RxQxyz:Rz x y Rx Qxy z Rz Reordering s
5x:y:Rxy:Qxyz:Rz x y Rx y Qxy z Rz Distribution of over
6x:Rxy:Qxyz:Rz x Rx y Qxy z Rz Simplification of (yy not free in RxRx)
7x:Rxy:Qxyx:Rx x Rx y Qxy x Rx renaming
8x:Rxy:QxyRxx Rx y Qxy Rx Distribution of over
9x:y:QxyRxRxx y Qxy Rx Rx Commutativity of
10x:y:QxyRxRxx y Qxy Rx Rx Associativity of
11x:y:QxyRxx 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=1)j 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
1x:φψx φ ψ  
2x:¬φψx φ ψ Definition of
3x:¬φψ x φ ψ Distribution of over
4¬x:φψ x φ ψ Complementation of
5x:φψ 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, aba 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, x:falsex 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.

Collection Navigation

Content actions

Download:

Collection as:

PDF | EPUB (?)

What is an EPUB file?

EPUB is an electronic book format that can be read on a variety of mobile devices.

Downloading to a reading device

For detailed instructions on how to download this content's EPUB to your specific device, click the "(?)" link.

| More downloads ...

Module as:

PDF | More downloads ...

Add:

Collection to:

My Favorites (?)

'My Favorites' is a special kind of lens which you can use to bookmark modules and collections. 'My Favorites' can only be seen by you, and collections saved in 'My Favorites' can remember the last module you were on. You need an account to use 'My Favorites'.

| A lens I own (?)

Definition of a lens

Lenses

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

What is in a lens?

Lens makers point to 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 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

Module to:

My Favorites (?)

'My Favorites' is a special kind of lens which you can use to bookmark modules and collections. 'My Favorites' can only be seen by you, and collections saved in 'My Favorites' can remember the last module you were on. You need an account to use 'My Favorites'.

| A lens I own (?)

Definition of a lens

Lenses

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

What is in a lens?

Lens makers point to 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 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