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.

Formal models of aspects of the Tractatus Logico-Philosophicus and Russell's philosophy of Logical Atomism.

The introductory chapter to the first part of an analytic history of philosophical logic.

Formalisation in higher order logic of parts of Aristotle's logic and metaphysics.

The abstract syntax and semantics of an infinitary first order set theory.

This is my third approach to set theory conceived as a maximal consistent theory of comprehension. It differs from the previous attempt (in t024) by simplification of the treatment of infinitary logic, allowing only a single binary relation.

This theory is for miscellanea which cannot be put in theory ``rbjmisc'' because of dependencies on other theories. It consists primarily of things required in the documents on non well-founded set theories but not specific to that work which make use of galactic set theory or fixed point theory.

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.

Explorations into the possibility of contructing non-well-founded 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 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}.

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.