# OpenStax_CNX

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

• #### First-Order Logic

• ##### Reasoning with inference rules
• Exercises for First-Order Logic

### 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?

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

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

Inside Collection (Course):

# first-order inference rules

Summary: Inference rules for reasoning about first-order logic formulas.

The following are in addition to those of propositional logic.

Table 1: Our first-order inference rules
Abbreviation Name If you know all of… …then you can infer
Intro -introduction
 φφ yy arbitrary.
x. φ[yx]x.φ[yx]
Elim -elimination
 ∀x. φ∀x.φ tt is any term that is free to be replaced in φφ. Domain non-empty.
φ [xt]φ[xt]
Intro -introduction
 φφ tt is any term in φφ that is free to be replaced. Domain non-empty.
x. φ[tx]x.φ[tx] , where tt is arbitrary
Elim -elimination
 ∃x. φ∃x.φ cc is a new constant in the proof. cc does not occur in the proof's conclusion.
φ [xc]φ[xc]

As usual, we use φφ as a meta-variable to range over first-order WFFs. Similarly, tt is a meta-variable for first-order terms, and cc is a meta-variable for domain constants. The notation φ[vw]φ[vw] means the formula φφ but with every appropriate occurrence of vv replaced by ww.

As discussed in the lecture notes, 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).

As a detail in Elim and Intro, the term tt must be free to replace the variable xx in φφ. This means that it is not the case that both tt contains a variable quantified in φφ, and that xx occurs free within that quantifier. In short, the bound variable names should be kept distinct from the free variable names. Also, only free occurrences xx get replaced. The restriction in Elim on cc being new is similar.

## Content actions

PDF | EPUB (?)

### What is an EPUB file?

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

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

PDF | EPUB (?)

### What is an EPUB file?

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

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

#### 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?

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?

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