Some presentations, given or in preparation,

A description of the problems I am working on and an index to the documents in which that work is progressing.

This paper is my second approach to set theory conceived as a maximal consistent theory of set comprehension. The principle innovation in this version is to simplify the syntax by removing comprehension, so that the syntactic category of term is no longer required.

An axiomatic development in ProofPower-HOL of a higher order set theory.

This document is an exploration into formalisation of geometric algebra and analysis using surreal numbers instead of real numbers.

This paper is concerned with set theory conceived as a maximal consistent theory of set comprehension. This is interpreted by looking for large subdomains of a notation for infinitary comprehension, and the theory is developed from such interpretations.

This document is concerned with the specification of an interpretation of the first order language of set theory. The purpose of this is to provide an ontological basis for foundation systems suitable for the formal derivation of mathematics. The ontology is to include the pure well-founded sets of rank up to some arbitrary large cardinal together with the graphs of the polymorphic functions definable in a polymorphic functional language such as ML, and the categories corresponding to abstract mathematical concepts. The interpretation is constructed by defining ``names'' or ``representatives'' for the sets in the domain of discourse by transfinite inductive definition in the context of a suitably large collection of pure well-founded sets. A membership relation and a equality congruence are then defined simultaneously over this domain, so that the domain of the new intepretation is a collection of equivalence classes of these representatives. Relative to a natural semantic for the names, the definitions of these is not well-founded, and special measures are required to obtain a fixed point for the defining functional. These include choice of a suitable boolean algebra of truth values for the defined relations, and the location of a suitable subdomain of the representatives.

Three formalisations in {\Product-HOL} are undertaken of NFU and NF. One is based on Hailperin's axioms. Another tries to follow Quine's original formulation by expressing stratified comprehension as a single higher-order axiom (axiom schemes are not supported by {\Product}. The last is a finite axiomatisation based on one originating with Holmes.

In well-founded set theories there is no category of (all) categories. This is one aspect of a wider collection of issues which might be raised against the foundation of mathematics exclusively on well-founded sets. More commonly perhaps, the failure of the notion of cardinal numbers as equivalence classes under equipollence, may be thought the primary motivation for considering non-well-founded set theories. Here we investigate non-well-founded ontoloyies without seeking new ways of representing numbers, but rather in order to have richer ontological support for abstract mathematics. There are two aims for this document concerned with the category of categories. The more ambitious and exotic, perhaps even frivolouw, is the construction of a category theoretic foundational ontology which might serve as an alternative to the established ontology of well-foundewd sets. This itself does not dewmand a departure from well-foundedness, but in our case we add the additional requirement that there be a category of all categories and more generally that the disctions between large and small categories which are necessary in well-founded set theories are rendered nugatory by the existence of categories encompassing the totality of relevant kinds of mathematical structures (e.g. a category corresponding to each kind of algebra). Though in this we aim for a category theoretic foundation which stands on its own (rather than being based on a set theory) we need a meta-language to describe this system and the ontology of that meta-language will include a non-well-founded set theory. This set theory will also be expected to have a category of categories. The exploration involves more than one set theoretic starting point, and more than one way of constructing concrete category theoretic structures from the chosen set theories. The interest is primarily in systems which combine a substantial collection of well-founded entities with a non-well-founded ontology including a universal set or category.

Formalisation of some of the concepts of category theory in {\ProductHOL}.

Formal models of various aspects of X-Logic in Z

An introductory illustrated description of ProofPower (not progressed far enough to be useful).

History and rationale of the development of ProofPower.

An analysis of the ideas behind the engineering of a proof tool to support the Z specification language by semantic embedding into HOL. From the ideas of Leibniz via the creation of the new academic disciplines, first of Mathematical Logic and then of Computer Science, we trace the roots of one small step in the mechanisation of reason.

This document provides facilities for automatic reasoning based on backward chaining. They are intended to be similar in capability to refutation proof procedures such as resolution or semantic tableau, but in order to fit in better with interactive proof in ProofPower are not refutation oriented. The main target is a backchaining facility which searches for a proof of the conclusion of the current goal from premises and rules drawn from the assumptions and elsewhere.

Theorem proving in ProofPower is heavily based on rewriting which is supported by term nets which partially match the rewriting rules against target terms. To provide a higher level of automation using unification, closer to the power of modern predicate calculus automation present in other implementations of HOL term nets which unify rather than match, and which also produce antiunifiers have been considered here. This is mainly design, and though there is a very crude implementation, this is for evaluation only and would not deliver reasonable performance.

Several structures providing tactics, tacticals, etc. for theories, forward chaining, backward chaining, theory trawling et.al.

This document consists of two parts. The first is a theory of well-orderings prepared by Rob Arthan for possible inclusion in the ProofPower theory of ordered sets. The second is material on well-foundedness, mainly consisting in the proof of the recursion theorem which is needed for consistency proofs of definitions by transfinite recursion respecting (if that's the right term) some well founded relationship.

This document provides examples of the use of the facilities provided in t007.doc.

Systematic facilities for a range of different kinds of inductive and co-inductive definitions of sets and types in ProofPower HOL.

This document contains things used by my other theories which do not particularly belong in them. Definitions or theorems which arguably belong in a theory already produced by someone else.

Fixed Points and Well Founded Relations

A queer way of doing set theory in HOL (together with some queer reasons for doing it that way).

The theory of real vector spaces, norms and derivatives of functions between normed vector spaces as required for formal modelling of some physical theories.

This document provides an example illustrating a method of formalising physical theories, together with a discussion of some aspects of {\it semantic positivism}.

Some generic formal models of abstract semantics.

If you have ProofPower and some extra mathematical theories available from the Lemma1 web site then this tarball can be used to rerun (and tamper with if you like) the material in all these documents.