Skip to content Skip to navigation Skip to collection information

OpenStax_CNX

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

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 inference rules

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

Summary: Using inference rules (formal proofs) for determining whether a first-order formula is true.

Inference with quantifiers

Proving first-order sentences with inference rules is not too different than for propositional ones. We have two slight twists to add: upgrading propositions to relations, and quantifiers. We still keep all our original propositional inference rules, but declare they can now be used on first-order WFFs. For our quantifiers, we introduce new first-order inference rules for adding and eliminating quantifiers from formulas. These four new rules look surprisingly simple, but they do have a couple of subtleties we have to keep track of.

Exists-intro

What is the most natural way to prove an existential sentence, like “there exists a prime number greater than 5”? That's easy — you just mention such a number, like 11, and show that it is indeed prime and greater than 5. In other words, once we prove (11>5)j:k:(11=jk)(j=1)(k=1) 11 5 j k 11 jk j1 k1 we can then conclude — using the inference rule Intro — that the formula p:(p>5)j:k:(p=jk)(j=1)(k=1)p p5 j k p jk j1 k1 is true. In general, to prove a formula of the form x:φx φ , we show that φφ holds when xx is replaced with some particular witness. (The witness was 11 in this example.) The inference rule is φ[pc] p:φφ[pc] pφ. The notation “φ[vw]φ[vw]” means the formula φφ but with every occurrence of vv replaced by ww. For example, we earlier wrote down the formula φ[p11]φ[p11], and then decided that this was sufficient to conclude p:φp φ .

watch out:

Observe that you'll never use the substitution-notation “ φ []φ[]” as part of a literal formula — it is only used in the inference rule, as a shorthand to describe the actual formula. (It's a pattern-matching metalanguage!)

Aside for logicians and macro-writers:

While it seems like substitution should be a simple textual search-and-replace, it is sometimes more complicated. In the formula φ=(x>5)x:Rx φ x 5 x Rx , we don't want φ[x6]φ[x6] to try to mention R6R6, much less generate something nonsensical like 6: 6 . In programming languages, we say we want “hygienic macros”, to respect our the language's notions of variables and scope. E.g., the C pre-processor's #define and #include notably does not respect hygiene, and can inadvertently lead to hard-to-find bugs. Solution: For simplicity, we will always consistently rename variables so that each quantifier binds a distinct variable.

How do you find a witness? That's the difficult part. You, the person creating the proof, must grab a suitable example out of thin air, based on your knowledge of what you want to prove about it. In our previous example, we used our knowledge about prime numbers and about the greater-than relation to pick a witness that would work. In essence, we figured out what facts needed to be true about the witness for the formula to hold, and used that to guide our choice of witness. Of course, this can easily be more difficult, as when proving that there exists a prime greater than 6971 of the form 4x1 4 x 1 . (It turns out that 796751 will suffice as a witness here.) Another approach is trial-and-error: Pick some candidate value, and see if it does indeed witness what you're trying to prove. If you succeed, you're done. If not, pick another candidate.

Exists-Elim

The complementary Elim rule corresponds to giving a (new) name to a witness. Thus if you know “there exists some prime bigger than 5”, then by Elim we can think of giving some witness the name (say) cc, and end up concluding “cc is a prime bigger than 5”. The caveats are that cc must be a new name not already used in the proof, and different from any variables free in the conclusion we're aiming for. However, we will be able to use that variable cc along with universal formulas to get useful statements.

Thus the general form of the rule is that p:φ φ[pc]pφ φ[pc]. That is, we can rewrite the body of the exists, replacing the quantified variable pp with any new variable name cc, subject to the restrictions just mentioned.

Forall-Intro

Can we extend that idea to proving a universal sentence? One witness is certainly not enough. We'd need to work with lots of witnesses, in fact, every single member of our domain. That's not very practical, especially with infinitely large domains. We need to show that no matter what domain element you choose, the formula holds.

Consider the statements “If nn is prime, then we know that …” and “A person XX who runs a business should always …”. Which nn is being talked about, and which person? Well, any number or person, respectively. After learning about quantifiers, you may want to preface these sentences with “For all nn” or “For all [any] persons XX”. But a linguist might point out that while yes “for all” is related to the speaker's thought, they are actually using a subtly different mode — that of referring to a single person or number, albeit an anonymous, arbitrary one. If “an arbitrary element” really is a natural mode of thought, should our proof system reflect that?

If we choose an arbitrary member of the domain, and show that the sentence holds for it, that is sufficient. But, what do we mean by “arbitrary”? In short, it means that we have no control over what element is picked, or equivalently, that the proof must hold regardless of what element is picked. More precisely, a variable is arbitrary unless:

  • A variable is not arbitrary if it is free in (an enclosing) premise.
  • A variable is not arbitrary if it is free after applying Elim — either as the introduced witness cc, or free anywhere else in the formula.
The usual way to introduce arbitrary variables is during Elim (w/o later using it in Elim). The formal inference rule for introduction of universal quantification will use these cases as restrictions.

Forall-Elim

Getting rid of universal quantifiers is easy: if you know x:φxφ (where φφ is a formula presumably involving xx), well then you can replace xx with anything you want, and the resulting formula will be true. We say x:φ φ[xt]xφ φ[xt] where tt is any term. Any variables in tt are arbitrary, unless it is an already-existing non-arbitrary variable.

For example, suppose we know that n:primen(n>2)oddnn primen n 2 oddn . We can replace nn with some term like m+4m4 to conclude primem+4(m+4>2)oddm+4 prime m4 m 4 2 odd m4 . The variable mm is arbitrary, unless it already occurred in non-arbitrary in a previous line of the proof (perhaps introduced via Elim). A more usual step is to use a term which is just a single variable, and (by coincidence) happens to have the same name as the quantified variable we are eliminating. Thus we often conclude primen(n>2)oddn primen n 2 oddn (note the absence of the initial ); nn is arbitrary (unless it had already been confusingly in use as a non-arbitrary variable earlier). This is helpful when we'll be later re-introducing the in a later step; see the example below.

Formal inference rules and proofs

Recall the syllogisms from a previous lecture. The general form of a syllogism is

  1. x:PxQxx Px Qx [major premise]
  2. PcPc [minor premise]
  3. QcQc [conclusion]

In our system, we don't have syllogism as a separate rule of inference, but it's easy to see how to translate any syllogism into our system: (for specific relations PP and QQ, and a specific constant cc).

Table 1
1x:PxQxx Px Qx Premise
2PcPc Premise
3PcQc Pc Qc Elim, by line 1, with x=cx c
4QcQc Elim, by lines 2,3, with φ=P=cφ Pc and ψ=Q=cψ Qc

Eliminating a quantifier via Elim and Elim is often merely an intermediate step, where the quantifier will be reintroduced later. This moves the quantification from being explicit to implicit, so that we can use other inference rules on the body of the formula. When this is done, it is very important to pay attention to the restrictions on Intro, so that we don't accidentally “prove” anything too strong.

Example 1

x:y:φ y:x:φ x y φ y x φ , for the particular case of φ=Rxy φ Rxy (other cases all similar).

Table 2
1x:y:Rxyx y Rxy Premise
2y:Rpyy Rpy Elim, line 1
3RpqRpq Elim, line 2
4x:Rxqx Rxq Intro, line 3
5y:x:Rxyy x Rxy Intro, line 4

Remember that in line 5, for Intro, we must verify that qq is arbitrary. It is, since it was introduced in line 3 by Elim, and there hasn't been an intervening Elim between lines 3 and 5.

We cannot instead conclude in line 4 that x:Rxqx Rxq by Intro, since variable pp was introduced by Elim in line 2, and therefore not arbitrary.

Exercise 1

Let's reverse the previous proof goal: y:x:φ x:y:φ y x φ x y φ , for the particular case of φ=Rxy φ Rxy (other cases all similar). This statement does not hold in general. So, what's the problem with the following “proof”?

Table 3
1y:x:Rxyy x Rxy Premise
2x:Rxqx Rxq Elim, line 1
3RpqRpq Elim, line 2
4y:Rpyy Rpy Intro, line 3
5x:y:Rxyx y Rxy Intro, line 4

Solution

In line 4, Intro requires that variable being generalized, qq, be arbitrary. It was introduced in line 2 by Elim, so that's OK. (E.g., we could've used Intro on line 3 to reintroduce the quantifier just eliminated.) But, qq was free when we used Elim on line 3, and this makes the variable no longer arbitrary. Line 3's choice of pp may depend on qq, and a variable is only arbitrary if it is free of any such constraints.

The Intro principle is actually very familiar. For instance, after having shown ¬(ab) ¬a¬b a b a b , we then claimed this was really true for arbitrary propositions instead of just aa,bb. (We actually went a bit further, generalizing individual propositions to entire (arbitrary) WFFs φφ,ψψ. This could only be done because in any particular interpretation, a formula φφ will either be true or false, so replacing it by a proposition still preserves the important part of the proof-of-equivalence.)

The Intro is also used in many informal proofs. Consider: “If a number nn is prime, then …”. This translates to “primen primen ”, where nn is arbitrary. We are entirely used to thinking of this as “n:primenn primen ” even though “nn” was introduced as if it were a particular number.

Proofs and programming

We previously saw that the inference rules of propositional logic are closely related to the process of type checking. The same holds here. For example, in many programming languages, we can write a sorting function that works on any type of data. It takes two arguments, a comparison function for the type and a collection (array, list, …) of data of that type. The type of the sorting function can then be described as “for all types TT, given a function of type (TT and TT) → TT, and data of type (collection TT), it returns data of type (collection TT)”. This polymorphic type-rule uses universal quantification.

Note that the details about substitutions and capture noted here arise in any kind of program that manipulates expressions with bound variables. That includes not only automated theorem provers, but compilers. To avoid such issues, many systems essentially rename all variables by using pointers or some similar system of each variable referring to its binding-site.

When people speak of proofs written by computer, they're talking about this style of inference rule proofs.

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 | 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 ...

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