Basic Features of Our Proof Checker

Our proof-checker Ref, a.k.a. ^tnaNova or Referee, processes script files, named scenarios, which consist of definitions, theorems, and detailed proofs of the theorems. After checking a scenario for syntactic validity, Ref verifies that the proofs are compliant with the version of set theory built into it. The language in which scenarios are written extends the usual language of first-order predicate logic with constructs reflecting the theory which underlies Ref: we can for example, as shown by most of the abbreviating definitions in Fig. 10.1,[1] exploit a very flexible set abstraction construct of the form

A few basic operations over sets and maps; two special properties

Fig. 10.1 A few basic operations over sets and maps; two special properties

to specify many familiar operations and relations over sets.

Ref’s second-order construct named Theory enables one to package definitions and theorems into reusable proofware components. Besides providing theorems of which it holds the proofs, a Theory has the ability to bring into a mathematical discourse decisive clues.11 Like procedures of a programming language, Ref’s The- orys have input formal parameters, in exchange for whose actualization they supply useful information. Actual input parameters must satisfy a conjunction of statements, called the assumptions of the Theory. A Theory usually encapsulates the definitions of entities related to the input parameters and it supplies, along with some consequences of the assumptions, theorems talking about those internally defined entities that the Theory returns as output parameters. After having been derived by the user once and for all inside the Theory, the consequences of the assumptions, as well as the claims involving the output parameters, are available to be exploited repeatedly.

Two Theory interfaces are shown in Fig. 10.2. The Theory finitelmage awaits as input parameters a set f0, assumed to be finite, and a global function g, namely one that sends every set x to a value g x; whenever applied to fitting actual parameters, this finitelmage will simply produce a claim of the form Finite {g x : x e f0} ).The other one, reachGlob,12 only expects a global function g; it will return the global function glob0 sending every set b to the smallest superset {b, g b, g(g b),... } of [2] [3]

{b} which is closed under application of g to its own elements, as precisely stated by the claims which this Theory will supply.

An example of the use of reachability through a global function is the construction of the set of all natural numbers intended a la von Neumann, which can be carried out in two steps:[4]

Apply (glob0 : count)reachGlob(g(X) ^ X и {X})^Thm natsa:[Upwardcounting] (Vy, x, z | y € count(x) & z € COUnt(y) ^ Z € COUnt(X)) &

  • (V b, X, y | b € count(b) & (x € count(b) & y = X U{x} ^ y € count(b))) &
  • (V b, t | b € t & (Vx € t | x U {x} € t) ^ count(b) C t) &
  • (Vb | count(b) = {b} U {u U {u} : u € count(b)}).

Def nats: [vonNeumann'snaturalnumbers] N =Def count(0).

It would be pointless to discuss here the inferential armory of Ref, because we are still in the phase of designing how to formalize the basic techniques underlying nonstandard analysis, and the expected outcome of such a formalization is best described by a plan concerning the core Theory interfaces and by choices as to how implement some key definitions.

An important enhancement to the Zermelo-Fraenkel set theory came historically with von Neumann’s introduction of an axiom,

which forbids membership to form infinite chains to э t1 э t2 э •••; this is tersely stated by singling out, for any given set x, a set a disjoint from x that belongs to x unless x = 0. In Ref this principle is embodied by a construct, arb (X), such that

13

Interfaces of two Ref Theorys

Fig. 10.2 Interfaces of two Ref Theorys

(implying arb (0) = 0). The meaning of arb is competently handled by a most basic inference method of Ref.

To appreciate the usefulness of arb, consider the Theory whose interface appears on the left of Fig. 10.3. Upon receipt of a set n0 that meets a given property P, this Theory will return a set transfInd® still enjoying P but none of whose elements satisfies P. In its hidden internal working, transfInduction first applies the Theory reachGlob seen in Fig. 10.2 to g(X) = arb ({u e X | P(u)}) and then applies the resulting glob0 to n0 to get a set N0 = {no, g n0, g (g n0)0} such that arb ({w e N0 | P(w)}) is the sought transfInd®.

In Ref the well-foundedness of membership also lies behind a definition mechanism based on e-recursion, shown at work with the specification of img in Fig. 10.4 and which we will repeatedly use in the ongoing. A discussion about the syntax of e-recursive definitions can be found in [35, pp. 216-217]); concrete illustrations of it will suffice here. A basic example is

defining the rank of a set X. The mechanism at stake is akin to recursion as used in computer programming; like it, it resorts to a base case to avoid circularity: in fact, rk (X) = 0 when X = 0, since obviously {rk (y) U {rk (y)} : y e0} = 0. But rk (X) might also be an infinite set (actually, a transfinite ordinal), a situation which will occur, e.g., when X is infinite or has some infinite elements.

Transfinite induction contrasted with finite induction

Fig. 10.3 Transfinite induction contrasted with finite induction. The former exploits the well- foundedness of e while the latter exploits the well-foundedness of C over finite sets. Other classical forms of induction, e.g., arithmetic induction or induction over ordinals, can be conveniently hooked to membership or inclusion

A viable specification of the iterated images of g and of the output symbol glob® inside the Theory reachGlob of Fig

Fig. 10.4 A viable specification of the iterated images of g and of the output symbol glob® inside the Theory reachGlob of Fig. 10.2. Here ax is a Ref’s built-in constant subject to the assumption that ax = 0 & (Vx e ax | ]x} e ax)

Let us digress briefly. The a’s satisfying the equality a = rk (a) turn out to be precisely the sets known, after von Neumann, as ordinal numbers;[5] and it is not hard to prove, about the indexed class of sets which satisfy the conditions

—historically called the cumulative hierarchy—, that Va consists, for each ordinal a, of all sets whose ranks lie below a. Now consider the property

In this new instance of e-recursion, the reader can recognize a streamlined definition of the stages of the cumulative hierarchy: as one readily sees, V(№) holds; more generally, one can show that V (L) is logically equivalent to the existence of an ordinal a such that L = Va. We do not prove this fact but do call attention to it because a similar change of perspective will motivate our formalization of superstructures in the following section.

  • [1] About Ref’s built-in operator arb (X) that occurs thrice in Fig. 10.1, suffice it to say for the timebeing that it selects an element of its operand X when X = 0, and that arb (0) = 0.
  • [2] In a passage echoing Abraham Robinson’s ‘provocative remark’ which we have recalled in the Introduction through Martin’s words, Jack says about this ability of THEORYs[35,p. 9]: “• • • definitionsserve to ‘instantiate’, that is, to introduce the objects whose special properties are crucial to an intended argument. Like the selection of crucial lines, points, and circles from the infinity of geometricelements that might be considered in a Euclidean argument, definitions of this kind often carry aproof’s most vital ideas”. A typical case of this kind is, in arithmetic, the selection of the leastnatural number that meets some key property.
  • [3] This is a specialized variant of the Theory reachability presented in [35, Sect. 7.3]. As seenhere, the formal output parameters of a Theory always carry a subscript в.
  • [4] What follows is not meant to imply that the definition of N shown is the ideal one.
  • [5] A common definition of ordinals, owing to a simplification due to Raphael Robinson, is: Ord(L) ^Def V x (x e U ^ x c U) & V x V y( {x, y}c U ^ (x e y v y e x v x = y}).
 
Source
< Prev   CONTENTS   Source   Next >