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 wellordering 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 wellfounded 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 lambdacalculi via construction of an infinitary calculus
in a wellfounded set theory.

Some preliminary explorative modelling of electronic circuits.

This is a limited development of universal algebra and lattice theory for the purposes
of XLogic.

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 HOLOmega in a formal higherorder
theory of wellfounded sets.

Formal models of aspects of the Tractatus LogicoPhilosophicus 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 wellfounded set
theories, but not specific to that work, which make use of galactic set theory or
fixed point theory.
Since I moved my nonwellfounded foundational work back from set theory to combinatory
logic using version of wellfounded set theory with urelements it has been necessary
to replicate those definitions required which depend upon wellfounded 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 wellfounded 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.
