Re: [RIF] Agenda 2 May RIF Telecon

In response to the continued difficulty in defining first-order logic in
the working group, I went looking for a good definition on the net.  The
Wikipedia has an entry for first-order logic but doesn't use a
model-theoretic semantics so I decided to take the syntax part of the
Wikipedia entry and add a semantics part.  The result is both included and
attached here.

Enjoy.

Peter F. Patel-Schneider


		First-order Logic (with Equality)

The following is a fairly vanilla definition of First-order Logic (with
Equality).  It should be "the same as" just about every other definition of
First-order Logic that uses Tarskian model theory for its semantics.


SYNTAX

[This section is mostly copied from the Wikipedia entry for First-Order
Logic (http://en.wikipedia.org/wiki/First_order_logic).  I have fixed up
the formatting a bit, made some minor changes, and added a bit about IRIs.]

Vocabulary (essentially from the Wikipedia):

The "vocabulary" is composed of

1. A set of predicates [...] (or relations) each with some valence (or
   arity) >=1, which are often denoted by uppercase letters P, Q, R,...
2. A set of constants, often denoted by lowercase letters a, b, c,... .
3. A set of functions, each of some valence >= 1, which are often denoted
   by lowercase letters f, g, h,... .
4. An infinite set of variables, often denoted by lowercase letters x, y,
   z,... .  
5. Symbols denoting logical operators (or connectives): ¬ (logical not), ^
   (logical and), v (logical or), and often others.
6. Symbols denoting quantifiers: A (universal quantification), E (existential
   quantification).  
7. Left and right parenthesis.  
8. An identity or equality symbol = is sometimes but not always included in
   the vocabulary.  [If it is, it takes the syntactic form of a binary
   predicate.]

The sets of constants, functions, and relations are usually considered to
form a language, while the variables, logical operators, and quantifiers
are usually considered to belong to the logic. 

[Note that it is certainly possible to make predicates, constants, and
functions take the form of IRIs.  It is even possible to have an IRI denote
several predicates, constants, and functions.  Variables do have to be
somehow distinguished from constants.]

Formation rules (essentially from the Wikipedia):

The formation rules define the terms, formulas, and the free variables in
them as follows. 

The set of terms is recursively defined by the following rules:

1. Any constant is a term (with no free variables).
2. Any variable is a term (whose only free variable is itself).
3. Any expression f(t1,...,tn) of n >= 1 arguments (where each argument ti
   is a term and f is a function symbol of valence n) is a term. Its free
   variables are the free variables of any of the terms ti.
4. Closure clause: Nothing else is a term.

The set of well-formed formulas (usually called wffs or just formulas) is
recursively defined by the following rules: 

1. Simple and complex predicates: If P is a relation of valence n >= 1 and
   the ai are terms then P(a1,...,an) is well-formed. Its free variables
   are the free variables of any of the terms ai. If equality is considered
   part of logic, then (a1 = a2) is well formed. All such formulas are said
   to be atomic.
2. Inductive Clause I: If p is a wff, then ¬p is a wff. Its free variables
   are the free variables of p.
3. Inductive Clause II: If p and q are wffs, then (p ^ q) and (p v q) are
   wffs. Their free variables are the free variables of p or q.
4. Inductive Clause III: If p is a wff and x is a variable, then Ax p and
   Ex p are wffs. Their free variables are the free variables of p or q
   other than x. (Any instance of x (is said to be bound - not free - in Ax
   p and Ex p .)
5. Closure Clause: Nothing else is a wff.




SEMANTICS

[This section is mine, but is quite vanilla.]


Given a vocabulary, an interpretation is a pair I = < D, II > where D, the
domain of the interpretation, is a non-empty set and II, the interpretation
function of the interpretation, is a function from the n-ary predicates of
the vocabulary to sets of n-ary tuples over D, from constants of the
vocabulary to elements of D, and from n-ary functions of the vocabulary to
mappings from n-ary tuples over D to elements of D.  If the equality symbol
is in the vocabulary, II maps it into the binary identity relation over D.

Given a vocabulary and an interpretation, a variable map is a map from the
variables of the vocabulary to elements of the domain of the
interpretation.  If V is a variable map, v is a variable, and d is a domain
element, then Vx/d is the map that maps x to d and all other variables the
same as V.

Interpretations are is in essence a way of giving meaning to a vocabulary.
Variable maps are needed to assist in giving meaning to free variables.

An interpretation, I=<D,II>, and a variable map, V, map terms to elements of
D as follows: 
1. IV(c) = II(c), where c is a constant
2. IV(x) = V(x), where x is a variable
3. IV(f(t1,...,tn) = II(f)(IV(t1),...,IV(tn)), for other terms

An interpretation, I=<D,II>, and a variable map, V, support a formula as
follows:
1. IV supports P(t1,...,tn) precisely when II(P) contains the tuple
   <IV(t1),...,IV(tn)>.
2. IV supports ¬p precisely when IV does not support P.
3. IV supports (p ^ q) precisely when IV supports both p and q.
4. IV supports (p v q) precisely when IV supports either p or q.
5. IV supports Ex p precisely when there is some domain element d such that
   IVx/d supports p.
6. IV supports Ax p precisely when IVx/d supports p for all domain elements
   d. 

It turns out that formulas with no free variables (often called sentences)
are supported independent of the variable map, so it is customary to say
that an interpretation by itself supports a sentence, or that the
interpretation is a model for the sentence.

A sentence that is supported by some interpretation (no interpretations,
all interpretations) is said to be satisfiable (unsatisfiable, a theorem,
respectively).  A sentence is said to entail another if all interpretations
that support the first sentence also support the second.

		First-order Logic (with Equality)

The following is a fairly vanilla definition of First-order Logic (with
Equality).  It should be "the same as" just about every other definition of
First-order Logic that uses Tarskian model theory for its semantics.


SYNTAX

[This section is mostly copied from the Wikipedia entry for First-Order
Logic (http://en.wikipedia.org/wiki/First_order_logic).  I have fixed up
the formatting a bit, made some minor changes, and added a bit about IRIs.]

Vocabulary (essentially from the Wikipedia):

The "vocabulary" is composed of

1. A set of predicates [...] (or relations) each with some valence (or
   arity) >=1, which are often denoted by uppercase letters P, Q, R,...
2. A set of constants, often denoted by lowercase letters a, b, c,... .
3. A set of functions, each of some valence >= 1, which are often denoted
   by lowercase letters f, g, h,... .
4. An infinite set of variables, often denoted by lowercase letters x, y,
   z,... .  
5. Symbols denoting logical operators (or connectives): ¬ (logical not), ^
   (logical and), v (logical or), and often others.
6. Symbols denoting quantifiers: A (universal quantification), E (existential
   quantification).  
7. Left and right parenthesis.  
8. An identity or equality symbol = is sometimes but not always included in
   the vocabulary.  [If it is, it takes the syntactic form of a binary
   predicate.]

The sets of constants, functions, and relations are usually considered to
form a language, while the variables, logical operators, and quantifiers
are usually considered to belong to the logic. 

[Note that it is certainly possible to make predicates, constants, and
functions take the form of IRIs.  It is even possible to have an IRI denote
several predicates, constants, and functions.  Variables do have to be
somehow distinguished from constants.]

Formation rules (essentially from the Wikipedia):

The formation rules define the terms, formulas, and the free variables in
them as follows. 

The set of terms is recursively defined by the following rules:

1. Any constant is a term (with no free variables).
2. Any variable is a term (whose only free variable is itself).
3. Any expression f(t1,...,tn) of n >= 1 arguments (where each argument ti
   is a term and f is a function symbol of valence n) is a term. Its free
   variables are the free variables of any of the terms ti.
4. Closure clause: Nothing else is a term.

The set of well-formed formulas (usually called wffs or just formulas) is
recursively defined by the following rules: 

1. Simple and complex predicates: If P is a relation of valence n >= 1 and
   the ai are terms then P(a1,...,an) is well-formed. Its free variables
   are the free variables of any of the terms ai. If equality is considered
   part of logic, then (a1 = a2) is well formed. All such formulas are said
   to be atomic.
2. Inductive Clause I: If p is a wff, then ¬p is a wff. Its free variables
   are the free variables of p.
3. Inductive Clause II: If p and q are wffs, then (p ^ q) and (p v q) are
   wffs. Their free variables are the free variables of p or q.
4. Inductive Clause III: If p is a wff and x is a variable, then Ax p and
   Ex p are wffs. Their free variables are the free variables of p or q
   other than x. (Any instance of x (is said to be bound - not free - in Ax
   p and Ex p .)
5. Closure Clause: Nothing else is a wff.




SEMANTICS

[This section is mine, but is quite vanilla.]


Given a vocabulary, an interpretation is a pair I = < D, II > where D, the
domain of the interpretation, is a non-empty set and II, the interpretation
function of the interpretation, is a function from the n-ary predicates of
the vocabulary to sets of n-ary tuples over D, from constants of the
vocabulary to elements of D, and from n-ary functions of the vocabulary to
mappings from n-ary tuples over D to elements of D.  If the equality symbol
is in the vocabulary, II maps it into the binary identity relation over D.

Given a vocabulary and an interpretation, a variable map is a map from the
variables of the vocabulary to elements of the domain of the
interpretation.  If V is a variable map, v is a variable, and d is a domain
element, then Vx/d is the map that maps x to d and all other variables the
same as V.

Interpretations are is in essence a way of giving meaning to a vocabulary.
Variable maps are needed to assist in giving meaning to free variables.

An interpretation, I=<D,II>, and a variable map, V, map terms to elements of
D as follows: 
1. IV(c) = II(c), where c is a constant
2. IV(x) = V(x), where x is a variable
3. IV(f(t1,...,tn) = II(f)(IV(t1),...,IV(tn)), for other terms

An interpretation, I=<D,II>, and a variable map, V, support a formula as
follows:
1. IV supports P(t1,...,tn) precisely when II(P) contains the tuple
   <IV(t1),...,IV(tn)>.
2. IV supports ¬p precisely when IV does not support P.
3. IV supports (p ^ q) precisely when IV supports both p and q.
4. IV supports (p v q) precisely when IV supports either p or q.
5. IV supports Ex p precisely when there is some domain element d such that
   IVx/d supports p.
6. IV supports Ax p precisely when IVx/d supports p for all domain elements
   d. 

It turns out that formulas with no free variables (often called sentences)
are supported independent of the variable map, so it is customary to say
that an interpretation by itself supports a sentence, or that the
interpretation is a model for the sentence.

A sentence that is supported by some interpretation (no interpretations,
all interpretations) is said to be satisfiable (unsatisfiable, a theorem,
respectively).  A sentence is said to entail another if all interpretations
that support the first sentence also support the second.