Skip to content Skip to navigation Skip to collection information

Connexions

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: John Greiner, Phokion Kolaitis, Moshe Vardi, Matthias Felleisen. E-mail the authors

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. φ[y↦x]∀x.φ[y↦x]
∀∀Elim ∀∀-elimination
∀x. φ∀x.φ
tt is any term that is free to be replaced in φφ.
Domain non-empty.
φ [x↦t]φ[x↦t]
∃∃Intro ∃∃-introduction
φφ
tt is any term in φφ that is free to be replaced.
Domain non-empty.
∃x. φ[t↦x]∃x.φ[t↦x] , 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.
φ [x↦c]φ[x↦c]

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 φ[v↦w]φ[v↦w] 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.

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