Pure Functions

Overview:

The theory of Pure Functions is an alternative to the theory of sets as a logical foundation for mathematics in which the elements of the universe of mathematics are functions rather than sets.
introduction
Ontological experiments in Higher Order Set theory.
objectives
To make a theory of functions which is a close as possible in spirit to Zermelo Fraenkel set theory.
methods
Define the universe of pure functions as a new defined type in higher order set theory. The theorems proven about the primitive and defined constants associated with the type correspond to axioms suitable for a first order axiomatisation.

introduction:

Ontological experiments in Higher Order Set theory.
Ontological Relativity
The first purpose of this discussion of pure functions is simply to illustrate the arbitrary nature of ontology. It is to show how mathematics might just as well be based on a theory of functions as upon a theory of sets.
congenial HOST
Another purpose is to illustrate that for this kind of foundational discussion, Higher Order Set Theory is a congenial environment, and to illustrate one way of proceeding about such an exercise.
Larger Goals
The motivation for my first attempt at the theory of pure functions (way back in 1988) concerned the semantics of specification languages. The aim was to come up with semantic domains for well-founded strong languages which included local polymorphic function definitions and elementary modularity. I was looking for a simple foundation system which could be used to define the semantics and derive the proof rules for specification languages such as VDM-SL and Z, and I had a prejudice in favour of high proof theoretic strength. Pure functions were the first step in a three stage construction which I then envisaged but did not complete.
What are Pure Functions?
The usual set theories (such as ZFC) are pure in the sense that the domain of discourse contains nothing but sets. An elaborate hierarchy of sets is built out of the empty set and nothing else. Pure sets are sets which, at bottom, contain nothing (possibly lots of times). Pure functions are analogous. The empty function is the only function whose domain and range are the empty set, and in set theory is identical with the empty set. If instead of starting with the empty set and making all the sets we possibly can, we start in the same place, but make only functions, then we get the pure (well-founded) functions.

objectives:

To make a theory of functions which is a close as possible in spirit to Zermelo Fraenkel set theory.
Proof Theoretic Strength
I'm looking for a theory of functions which has the same proof theoretic strength as ZFC.

Since we start by constructing a model rather than a logic it may not be immediately obvious what this means. What it means is that the model should be sufficiently rich to establish the consistency of an axiomatisation of the theory which has high proof theoretic strength.

The way this is achieved is to ensure that there are enough pure functions that the universe of pure functions contains a straightforward model for ZFC.

Uniformity of Ontology
This isn't targeted as a first order theory, though a first order presentation should be straightforward. Just as in set theory, there should be no type system, and only one kind of object in the universe. In this case they are functions.
Extensional
I was looking for a completely unqualified extensionality to make it look very close to set theory. So two functions must be equal iff they yield the same value absolutely everywhere.
Well Founded
Just like classical set theory, I was looking for a well-founded set theory. This means that no function could be in its own domain or range.
Limited Abstraction
Well-foundedness is closely related to limitations on functional abstraction which are analogous to the use of separation instead of unrestricted comprehension in ZFC. This is done in a very similar way to set theory. In a functional abstraction the domain of the required function must be specified (as the range of some already available function).

methods:

Define the universe of pure functions as a new defined type in higher order set theory. The theorems proven about the primitive and defined constants associated with the type correspond to axioms suitable for a first order axiomatisation.
1. Environment
I addressed this problem using a formal and machine supported logical system strong enough to allow the definition of semantic domains similar to the universe of ZFC and of appropriate operations and relations over these domains. The logic and tool of choice originally was HOL, Higher Order Logic and the LCF style proof system for that logic developed at the Computer Labs of the University of Cambridge. Before starting on the theory of pure functions some extensions were made to this to give a system which I then called HOL-ZFC.
3. Type Definition
The next step is to define the type of pure functions. This can now be done by strictly conservative methods using the type definition facilities in HOL. These facilities permit the introduction of a new type which is isomorphic (equipollent, of the same size) as a subset (not necessarily proper) of some already available type. For the pure functions this is a proper subset of the type SET.
2. Extensions
For cosmetic reasons I first wrapped pre and post processors round the proof tool to allow me to use an extended character set including the usual logical and set theoretic symbols. Then I introduced by non-conservative axiomatic extension a new type SET which was similar to the universe of ZFC. This gives a logical system which is strictly stronger than ZFC (since it could be used to prove the consistency of ZFC). With this extension in place it is possible to work with models of strong logical systems without further non-conservative extensions. The axiomatisation was quite straightforward so I won't show it here (though I may get round to it eventually).

:

Pure Functions

The theory is to be substantially in the spirit of classical set theory. Apart from the change from sets to functions, and those things which naturally flow from that change, the important features of set theory are to be preserved.

Among the features of ZFC considered important in this context are:

The theory of pure functions is constructed by filtering out from the universe of ZFC those sets which represent functions. Sufficient proof theoretic strength is provided for by observing that the set of functions selected, though a strict subset of the sets of ZFC, contain functions which can be used to represent every set in ZFC. This makes possible the reconstruction of ZFC within the theory of pure functions, which guarantees that the theory can be given the same proof theoretic strength as ZFC One way of doing this is to use the pure identity functions as representatives of the sets over which they are defined, these being defined in terms of pure functions in a manner analogous to the definition of the pure functions in terms of sets. (This gives us two one-one surjections from some sets to all pure functions, and from some pure functions to all sets.)

Uniformity of the domain is ensured by the use of a single appropriate selection criteria which characterises the sets which will represent the pure functions.

Since the intended theory is type free the principle of extensionality will be formulated by quantification over all elements of the universe. The limitation of size principle which limits the functions representable as graphs in ZFC, will limit the functions available in this theory of pure functions. Consequently, the proper domains of these functions will be sets in ZFC, and some arbitrary choice will have to be made in any model of the theory about the values obtained when a function is applied outside its domain.

In my original approach to this theory the choice of the value obtained by application of a function outside its domain was difficult, and resulted in complications to the definition of pure function and in the resulting theory. This was because I only considered choice of a particular value for this purpose, and whatever value is chosen cannot then be in the range of any pure function without causing a problem with the principle of extensionality.

When a came back to give an account of the theory a better alternative immediately occurred to me, which is to return a value which cannot possibly be in the graph of the function, e.g. the function itself. Though this means that this "undefined" value varies from function to function, but does not interfere with the principle of extensionality, and never appears in the range of a function. The theory developed in this way promises to be significantly simpler than the original, so its easier (and certainly more interesting) to develop and present the new version than give an account of the old. Note that the detail of what the undefined value is will not appear in the theory.

This is a sketch, I hope to do at least the formal definitions, and maybe prove the required results with either ProofPower or Isabelle. Lets suppose we have a formalisation of set theory in higher order logic, which we call HOL-ZFC. Now we define a new type in HOL-ZFC.

The first-thought defining property for the type is that it is isomorphic to the set of many one relations in the type SET of ZFC in HOL. This doesn't yield a pure theory of functions, because these functions are defined over and yield values which need not themselves be functions.

The collections of pure functions must be defined inductively. We define a property of properties of sets called pf hereditary.

A property is pf hereditary if:

  1. It is true of the empty set.
  2. Whenever it is true of all the elements in the field of a function it is true of that function.
A pure function in ZFC is any set which possesses all pf hereditary properties.

This definition is analogous to defining the natural numbers as the smallest set containing zero and closed under the successor function. The pure functions are the smallest collection which contains the empty set and is closed under the operation of forming new functions whose domain and range contain only values already known to be pure functions.

Having defined this set of SETs in ZFC in HOL we next define a number of operators over this collection which will server similar roles in our theory to the operators available in SET.

The following operators, definable as functions in HOL, are introduced:

The details of these operators are described below.

Equality

This is the primitive HOL polymorphic equality function specialised to type SET. The definition chosen will suffice to establish the required extensionality result for this equality relation.

Application

Application is defined in the usual way for a function and an argument in the domain of the function. For an argument outside the domain we can think of application as returning the function. Since the function could not possibly be in its own range (all these pure functions are well-founded), this ensures that the law of extensionality is true even when quantifying over the entire universe rather than just the domain of the function. However, its best not to use this coding trick in the theory, so to find out whether something is in the domain we have the Domain relation, and function application is defined loosely, so you don't actually know what the result of applying a function outside its domain is.

The Empty Pure Function

This is the same as the empty SET in ZFC in HOL, thought of as a the pure function whose domain is the empty set.

Functional Abstraction

This function takes a function in HOL defined over type SET together with a SET which determines the domain of the required function and returns the SET which is the graph of the restriction of the HOL function to the designated domain. The restriction is required by the classical principle of "limitation of size". In the absence of this principle the function spaces cannot be the full classical function space.

The SET used to designate the domain is cannot be the set of elements in the domain of the required function, since this will not be a pure function. Any pure function whose domain is the required set will server to determine the domain.

The Maplet Constructor

This gives the unit set of an ordered pair. Given two pure functions this will yield a pure function with a singleton domain.

Functional Override

This is the functional override operator defined over functions represented as graphs in SET. This operator is closed over pure functions.

Dependent Function Space Constructor

This operator and its associated axiom serves the roles performed in SET by the power set operator and the axiom of replacement.

The operator takes a pure function which is regarded as defining an indexed collection of sets. The sets are the domains of the pure functions in the range of the function.

The result of the operator is the set of dependent functions having the same domain as the operand function, and mapping each point in that domain onto a value in the set determined by the value of the operand function at that same point.


UP HOME © RBJ last modified 1998/12/12