An axiomatic development in ProofPowerHOL of a higher order theory of wellfounded sets.
This is similar to a higher order ZFC strengthened by the assertion that every set is a member of some other set which is
a (standard) model of ZFC.

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 wellfounded 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 wellfounded 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 wellfounded, 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 {\ProductHOL} 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 higherorder axiom
(axiom schemes are not supported by {\Product}.
The last is a finite axiomatisation based on one originating with Holmes.

Explorations into the possibility of contructing nonwellfounded foundations systems which are ontologically category theoretic
and include a category of all categories.

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

Formal models of various aspects of XLogic 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 wellorderings prepared by Rob Arthan for possible inclusion in the ProofPower theory of ordered
sets.
The second is material on wellfoundedness, 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 coinductive 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, well founded relations and a recursion theorem.

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}.

Formal models of aspects of Metaphysical Positivism

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.
