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.

Some notes on methods for formal verification of system architecture in the context of Model Based Systems Engineering.

This document serves to establish what characters render like in utf8 ProofPower documents prepared using lualatex.

This paper explores some ideas for providing general support in HOL for structures defined by transfinite induction, by exploiting a strong infinity axiom expressed in terms of a well-ordering on a new type of "'a ordinals".

Another approach to illative combinatory logic, based this time on the hol4 example on pure combinatory logic. Mainly an attempt to understand why that example is so much simpler than my own efforts.

An exploration of axiomatic method using ProofPower.

A broad discussion of ontologies for mathematics and abstract semantics.

A discussion of formal semantics and semantic embedding.

This is a formal exploration with ProofPower of a topic addressed by {\O}ystein Linnebo in a paper under the same title.

A partly formal discussion of modal concepts leading to a discussion of certain kinds of metaphysics.

This is a second exploratory approach to Universal Algebra.

This theory is for miscellanea which depend upon well-founded set theory with urelements (GSU). It also has misc1 as a parent.

This is a modification of the pure set theory GS to admit urelements.

This is an approach to illative lambda-calculi via construction of an infinitary calculus in a well-founded set theory.

Some preliminary explorative modelling of electronic circuits.

This is a limited development of universal algebra and lattice theory for the purposes of X-Logic.

At present this document is a (small) mess pot of explorations of how one might go about presentation of Church's Simple Theory of Types and ultimately ProofPower HOL using Standard ML and/or ProofPower HOL. I am interested both in exposing exactly what Church said, comparing the details of his system with those of ProofPower HOL and discussing the reasons for the differences, but also I am looking for an interesting and digestible way of presenting ProofPower HOL to philosophers or other groups without much IT background. Its doubtful that all these objectives are compatible, and so far my attempts have not been in the least impressive, but I probably will keep picking at it and may eventually come up with something useful.

Formal analysis (using Higher Order Logic with ProofPower) and commentary on Grice's system Q (G, $G_{HP}$) first presented in his paper \emph{Vacuous Names}.

A place to play formally with the concept of proposition. This actually started as a formal look at some of Harvey Friedman's ideas, particularly his concept calculus but also BRT theory, and I think somehow I got the idea that the relevance of this to me was something to do with propositions. Anyway, it hasn't really got anywhere.

Formal models of aspects of the Logic and Metaphysics of Gottfried Wilhelm Leibniz.

The abstract syntax and semantics of Pure Type Systems and HOL-Omega in a formal higher-order theory of well-founded sets.

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

The introductory chapter to the second part of Analyses of Analysis.

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. Since I moved my non-well-founded foundational work back from set theory to combinatory logic using version of well-founded set theory with urelements it has been necessary to replicate those definitions required which depend upon well-founded set theory in the context of this other version of well founded set theory. For that reason this document is in the process of being restructured as three theories, one of material which does not depend on the well founded set theory, and one for materials dependent respectively on each of the two versions of well-founded set theory. These are the theories misc1, misc2 and misc3.

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 theory of well-founded 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 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, 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.