Collected papers

Some of these may be published versions, some may be late drafts.

In some cases, I am uncertain which is the best version. This explains some apparent duplications.

Set theory, philosophical or survey pieces
The first two are on the philosophical motivation for NF. The last two are general surveys of alternative set theories.
Miscellaneous logic and set theory
- representation of functions and relations in third order logic and this.
  it does have a connection to NF3, of course, but it is not really an NF paper.
- The set of sets hereditarily of size less than kappa exists in ZF
Stratified combinatory logic and lambda-calculus
This was the original program of my thesis, and led to the Watson program.
The Urysohn paper
This was an isolated foray into mainstream mathematics. The paper is based on my Masters thesis. My advisor admitted later that it was really a PhD thesis, but it would have been quite disastrous for me to get a PhD thesis in functional analysis...without knowing any functional analysis!
- the Urysohn space and its embeddings into Banach spaces and this and this.
Set theory (stratified or typed)
This has been my main line of work. Substantial time spent thinking about the model theory of NFU is manifest in the strong axioms paper, with a footnote in the paper about models preserving information. The tangled type theory paper is the start of my main line of attack on the consistency problem for NF itself. The other papers touch on other consistent fragments of NF or important techniques in NF. The acyclic comprehension paper is about a very peculiar proposal about the axiomatics of NFU...which turns out to work perfectly. The Tarski's Theorem and NFU paper is an oddment.
- Strong axioms of infinity in NFU with errata corrected
- The usual model construction for NFU preserves information
  Also this: preserves3 seems to be the submitted version; I have no idea what preserves4 actually is in versioning terms.
- tangled type theory
- cahiers 7 article on modelling fragments of NF
- subsystems of NF with predicativity restrictions
- permutation methods in NF(U) with Forster
- forcing in NFU and NF
- there is a Forster term model of TST
- The acyclic comprehension paper with Zuhair and Nathan.
- Tarski's theorem and NFU and this.
Double extension set theory
- Paradoxes in double extension set theories
- the structure of the ordinals in double extension set theory
The ramified theory of types of Russell
- subsystems of NF with predicativity restrictions
  This paper also appears under the general NF set theory heading, but it says something about the type theory of PM.
- type checking the ramified type theory of PM also this and this and this and this.
  This is the version of the paper I packed with the sources (visible in my RTT directory).
Theories of sets and classes with a symmetry criterion for sethood: these lead to versions of NF.
- the first symmetric comprehension paper, with superclasses
- the second symmetric comprehension paper, no superclasses
The Watson theorem prover
- the Watson theorem prover
- Disguising recursively chained rewrite rules as equational theorems (the tactic language of Watson)
- a strong and mechanizable grand logic (the logic of Watson)
  This also appeared under stratified lambda calculus above. The untyped lambda calculus paper which appears there also mentions Watson but seems less a Watson paper than this one.
Master's theses of my students (there are three, putting one up now with this reminder to myself)

the raw list