Set-Encoding of Bounded-Quantifier Formulae

Before we can exploit Ref to state and prove propositions such as the transfer principle (not to mention Los’s theorem, see Sect. 10.3), we must devise a set-encoding of terms and formulae that enables easy specifications of how to

  • (A) evaluate a term or formula under a set-assignment for its variables,
  • (B) determine the truth value of a sentence,
  • (C) replace a free variable by a constant within a term or formula,

and the like. Then we will be able to reason formally with Ref about the languages of specific universes.

The set-theoretic representation of terms and formulae can be conceived of rather liberally. By seeing each universe U as embedded in the class of all sets, which is Ref’s domain of discourse, we will in particular

  • • treat the different languages by a single encoding instead of separately,
  • • specify the function val that evaluates a ‘term’t under a set-assignment v for the variables occurring in it so that val(t, v) yields a result even when t does not encode a term.
Theory about the set-encoding of terms

Fig. 10.8 Theory about the set-encoding of terms

About one feature of the representation of the syntax, we see no reason for being flexible: each variable xn will be encoded by its subscript n, a positive integer.

The Theory interface displayed in Fig. 10.8 formulates the constraints to which we submit our encoding of terms, effected via two properties, Pair and Appl, and three functions: Ift, rgt, and cst. The two properties are meant to indicate which sets encode terms of the respective forms (l, r} and (l r); lft( p) and rgt( p) will provide, when applied to a set p that encodes a term of the form (l, r}, the two sets encoding the immediate subterms, l and r respectively; lft(q) and rgt (^) will behave likewise when q encodes a term of the form (l r). As for cst, it will send each set c to a constant c designating it univocally: not only cst (c) = cst (k) must hold whenever c = k, but we require also that -Pair(cst(c)), -Appl(cst(c)), and cst(c) / N, to avoid ‘collision’ between cst(c) and any set encoding a non-constant term. Unambiguous readability also demands that p e N, q / N, and p = q hold when Appl(p) and Pair(q) hold. This is the rationale behind the first two claims issued by the Theory termEncoding. To understand the third, fourth, and fifth claim thereof, think of 0 as non-encoding set par excellence: for every pair x, y of sets which differ from 0, we want unique sets p, q to exist such that lft(p) = lft(q) = x, rgt(p) = rgt(q) = y,and Pair(p), Appl(q) hold; conversely, we want lft(y) and rgt(s) to differ from 0 when either Pair(s) or Appl(s) holds. The last claim of termEncoding plays a technical role: since the only built-in kind of recursion in Ref is e -recursion, by imposing that the immediate subterms of any compound term t (as encoded by a set) belong to t, this claim will ease the recursive definition of functions over all terms.

Figure 10.9 suggests oneway of implementing the wanted functions and properties inside termEncoding, based on the remark that when 0 / {x, y} the projections x, y can be retrieved from both variants (x, y) U {x, y}, (x, y) U {x, y} U {0} (the former of which equals {x, y}+ U [1]) of Kuratowski’s pair (x, y).

Assuming that terms are encoded according to a quintuple such as the one produced by termEncoding, it is easy to implement their evaluation thus developing the Theory evalTerm whose interface is shown in Fig. 10.10.

A viable implementation of the quintuple needed to encode terms, followed by encodings of literals of the forms

Fig. 10.9 A viable implementation of the quintuple needed to encode terms, followed by encodings of literals of the forms (s 6 t), (s $ t) and ofbounded quantifiers of the forms (3 xn 6 t), (V xn 6 t). Equality can be eliminated in terms of membership

A Theory about the evaluation of terms

Fig. 10.10 A Theory about the evaluation of terms

This Theory receives, along with a quintuple of the said kind, a function th( N, V) supplying the value of the N-th variable in a set-valued assignment V; it manufactures and produces in output the evaluating function vai0. In order to represent a set-valued assignment it suffices to use a finite-length list which must, in its turn, be modeled somehow: in a manner—we propose—complying with the Theory interface shown in Fig. 10.11.

The property Lst produced by the Theory list is meant to indicate which sets represent lists; the dyadic function th associates with any such set t the number of components of the list and the sets occupying those components.16 Specifically, supposing that Lst(t) holds, th (0, t) will exceed by one the overall number of components of t, and th(n, t) will provide the n-th component of t when0 < n < th(0, t). It should be clear from this explanation that the three claims issued by list state that:

A Theory of lists

Fig. 10.11 A Theory of lists

  • 1. the length of every list is a finite ordinal;
  • 2. the equality criterion for lists t, m is that t and m have the same length h and the same я-th component for n = 1,...,h;
  • 3. from every triple m, h, x consisting of a list m, a natural number h, and a set x, one can obtain a list t of length h whose last component—if any—is x and whose n-th component is th(n, m) for n = 1,...,h — 1; viz.:

For a sparing encoding of formulae, we can think of equality as a derived construct; a logical equivalence by which it can be eliminated is in fact (s = t) ^ (3 xn e (s, s})(t e xn), where xn does not occur in s or in t. It is also advisable to treat conjunction and disjunction as polyadic connectives, so that the only formulae which need to be encoded directly are the ones of the forms (s e t), (s t), (3 xn e t) ^/h=0 , and (Vxn e t) (Vkj=0 , where each and each has in

its turn one of these forms. An expedient way of representing a multiple conjunction or disjunction, that owes much to Martin Davis for its dissemination in the early 1960s, is as the sets of conjuncts or disjuncts, respectively;[2] we will rely on this representation for completing our endeavor.

  • [1] x
  • [2] This way of representing formulae in conjunctive normal form is widely used today. In recentyears [32] resorted to it, to give a Ref-based correctness proof for the DPLL satisfiability algorithm.
 
Source
< Prev   CONTENTS   Source   Next >