Propositions for the Common Logic Interchange Format


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))
is so interpreted that the constant ‘baz’ is taken to be a function symbol, and hence ‘(baz a b)’ simply denotes an individual in the domain of quantification, viz., the value of the function denoted by ‘baz’ on the pair ⟨a,b⟩ indicated by ‘a’ and ‘b’, respectively. However, in McCarthy's theory of contexts, in the intended semantics of
(ist ?con (baz a b))
the expression ‘(baz a b)’ signifies a proposition that is asserted to be true in the context denoted by ‘?con’. Hence, it would appear that we need a new piece of syntax to be able to get the intended semantics of ‘ist’ right. Granted, we could treat ‘ist’ as an exception, but it seems best not to alter the basic nature of the semantics if we don't have to. ‘’ Alternatively, we could declare ‘ist’ to be a sentence operator rather than a predicate (this seems to be McCarthy's syntax), but given that we are introducing propositions as objects (indeed, we already have them to a limited degree in CL in the guise of 0-place relations), it seems to make better sense to let count ‘ist’ as a predicate.

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


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 ⟨DI,PI⟩. DI comprises the objects of I and PI the propositions of I. UI = DI∪PI as the universe, or domain (of discourse), of I. DI is to contain at least two distinguished objects T and F. There are three defined mappings on UI: relI from UI to subsets of UI*, funI from UI to functions UI*->DI, and intI from V to UI, such that intI(n) is in UI. If p ∈ PI, then we stipulate that relI(p) ∈ {T,F}. Henceforth, We will omit the subscripts and identify intI with I when no confusion arises.

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

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(q1,…,qn) = CONJ(r1,…,rm) if {q1,…,qn} = {r1,…,rm}, for qi,rj ∈ P.

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

    CONJ(q1,…,qn) = CONJ(r1,…,rm) only if {q1,…,qn} = {r1,…,rm}, for qi,rj ∈ P – Range(Conj).

  4. Iterated applications of the conjunction operator are redundant:

    CONJ(q1,…,qn) = CONJ(q1,…,qi,CONJ(qi+1,…,qj),qj+1,…,qn), for 0 ≤ in.

  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.

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(e1,…,en), it also has LF NEG(NEG(F(e1,…,en))). 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.

Valid HTML 4.01!

Last modified: Fri Jun 24 09:58:57 CDT 2005