Logic for Computer Science/First-Order Logic

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:
  1.  
  2.  
  3.  
  4.  
  5.  
  6.  

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
  2.  
  3.  
  4.  

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: