Logic for Computer Science/First-Order Logic

From Wikibooks, open books for an open world
Jump to: navigation, search

First-Order Logic[edit]

In propositional logic, we considered formulas made about atomic objects, which could only be either true or false. First-order logic, the topic of this chapter, builds upon propositional logic and allows you to look inside the objects discussed in formulas. We can provide this more refined level of granularity by discussing objects as elements of sets that can be larger than just the set , and also include arbitrarily complex relationships with each other.

We begin first by defining the syntax of first-order (FO) logic, and then give these structures meaning.

Syntax[edit]

The domain of discourse for first order logic is first-order structures or models. A first-order structure contains

  1. Relations,
  2. Functions, and
  3. Constants (functions of arity 0).

The vocabulary of first-order logic is

  1. a set of relation symbols with associated arities, and
  2. a set of function symbols with associated arities.

Here are some example first-order logic vocabularies:

  1. A graph
    • Relation Set = {  : unary,  : binary }
    • Function Set = {  : unary }
  2. Arithmetic
    • Relation Set = {  : ternary,  : ternary,  : ternary,  : binary,  : binary}
    • Function Set = {  : unary,  : const }

Here, a graph is a set of vertices and a set of edges . For the arithmetic set note that the use of and is purely syntactic and we could have used the symbols "plus" and "times" instead. We haven't provided the symbols with any meaning yet.

A term denotes an element in the first-order structure. A term is used to refer to the elements in our domain of discourse. Here are the rules that describe what a term is:

  • every variable is a term, where a variable is simply another set of symbols
  • every constant is a term
  • If are terms, and is a -ary function then is a term.

For example, if is a binary function and is a ternary function then the following are all terms: .

An atomic formula is

,

where is a -ary relation and are terms. When viewing as a set, then this is just another way of saying that the tuple

.

A special relation means "equal" and cannot be interpreted otherwise. For example, stands for

.

A first-order formula is an expression built using a given first-order vocabulary and variables and the symbols . The set of first-order formulas is the minimum set satisfying the following:

  • atomic formulas are first order formulas
  • If and are formulas and is a variable, then the following are also formulas:

Semantics[edit]

A first-order structure over a given vocabulary consists of

  1. A domain, which is a set of elements (also known as a universe)
  2. A mapping associating to every -ary relation symbol in the vocabulary a -ary relation over the domain, and to every -ary function symbol a -ary function over the domain.

These components give meaning to the symbols.

Example:

Relation Set = {  : ternary,  : ternary,  : ternary,  : binary,  : binary }
Function Set = {  : unary,  : const }

A first-order structure over this vocabulary is:

  1. Domain: the set of integers
  2. Mapping : addition, multiplication, exponentiation, ordering,

In this structure, the formula

expresses the statement "there exists a prime number" (the number 1 also satisfies this statement).

Note here that is equivalent to .

Scope of Quantifiers[edit]

In the formula or , is referred to as the scope of quantification of the variable . An occurrence of a variable in a formula is bound if it is in the scope of quantification of that variable, otherwise the occurrence is said to be free. You can consider a quantifier use as a variable declaration.

A sentence is a formula with no free variables (i.e., all variables are bound). A sentence is either true or false.

A formula with free variable(s) can be considered as describing the properties of the free variable(s). For example, denotes a formula with occurring free and describes the properties of .

If a sentence evaluates to true over a structure , we say satisfies and denote this by .

  • iff , where is the interpretation of by .
  • iff and . (Similar for .)
  • iff .
  • if for some in the domain.
  • if for every in the domain.

Note: denotes the result of substituting for every free occurrence of in . Substitution is covered further later in this chapter.

Axiomatic approach[edit]

The axioms are a set of sentences meant to distinguish "desired" models from others. But typically, also have "undesired" models, which are called non-standard models.

Examples: Consider the vocabulary , where the symbols have the usual meaning (defined by FO sentences over this vocabulary). The standard interpretation for this set of axioms (see the end of this chapter) is the integers, but these are also satisfied by the set of integers modulo . This possibility is ruled out by adding the following sentence to the axioms:

Question: Can all non-standard models be axiomatized away? The answer is no. Consider the model shown in [TODO: import figure] for the vocabulary containing only (all elements in the upper line are larger than those on the lower line).

There is no set of first-order sentences that can distinguish this model from the natural numbers. Intuitively, the reason is that we cannot "backtrack" arbitrarily (towards ) in a first-order sentence. A similar non-standard model can be obtained for the full vocabulary above.

Evaluating FO Sentences[edit]

Given a first-order structure and a FO sentence , can we tell if ?

This problem is decidable for finite structures. For example, suppose is a binary relation representing the edges of a graph, and the given sentence is

.

We can evaluate the truth of this sentence by trying all possible values for and . (Naive evaluation: "nested loop".) This is polynomial time (in domain size) but exponential in the size of the formula.

On infinite domains, we may or may not be able to evaluate the truth of a sentence. With the vocabulary , where is the set of natural numbers, it is decidable if a sentence is true. (This is known as Presburger arithmetic.) However if we include multiplication, the truth of a sentence becomes undecidable.

A Deductive System for FO[edit]

A set of FO sentences is

  • Satisfiable if there is some structure such that
  • Unsatisfiable if it is not satisfiable
  • Valid if for all structure

Given a set of FO sentences and a sentence

  • entails (denoted ), if every structure that satisfies also satisfies .
  • iff is unsatisfiable.
  • If is finite then, iff is valid.
  • If a formula has free variables , is valid iff is valid.

Axioms for Validity[edit]

The axioms for validity are from three categories:

  1. Axioms for boolean validity. These are inherited from propositional logic.
  2. Axioms for equality.
  3. Axioms for quantification.
Boolean Validity[edit]

Given a FO formula , a boolean form of a propositional formula such that is obtained from by replacing each propositional variable in by a subformula of .

The set of Boolean forms of is denoted .

Examples:

  • For the FO formula , the boolean form is .
  • If , then where .

Claim: If and is valid, then is valid.

Equality Axioms[edit]

Let be terms. The following are valid formulas.

  • , where is a -ary function.
  • , where is a -ary relation.
Substitutions[edit]

Given a formula in which variable occurs free (denoted by ) and a term , we define the substitution of for in , denoted , as the formula that results from replacing every free occurrence of in by , subject to the constraint that contains no variable quantified in such that occurs free within the scope of quantification of . If does not occur free , then is defined as .

Example: Let be

,

then

  • is a valid substitution
  • is not a valid substitution.
Quantification Axioms[edit]
  1. , where is a term and is a valid substitution

In summary, the axioms for validity are :

  1. Axioms for boolean validity. These are inherited from propositional logic.
  2. Axioms for equality.
  3. Axioms for quantification.

Definition: A proof is a sequence of FO sentences such that for each either or such that and .

Notation: If there is a proof of using , we denote this fact by .

Fact (Soundness): If , then is valid.

Remark: The set of formulas which can be proven valid is recursively enumerable.

Example: Proof of the formula

The proof of is symmetrical.

Useful Equivalences[edit]

  • e.g. "x is even" and "x is odd"

Prenex Normal Form[edit]

Claim: Every FO sentence is equivalent to a FO sentence of the form , where and is quantifier free.

This is proved using the distributive properties of quantifiers. It may be necessary to rename variables, to avoid ambiguities. Although you can always move all quantifiers to the left, the resulting formula can actually be exponentially larger than the original one.

Example:

Recall the Axiomatic Method[edit]

  1. Describe the desired model as closely as possible using a (possibly infinite but recursive) set of axioms (FO sentences).
  1. Prove things using deduction.

Notation: We say is a valid consequence of (denoted ), if every model satisfying also satisfies .

Fact: iff is unsatisfiable.

Aside: Nonlogical axioms for number theory[edit]

The following fourteen first-order axioms describe the properties of arithmetic and numbers, i.e. addition (), multiplication (), exponentiation (, equality (), ordering (), successor function () and remainder (mod). This example shows the expressive power of first-order statements, which were originally hoped to provide a basis for the "one true mathematics."

Question: Why are they called "nonlogical" axioms?

NT1:
NT2:
NT3:
NT4:
NT5:
NT6:
NT7:
NT8:
NT9:
NT10:
NT11:
NT12:
NT13:
NT14: