Syntax

For purposes here, we will assume a simple ASCII lexicon and a KIF'ish syntax. The lexicon must include identity, the usual boolean operators and quantifiers, and a distinguished constant "ist" for McCarthy's "true in a context" relation. We also need — or it will at least be convenient — to have a special term forming operator that turns sentences into terms for propositions. The reason this seems necessary is that, according to current CL semantics, an atomic sentence of the following form

(foo bar (baz a b))

(ist ?con (baz a b))

For purposes here, then, I will use square brackets ‘[...]’ as a term forming operator; that is, if φ is a wff, then [φ] is a term — intuitively, of course, one that denotes the propositions expressed by φ. I will also only assume a global vocabulary, i.e., one that contains only denoting names, as I'm still not convinced Pat's treatment of nondenoting names quite works as stated. I'll present the semantics simply by modifying the HTML in Pat's SCL document.

CLIF semantics

Interpretations

The semantics of CLIF is defined conventionally in terms of a satisfaction relation between CLIF text and structures called interpretations. Since CLIF core syntax contains a number of 'syntactic sugar' constructions, we give the semantic conditions for a basic subset called the CLIF kernel, and then translate the remaining syntactic constructions into the kernel.

A vocabulary is a set of names. The vocabulary of an CLIF text is the set of names occurring in the text,. The vocabulary of an CLIF module is the union of the vocabularies of all text in the module.

An interpretation I of a vocabulary V is a pair ⟨D_I,P_I⟩. D_I comprises the objects of I and P_I the propositions of I. U_I = D_I∪P_I as the universe, or domain (of discourse), of I. D_I is to contain at least two distinguished objects T and F. There are three defined mappings on U_I: rel_I from U_I to subsets of U_I*, fun_I from U_I to functions U_I*->D_I, and int_I from V to U_I, such that int_I(n) is in U_I. If p ∈ P_I, then we stipulate that rel_I(p) ∈ {T,F}. Henceforth, We will omit the subscripts and identify int_I with I when no confusion arises.

The set P_I of propositions is closed under a number of operations:

• A one-to-one operation PR that maps an object (in the signficant case, a relation) and n objects into P (formally, D × {Dⁿ | n ∈ N⁺} → P). Let p = PR(r,e₁,…,e_n):
  • Each e_i is said to be a constituent of p.
  • Let e ∈ {e₁,…,e_n}. For d ∈ D, let p[e/d] = PR(r,d₁,…,d_n), where d_i is e_i if e_i is not e, and d_i is d, if e_i is e. Intuitively, of course, p[e/d] is the proposition just like p except that it involves d instead of e.
  • The type of p is atomic.
• An operation NEG that maps propositions to propositions. Let p = NEG(q):
  • An object e is a constituent of p just in case e is a constituent of q;
  • If e is a constituent of p, p[e/d] is NEG(q[e/d]).
  • if q is any proposition other than NEG(p), the type of p is negation.
• An operation CONJ that maps finite sequences of length > 1 of propositions to propositions. Let p = CONJ(q₁,…,q_n):
• An object e is a constituent of p just in case it is a constituent of one of the q_i ;
• p[e/d] is CONJ(q₁[e/d],…,q_n[e/d]);
• The type of p is conjunction.
• An operation EXIST that maps a proposition q and an object c to a proposition. Let p = EXIST(c,q):
• If c is a constituent of q, then c is not a constituent of p
• For e other than c, p[e/d] is EXIST(c,q[e/d]); p[c/d] is just p.
• The type of p is existential quantification.

A condition on our operations is that every proposition is of exactly one type.

There are several principles governing identity with respect to these operations.

1. Double negations cancel each other out:

   NEG(NEG(p)) = p, for any p ∈ P.

2. Conjunctions are identical if their respective arguments constitute the same set. Hence, the order of the arguments in a conjunction is irrelevant, and repeats in the argument sequence are irrelevant:

   CONJ(q₁,…,q_n) = CONJ(r₁,…,r_m) if {q₁,…,q_n} = {r₁,…,r_m}, for q_i,r_j ∈ P.

3. Conjunctions of nonconjunctions are identical only if their respective arguments constitute the same set.

   CONJ(q₁,…,q_n) = CONJ(r₁,…,r_m) only if {q₁,…,q_n} = {r₁,…,r_m}, for q_i,r_j ∈ P – Range(Conj).

4. Iterated applications of the conjunction operator are redundant:

   CONJ(q₁,…,q_n) = CONJ(q₁,…,q_i,CONJ(q_i+1,…,q_j),q_j+1,…,q_n), for 0 ≤ i ≤ n.

5. If propositions differ only with regard to a single constituent, then the generalizations of those propositions with respect to those constituents are identical:

   If q = p[e/d] ≠ p, then EXIST(d,q) = EXIST(e,p).

6. The order of iterated generalizations is irrelevant:

   EXIST(c,EXIST(d,q)) = EXIST(d,EXIST(c,q)).

Truth Values Determined by Type

Recall that every proposition is of one and only one type. We stipulate that the relational extension rel of a proposition be constrained in the following way depending on its type.

• If p = PR(r,e₁,…,e_n), then rel(p) = T iff ⟨e₁,…,e_n⟩ ∈ rel(r).
• If p = NEG(q), where q is not NEG(p), then rel(p) = T iff rel(q) = F.
• If p = CONJ(q₁,…,q_n), then rel(p) = T iff rel(q_i) = T for all i < n (i > 0).
• If p = EXIST(e,q), then rel(p) = T iff, for some d ∈ U, rel(q[e/d]) = T.

Logical Form

Any particular composition of the four operations, applied to a given initial stock of objects and relations, that yields a proposition p can be thought of as a logical form (LF) for p. No complex proposition has a unique LF. Trivially, for instance, if p has LF F(e₁,…,e_n), it also has LF NEG(NEG(F(e₁,…,e_n))). Less trivially, suppose q, r, and s are atomic propositions, and let p be CONJ(q,r,s). By principle 4 above, CONJ(q,r,s) = CONJ(q,CONJ(r,s)). It follows that p is both the conjunction of three atomic propositions and the conjunction of a single atomic proposition with the conjunction of two atomic propositions. Similarly, let p be EXIST(a,EXIST(b,PR(r,a,b))). By principle 6, p is also EXIST(b,EXIST(a,PR(r,a,b))). We can, however, specify a simplest LF for any proposition, which we can then use as a sort of canonical LF for p.

Determining Propositional identity

Algorithm for reducing to simplest LF. Given two propositional terms:

1. Convert to existential/conjunctive form (with negation)
2. Remove double negations.
3. Eliminate all nested conjunctions, e.g., convert "(and (p q … (and r s …) …))" to "(and p q … r s …)".
4. Eliminate all duplicate conjuncts.
5. Order conjuncts alphabetically within each conjunction.
6. Order iterated quantifiers alphabetically (according to bound name)
7. Test for alphabetic variance.