[RIF] Proposal for vanilla first-order logic

The following satisfies part of my assigned action for last week, to 
propose a version of a vanilla first-order logic in order to clarify what 
is meant by the requirement that the RIF is at least as expressive as 
first-order logic. This text still needs to be put into wiki form. In the 
meantime, it is enclosed in the text of this email and attached as a Word 
document.

I believe that Peter Patel-Schneider's email last week  proposing a 
version of first-order logic was right on the mark; however, for those who 
feel that the reference must be a published text, the following might be 
useful.

Best regards,
Leora Morgenstern
=================================================================================

VANILLA FIRST-ORDER LOGIC

Presented below is a definition of a standard first-order logic having 
both predicates and functions, with equality defined as a logical symbol. 
It says nothing about whether arithmetic is included. Unlike Common Logic, 
it does not allow quantification over predicates, and thus does not 
exhibit behavior associated with higher-order logics.

Source: Ernest Davis, Representations of Commonsense Knowledge, Morgan 
Kaufmann, 1990, Chapter 2.  This largely follows the treatment by Benson 
Mates in Elementary Logic, with changes and additions for functions, etc. 
Note that minor changes in notation have been made to ease dissemination 
on the web. In particular, Roman letters are often substituted for Greek 
letters; quantifiers are represented by unreversed, right-side up letters; 
 standard keyboard symbols are used for Boolean operators; the  Boolean 
operator exclusive or is not used . Also, the = term is used in both an 
in-language and meta-language sense; context is used to disambiguate. 

(Reasons for choosing this source:
·       Syntax familiar and readable to people in Computer Science and AI 
(unlike, say, Mates); close to Peter Patel-Schneider?s document on vanilla 
FOL, based on the Wikipedia entry, but has a well-known book as a 
reference.
·       Well written, easy to understand
·       Accessibility and familiarity

SYNTAX

The symbols of a language L of  First-Order Logic consist of the logical 
symbols and the nonlogical symbols.

Logical symbols are: 
Boolean operators (~, v, &, , >)
The universal quantifier A
The existential quantifier E
The equal sign =
The open parenthesis ( , the close parenthesis ), and the comma ,
An infinite collection of variable symbols

Nonlogical symbols can be divided into three sorts: constant symbols, 
predicate symbols, and function symbols. (In this twiki, they will be 
differentiated by context; this may change in a later draft.)  Each 
predicate and function symbol is associated with a positive integer, 
denoting the number of arguments that the symbol takes. 

A string T is a term of L if one of the following holds:
1.  T is a constant symbol
2. T is a variable symbol
3. T has the form f(t1,t2, ?, tk) where f is a k-place function symbol and 
each of the ti is a term.

A string W is a well-formed formula of  of L if one of the following 
holds:

1.      W has the form P(t1,t2, ?, tk) where P is a k-place relation and 
each of the ti isa term. (These are the atomic formulas.)
2.      W has one of the following forms: ~X, X & Y, X v Y, X  Y, X<-> Y, 
where X and Y are well-formed formulas.
3.      W has the form (E v) X or (A x) V where v is a variable symbol and 
X is a formula.

An occurrence of a variable v within a wff W is  bound if it is within an 
occurrence in W of a formula of the form (E v) X or (A x) V. An occurrence 
that is not bound is free.

A formula W is closed if every occurrence of a variable in W is bound. 
Otherwise it is open in the variables that appear free. A sentence is a 
closed formula.

SEMANTICS

A domain D for a first-order language L is a set of entities or 
individuals. A constant symbol denotes an individual in D.  A k-place 
predicate symbol P denotes an extensional relation PP, which is a set of 
k-tuples of elements of D. (We can also say that PP is a set of elements 
of D-k, where D-k denotes those elements of D that are k-tuples.) A 
k-place function symbol f denotes an extensional total function ff from 
D-k to D; a set of k+1 tuples, whose last element depends functionally on 
the first k elements. 

An interpretation I for L associates 
·       each of the constant symbols with an element of D
·       each of the k-place function symbols with a function from D-k to D
·       each of the k-[place predicate symbols with a k-place relation on 
D, a subset of D-k

To define the semantics, one first defines the meaning of atomic formulas 
with no variables or quantifiers, and second defines the meaning of 
complex sentences. The truth of quantified sentences is defined in terms 
of substitutions, as developed below.

 A ground term is a term containing no variables. A ground formula is a 
formula containing no variables, free or bound.

If t is a ground term in L and I is an interpretation of L, then there is 
an individual u in D that is denoted by t under I. We write u = (t,I). 
Denotation is thus determined as follows:

a.      If t is a constant symbol a, then T denotes the individual that A 
associates with the symbol. (t,I) = (a,I).
b.      Otherwise, t has the form B(t1, ?, tk). The denotation of t is the 
result of applying the extensional function that I associates with B to 
the denotations of t1,?,tk.  Thus, <(t1,I),?,(tk,i),(t,i)> is a member of 
(B,I)

Let W = P(t1, ?, tk) be an atomic ground sentence. I |= W  (or, in 
notation closer to that of the book, (W,I) = True) just if the relation 
(P,I) holds on the objects (t1,I), ?, (tk,I);that is if the tuple 
<(t1,I),?,(tk,I)> is an element of (P,I). Otherwise I ~ |= W ;  (W,I) = 
False.

Further, let W be of the form t1 = t2, where t1 and t2 are ground terms. 
Then W is True if (t1,I) = (t2,I).

Let I be an interpretation of L, and let X and Y be closed formulas in L. 
Then:
a.      Let W = ~ W. Then (W,I) = True just if (X,I) is False; otherwise, 
(W,I) is False.
b.      Let W = X v Y. Then (W,I) is True just if either (X,I) is True or 
(Y,I) is True; otherwise, (W,I) is False.
c.      Let W = X & Y. Then (W,I) is True just if both (X,I) and (Y,I) are 
True; otherwise, it is False.
d.      Let W = (X  Y). Then (W,I) is True just if either (X,I) is False 
or (Y,I) is True; otherwise it is False.
e.      Let W = (X <-> Y). Then (W,I) is True just if both (X,I) and (Y,I) 
are True or if both (X,I) and (Y,I) are False; otherwise it is False.

The semantics for quantified terms and formulas are given using the 
following notion of substitution.

Let I be an interpretation of L with domain D. Let u be any member of D, 
and let d be a symbol not in L. Define a language L? = L union d = the 
first-order language containing all the symbols in L and also containing 
d, used as a constant symbol. Then I union (d -> u) is an interpretation 
of L union d with domain D with the following properties:
·       For each symbol a in L, (a, I union (d -> u)) = (a,I)
·       (d, I union (d -> u)) = u.


Let I be an interpretation of L with domain D. Let d be a symbol not in L. 
For any formula W, let W(m/d) be the formula that is just like W except 
that d has been substituted for every free occurrence of  m. Then:
a.      Let the closed formula X have the form (E m) W. Then (X,I) = True 
just if there is some element u in D such that (W(m/d), I union (d -> u)) 
= True.
b.      Let the closed formula X have the form (A m) W. Then (X,I) = True 
just if for every element u in D (W(m/d), I union (d -> u)) = True.


Inference

Can be specified using a natural deduction system (see. e.g, Mates?s 
system for L1, his first-order language with equality), or using a set of 
axioms, as in Davis, p. 39 (need to type this in here) plus the rule of 
inference Modus Ponens. Note that Davis?s axiom FOL.6 permits 
generalization, which is usually realized by an inference rule.)

VANILLA COMMON LOGIC (still to be done; sketch follows below)

We can define a subset of Common Logic that is similar in terms of 
expressivity and inferential power to the vanilla logic defined above, 
that is, a first-order logic with equality.

That is, we would choose to use the segregated version/dialect of Common 
Logic in which there is a distinction between functions, predicates, and 
constants. Thus, we would not get the ability to effectively quantify over 
functions and predicates ?for free?; thus, this version of CL would remain 
first-order. 

What we would keep from Common Logic is the ability to embed in sentences 
of CL ?irregular sentences? that are not themselves sentences of CL. 
Sentences of modal logic are examples of irregular sentences. This could 
provide the RIF with the ability to permit partial reasoning on theories, 
some of whose sentences were not written in first-order logic.

Common Logic has an abstract syntax that allows various concrete 
realizations. In practice, however, it would be necessary to specify this 
vanilla Common Logic in some particular concrete syntax.  It would seem 
advisable to use CLIF, the Common Logic version of KIF syntax.

A serious issue to consider with regard to using Common Logic is the fact 
that the (ISO) standard for Common Logic will not be made public. Although 
corporations, academic institutions, research labs, and other 
organizations could presumably gain access to the standard without much 
difficulty, there is still --- in my opinion --- something inherently 
troublesome about using a first-order logic which is not made publicly 
available in the manner which has been accepted as standard throughout the 
world for several millennia. Perhaps, rather than use the ISO Common Logic 
standard, RIF could use a version that has already been published and is 
accessible on the web by all, such as the draft at 
http://cl.tamu.edu/docs/cl/32N1377T-FCD24707.pdf. Certainly, the concern 
felt by some, when Peter Patel-Schneider presented his version of 
first-order logic based on information found at Wikipedia, that it would 
be better to use a more standard, traditionally published source, would 
seem to be magnified if the source cannot even be accessed by all on the 
web, as is the case with ISO standards.