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.
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 condition on our operations is that every proposition is of exactly one type.
There are several principles governing identity with respect to these operations.
NEG(NEG(p)) = p, for any p ∈ P.
CONJ(q_{1},…,q_{n}) = CONJ(r_{1},…,r_{m}) if {q_{1},…,q_{n}} = {r_{1},…,r_{m}}, for q_{i},r_{j} ∈ P.
CONJ(q_{1},…,q_{n}) = CONJ(r_{1},…,r_{m}) only if {q_{1},…,q_{n}} = {r_{1},…,r_{m}}, for q_{i},r_{j} ∈ P – Range(Conj).
CONJ(q_{1},…,q_{n}) = CONJ(q_{1},…,q_{i},CONJ(q_{i+1},…,q_{j}),q_{j+1},…,q_{n}), for 0 ≤ i ≤ n.
If q = p[e/d] ≠ p, then EXIST(d,q) = EXIST(e,p).
EXIST(c,EXIST(d,q)) = EXIST(d,EXIST(c,q)).
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.
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_{1},…,e_{n}), it also has LF NEG(NEG(F(e_{1},…,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.
Algorithm for reducing to simplest LF. Given two propositional terms: