.nr PS 11
.nr VS 14
.so roff.defs
.RP
.TL
Universal Set Theory in SML (document 45)
.AU
Roger Bishop Jones
.AI
ICL Defence Systems
.AB
This document consists of a formal specification in SML
of a variant of classical first order set theory.
This particular variant consists of ZFC augmented by a
hierarchy of universes, each enjoying the same closure properties as ZFC.
To cap it all we have classes.
.LP
This issue is update by removing an error in the definition of
substitution and by modification and extension to the auxiliary
functions, some of which will be used in subsequent documents.
Use of the SML `modules' has been introduced.
.IP "\fBChanges Forecast\fP"
Future changes may be made to make the theory practicable for use in deriving the proof theory of langauges whose semantics is defined in terms of UST.
This may involve introducing some "urelements" rather than sticking to a pure set theory, since the terms needed to give denotations to primitive types such as natural numbers rapidly get out of hand.
.AE
.ds LH DBC/FMU/RBJ/085   Issue 2.1
.ds CH UST in SML
.ds RH 1988-03-01 Page \\n(PN
.ds LF DBC/FMU/RBJ/085   Issue 2.1
.ds CF UST in SML
.ds RF Page \\n(PN
.LP
.KS
.NH
INTRODUCTION
.LP
This document provides a formal description of a variant of classical
set theory axiomatised in first order logic.
This is claimed to be a suitable formal foundation for the VDM specification
language.
It is richer than strictly necessary, but this makes some of the constructions
simpler, and provides more flexibility for dealing with problems in the
current model.
.KE
.LP
It could be used simply to give a formal description of the current type
model, which would help in deriving the proof theory.
In this case the iterative constructions in the model could be simplified
by taking intersections of sets containing the basic types and closed
under the type constructors.
.LP
More radical changes are also possible, such as closing the type universe
under a full partial function space constructor, and eliminating the
two tier construction of the present model.
Special provision is made in the choice function to smooth the use
of graphs to represent partial functions over spaces not containing
a bottom element.
.LP
Even after such constructions there remain larger sets which will support
semantics for polymorphism and modularity.
.LP
The set theory is roughly NBG with added universes.
The smallest universe is the universe of ZFC, and every universe is a member
of a larger universe with similar closure properties.
.LP
The specification is written in the language SML (standard ML).
.LP
SML is described in ECS-LFCS-86-2 (University of Edinburgh, Laboratory
for Foundations of Computer Science).
.KS
.NH
ABSTRACT SYNTAX
.sv lpf
infix 4 \*h;
infix 5 \(rh;
infix 6 \*d;
infix 7 \*e;
infix 8 == \(mo \(*e -- \(ib t_subs_for subs_for;
infix 9 inn;
structure UST =
struct
structure FTM =
struct
.sw
.sv lpf

type var	= string;
.sw
.KE
.sv lpf
datatype
	formula	=	\(no of formula				|
				op \(rh of (formula * formula)		|
				\*j of (var * formula)			|
				op == of (term * term)			|
				op \(mo of (term * term)
.sw
.LP
These constructs have their normal meaning, viz. negation,
material implication, existential quantification, equality and
membership respectively.
.sv lpf
and	term	= 		Var of var					|
				\(*m of term					|
				comp of (var * formula)			|
				V of term;
.sw
.KS
.LP
The meanings of these term constructors are:
.RS
.IP Var
Variables
.IP \(*m
choice function (following Oxford Z usage)
yields a set, which will be a member of its argument except
in the case that the argument is \(es.
.IP comp
.br
comprehension, "comp(a,b)" is more usually written {a | b}
.br
comprehension rather than separation is allowed but does not
necessarily yield a set.
It yields the class of sets which satisfy the predicate "\(*l a.b".
.IP V
V x is a "universe" containing x
.br
A universe is a set which satisfies very liberal closure conditions,
it is closed under all the set forming operations of ZF.
Every set is a member of some universe, and V x is a universe containing
x.
.RE
.KE
.LP
.KS
.NH
SUBSTITUTION
.NH 2
Set Theory in the Metalanguage (sml)
.LP
First a few definitions which enable us to talk about lists as
if they were sets.
.KE
.sv lpf
fun	x \(*e []	= false					|
	x \(*e (y::z)	= x = y orelse x \(*e z;
.sw
.sv lpf
fun	m\(cu []	= []						|
	m\(cu (a::b)	= a @ (m\(cu b);
fun	[] -- a		= []						|
	(h::t) -- a	= if h=a then t -- a else h::(t -- a);
.sw
.LP
Note here that:
.IP
m\(cu is here defined as a single prefix operator meaning distributed union.
.IP
@ is the concatenation operator built into SML.
.KS
.NH 2
Free Variables
.LP
We define the free variables in a formula or term as follows:
.sv lpf
fun	term_freevars (Var v)		= [v]							|
	term_freevars (\(*m t)		= term_freevars t					|
	term_freevars (comp (v,f))	= freevars f -- v					|
	term_freevars (V t)		= term_freevars t
	
and	term_list_freevars term_list	= m\(cu (map term_freevars term_list)
.sw
.KE
.sv lpf
and	freevars (\(no f)			= freevars f						|
	freevars (f1 \(rh f2)		= freevars f1 @ (freevars f2)			|
	freevars (\*j (v,f))			= freevars f -- v					|
	freevars (t1 == t2)		= term_freevars t1 @ (term_freevars t2)	|
	freevars (t1 \(mo t2)			= term_freevars t1 @ (term_freevars t2);
.sw
.KS
.NH 2
Substitutions
.LP
First define substitutions into terms.
.sv lpf
fun	primed nv varl =
			if	nv \(*e varl
			then	primed (nv^"'") varl
			else	nv;
fun	freev v terml = primed v (term_list_freevars terml);
.sw
.KE
.sv lpf
datatype ('a,'b)inc = op inn of ('a * 'b);
.sw
.sv lpf
fun	term t_subs_for ivar inn (Var v)
		=	if	ivar = v
			then	term
			else	Var v								|
	term t_subs_for ivar inn (\(*m t)
		=	(\(*m (term t_subs_for ivar inn t))				|
	term t_subs_for ivar inn (comp(v,f))
		=	if	ivar = v
			then	(comp(v,f))
			else	let	val nv = primed v (term_freevars term @
									(freevars f -- v))
					val nf = term subs_for ivar inn
							((Var nv) subs_for v inn f)
				in	(comp(nv,nf))
				end								|
	term t_subs_for ivar inn (V t)
		=	V (term t_subs_for ivar inn t)
and	curried_t_subs term ivar term'
		=	term t_subs_for ivar inn term'
.sw
.LP
Next substitutions into formulae.
.sv lpf
and	term subs_for ivar inn (\(no form)
		=	\(no (term subs_for ivar inn form)				|
	term subs_for ivar inn (form1 \(rh form2)
		=	(term subs_for ivar inn form1)
			\(rh (term subs_for ivar inn form2)				|
	term subs_for ivar inn (\*j (ivar',form))
		=	if	ivar = ivar'
			then	(\*j (ivar',form))
			else	let	val nv = primed ivar' (term_freevars term @
									(freevars form -- ivar'))
					val nf = term subs_for ivar inn
							((Var nv) subs_for ivar' inn form)
				in	(\*j(nv,nf))
				end								|
	term subs_for ivar inn (t1 == t2)
		=	(term t_subs_for ivar inn t1)
			== (term t_subs_for ivar inn t2)				|
	term subs_for ivar inn (t1 \(mo t2)
		=	(term t_subs_for ivar inn t1)
			\(mo (term t_subs_for ivar inn t2)
and	curried_subs a b c = a subs_for b inn c;
.sw
.KS
.NH
DERIVED CONSTRUCTORS
.NH 2
Boolean Connectives
.LP
.sv lpf
fun a \*d b	= (\(no a) \(rh b;
fun a \*e b	= \(no( (\(no a) \*d (\(no b));
fun a \*h b	= (a \(rh b) \*e (b \(rh a);
.sw
.KE
.NH 2
Existence and Subset
.LP
.sv lpf
fun \*k (v,f)	= \(no (\*j(v,\(no f));
fun a \(ib b	=	let	val x = freev "x" [a,b]
				in	\*j (x,(Var x \(mo a) \(rh (Var x \(mo b))
				end;
.sw
.KS
.NH 2
Sets
.LP
This set theory has classes.
Everything is a class, a set is a class which is the member of
a class (or a set).
.sv lpf
fun set a =	let val x = (freev "x" [a])
		in	\*k(x, a \(mo (Var x))
		end;
.sw
.KE
.LP
The empty set is the class which has no members (an axiom asserts
that this is a set).
.sv lpf
val \(es = comp("x",\(no(Var "x" == Var "x"));
.sw
.KS
.NH 2
Pairs Ordered Pairs and unit sets.
.LP
The following definitions of pair and ordered pair (opair) are
the usual ones.
.sv lpf
fun pair a b =
		let val x = (freev "x" [a,b])
		in	comp (x,(Var x==a) \*d (Var x==b))
		end;

fun opair a b = pair a (pair a b);

fun left a =
		let	val x = (freev "x" [a])
			and y = (freev "y" [a])
		in	\(*m (comp(x, \*k(y, a == opair (Var x) (Var y))))
		end;

fun right a =
		let	val x = (freev "x" [a])
			and y = (freev "y" [a])
		in	\(*m (comp(x, \*k(y, a == opair (Var y) (Var x))))
		end;

fun unit a = pair a a;
.sw
.KE
.KS
.NH 2
Power Set, Union, Intersection
.LP
.sv lpf
fun \*m a =	let val x = (freev "x" [a])
		in	comp (x,(Var x \(ib a))
		end;

fun \(cu a =
		let	val x = (freev "x" [a]);
			val y = (freev "y" [a])
		in	comp (x,\*k (y,(Var x \(mo (Var y)) \*e (Var y \(mo a)))
		end;

fun \(ca a =
		let	val x = (freev "x" [a]);
			val y = (freev "y" [a])
		in	comp (x,\*j (y,(Var y \(mo a) \(rh (Var x \(mo (Var y))))
		end;
.sw
.KE
.KS
.NH 2
Relations and (Partial) Functions
.LP
A relation is simply a set of ordered pairs.
.sv lpf
fun is_rel a =	let	val w = freev "w" [a]
			and x = freev "x" [a]
			and y = freev "y" [a]
			and z = freev "z" [a]
		in	\*j(w, (Var w \(mo a) \(rh
				\*k(x,\*k(y, ((Var w) == opair (Var x) (Var y)))))
		end;
.sw
.LP
dom and ran are respectively the domain and range of a relation.
.sv lpf
fun dom f =
		let 	val x = freev "x" [f]
			and y = freev "y" [f]
		in	comp (x,\*k(y,opair (Var x) (Var y) \(mo f))
		end;
fun ran f =	let 	val x = freev "x" [f]
			and y = freev "y" [f]
		in	comp (x,\*k(y,opair (Var y) (Var x) \(mo f))
		end;
.sw
.KE
.KS
.LP
The following defines the property of being a single valued relation
(many-one).
.sv lpf
fun is_sv a =	let	val x = freev "x" [a]
				and y = freev "y" [a]
				and z = freev "z" [a]
			in	is_rel a \*e
			\*j(x,\*j(y,\*j(z,
			(opair (Var x) (Var y) \(mo a) \*e
			(opair (Var x) (Var z) \(mo a) \(rh ((Var y) == (Var z)))))
		end;

.sw
.LP
The following function is the domain restriction of a relation.
The domain restriction of r to d is the class of ordered pairs in r whose
left member is in d.
.sv lpf
fun dom_restr r d =
	let	val x = freev "x" [r,d]
		and y = freev "y" [r,d]
	in	comp(x, (Var x) \(mo r \*e (left (Var x) \(mo d))
	end;
.sw
.LP
Relational override is defined by a domain restriction and a union.
.sv lpf
fun rel_over r1 r2 = \(cu (pair (dom_restr r1 (dom r2)) r2);
.sw
.LP
Relational update is a version of override for a single value.
.sv lpf
fun rel_update r1 a v = rel_over r1 (opair a v);
.sw
.KE
.KS
.NH
THE ABSTRACT DATA TYPE THEOREM
.LP
The set theory is formalised as a hilbert style axiom system by defining
an abstract data type of theorems, where theorems are represented
by formulae.
.KE
.KS
.NH 2
Inference Rules
.LP
Inference rules are formalised as functions from theorems to theorems,
and axioms schemata as functions on any type yeilding theorems.
.KE
.sv lpf
end; (* of FTM *)
structure THM = struct
local open FTM in
abstype theorem = \*o of formula
with
.sw
.KS
.NH 3
Modus Ponens
.LP
Modus Ponens takes two theorems of the form \*o A, \*o A \(rh B and returns
\*o B.
If the second theorem is not of the correct form then it will just return
the first.
This preserves the soundness of the logic while avoiding the extra
complexity of exception handling.
.sv lpf
fun	MP (\*o A) (\*o (op \(rh (B,C)))	= if A=B then  \*o C else  \*o A			|
	MP x y			= x;
.sw
.KE
.KS
.NH 3
Generalisation
.LP
UI takes as parameters a theorem and a variable name, returning
a generalisation of the theorem.
.sv lpf
fun UI (\*o A) x = \*o (\*j(x,A));
.sw
.KE
.KS
.NH 2
Propositional Axioms
.LP
These propositional axiom schemata are parameterised by arbitrary formulae.
.sv lpf
fun P1 A B		= \*o ((A \(rh B) \(rh A);
fun P2 A B C	= \*o ((A \(rh B \(rh C) \(rh (A \(rh B) \(rh (A \(rh C));
fun P3 A B		= \*o ((\(no A \(rh \(no B) \(rh (B \(rh A));
.sw
.KE
.KS
.NH 2
Axioms of Quantification
.LP
In the quantification schemata A and B are arbitrary formulae, x is
a variable name and t a term.
Instead of rejecting combinations which would not be sound variables
will be renamed (by priming) as appropriate to arrive at a valid instance.
.sv lpf
fun Q1 A x t	= \*o (\*j(x,A) \(rh (t subs_for x inn A));
fun Q2 A x		= \*o (A \(rh \*j(primed x (freevars A),A));
fun Q3 A B x	= \*o (\*j(x,A \(rh B) \(rh \*j(x,A) \(rh \*j(x,B));
.sw
.KE
.KS
.NH 2
Equality and Membership
.LP
Equality need not be primitive, axiom EQ could be replaced by a similar
definition in the metalanguage.
.sv lpf
fun EQ a b x	=
			let	val nx = freev x [a,b]
			in	\*o ((a==b) \*h (\*j(nx,
					(Var nx \(mo a \*h Var nx \(mo b))))
			end;
fun EXT a b x	=
			let	val nx = freev x [a,b]
			in	\*o ((a==b) \*h (\*j(nx,
					(a \(mo (Var nx) \*h b \(mo (Var nx)))))
			end;

.sw
.KE
.KS
.NH 2
Comprehension
.LP
By contrast with Zermelo-Fraenkel we have comprehension rather than
separation.
This is sound because a comprehension does not always yield a set,
it may yield a class, and because, as the following axiom states,
it yields a class which contains just those sets which satisfy the
predicate.
Classes are never members of anything, hence the class of all sets
which are not members of themselves is not a member of itself.
.sv lpf
fun COM x p	= \*o (\*j (x,set (Var x) \*e p \*h (Var x) \(mo comp(x,p)));
.sw
.KE
.KS
.NH 2
Sets
.LP
The empty class is a set, as is the pair formed from any two sets.
This latter axiom may be redundant.
.sv lpf
fun S\(es x		= \*o (set \(es);
fun Spair a b	= \*o (set a \*e set b \(rh set (pair a b));
.sw
.KE
.KS
.NH 2
Universes and Closure
.LP
The function U maps each set onto a universe containing it.
A universe is a transitive set (every member of it is a subset of it)
closed under the set forming operations of Zermelo-Fraenkel, viz 
power set formation, union, and replacement.
These axioms imply also closure under separation, pairing, and choice
from non-empty sets.
The availability of classes makes the statement of the replacement
axiom smoother.
.KE
.LP
Urep looks slightly stronger than the equivalent closure condition
in Cohn, since it asserts that the range of the function is in the
same universe as the domain, Cohn merely states that the union of
the range is in the universe and that the range itself is a set.
.sv lpf
fun Umem u	= \*o (set u \(rh u \(mo (V u) \*e set (V u));
fun Utrans u x	= \*o (x \(mo (V u) \(rh x \(ib (V u));
fun Upower u a	= \*o (a \(mo (V u) \(rh (\*m a \(mo (V u)));
fun Union u a	= \*o (a \(mo (V u) \(rh (\(cu a \(mo (V u)));
fun Urep u f	= \*o (is_sv f \*e (dom f) \(mo (V u) \*e (ran f) \(ib (V u)
			\(rh	(ran f) \(mo (V u));
.sw
.KS
.NH 2
Choice
.LP
The choice function maps every non-empty class onto a member of itself.
It maps the empty set onto an unspecified class.
.LP
.KE
This formulation of the choice axiom is in the first clause like the
usual formulation for ZF.
The second clause is my innovation, in order to ensure that the value
obtained on application of a partial function to an element outside its
domain is distinct from any element in its range.
(it is \(*m \(es, which is by this axiom a proper class and hence may not
be in the range of any function).
.sv lpf
fun CH t = \*o ((set (\(*m t) \*h (\(no (t == \(es)))
			\*e ((\(no (t == \(es)) \*h (\(*m t) \(mo t));
.sw
.KS
.NH 2
Foundation
.LP
The axiom of foundation is needed to permit inductive definitions.
.sv lpf
fun FO t =	let	val y = primed "y" (term_freevars t)
		in	\*o (t==\(es \*d
			\*k(y,Var y \(mo t \*e (\(ca (pair t (Var y)) == \(es)))
		end;
.sw
.KE
.KS
.NH 2
Extracting the Formula from a Theorem
.LP
The following procedure allows inspection of the content of a theorem from outside the abstract data type.
.sv lpf
fun formula(\*o t) = t;
.sw
.KE
.KS
.NH 2
End of Abstract Data Type
.LP
.sv lpf
end; (* of local clause *)
end; (* of abstract data type *)
end; (* of structure THM *)
end; (* of structure UST *)
open UST.FTM UST.THM;
.sw
.KE
.KS
.LP
The types inferred by the SML compiler were:
.DS L
> type theorem
  type var = string
  datatype term = V of term | Var of var | \(*m of term | comp of var * formula
  datatype ('a,'b) inc = inn of 'a * 'b
  datatype formula = \*j of var * formula | == of term * term | \(rh of formula *
 formula | \(mo of term * term | \(no of formula
  val Utrans = fn : term \(-> (term \(-> theorem)
  val Urep = fn : term \(-> (term \(-> theorem)
  val Upower = fn : term \(-> (term \(-> theorem)
  val Union = fn : term \(-> (term \(-> theorem)
  val Umem = fn : term \(-> theorem
  val UI = fn : theorem \(-> (var \(-> theorem)
  val Spair = fn : term \(-> (term \(-> theorem)
  val S\(es = fn : 'a \(-> theorem
  val Q3 = fn : formula \(-> (formula \(-> (var \(-> theorem))
  val Q2 = fn : formula \(-> (string \(-> theorem)
  val Q1 = fn : formula \(-> (var \(-> (term \(-> theorem))
  val P3 = fn : formula \(-> (formula \(-> theorem)
  val P2 = fn : formula \(-> (formula \(-> (formula \(-> theorem))
  val P1 = fn : formula \(-> (formula \(-> theorem)
  val MP = fn : theorem \(-> (theorem \(-> theorem)
  val FO = fn : term \(-> theorem
  val EXT = fn : term \(-> (term \(-> (string \(-> theorem))
  val EQ = fn : term \(-> (term \(-> (string \(-> theorem))
  val COM = fn : var \(-> (formula \(-> theorem)
  val CH = fn : term \(-> theorem
  con \(no = fn : formula \(-> formula
  val unit = fn : term \(-> term
  val term_list_freevars = fn : (term list) \(-> (var list)
  val term_freevars = fn : term \(-> (var list)
  val t_subs_for = fn : (term * ((var,term) inc)) \(-> term
  val subs_for = fn : (term * ((var,formula) inc)) \(-> formula
  val set = fn : term \(-> formula
  val right = fn : term \(-> term
  val rel_update = fn : term \(-> (term \(-> (term \(-> term))
  val rel_over = fn : term \(-> (term \(-> term)
  val ran = fn : term \(-> term
  val primed = fn : string \(-> ((string list) \(-> string)
  val pair = fn : term \(-> (term \(-> term)
  val opair = fn : term \(-> (term \(-> term)
  val m\(cu = fn : (('a list) list) \(-> ('a list)
  val left = fn : term \(-> term
  val is_sv = fn : term \(-> formula
  val is_rel = fn : term \(-> formula
  con inn = fn : ('a * 'b) \(-> (('a,'b) inc)
  val freevars = fn : formula \(-> (var list)
  val freev = fn : string \(-> ((term list) \(-> string)
  val dom_restr = fn : term \(-> (term \(-> term)
  val dom = fn : term \(-> term
  val curried_t_subs = fn : term \(-> (var \(-> (term \(-> term))
  val curried_subs = fn : term \(-> (var \(-> (formula \(-> formula))
  con comp = fn : (var * formula) \(-> term
  val \*d = fn : (formula * formula) \(-> formula
  con \(mo = fn : (term * term) \(-> formula
  val \(ib = fn : (term * term) \(-> formula
  val \(es = comp ("x",\(no(== (Var "x",Var "x"))) : term
  val \(cu = fn : term \(-> term
  val \(ca = fn : term \(-> term
  con \(*m = fn : term \(-> term
  val \(*e = fn : (''a * (''a list)) \(-> bool
  val \*m = fn : term \(-> term
  val \*k = fn : (var * formula) \(-> formula
  con Var = fn : var \(-> term
  con V = fn : term \(-> term
  con \(rh = fn : (formula * formula) \(-> formula
  con == = fn : (term * term) \(-> formula
  val \*h = fn : (formula * formula) \(-> formula
  val \*e = fn : (formula * formula) \(-> formula
  val -- = fn : ((''a list) * ''a) \(-> (''a list)
  con \*j = fn : (var * formula) \(-> formula
.DE
.KE