Here is the New Foundations Home Page (NF home page is extremely out of date and needs to be edited, note to self August 2014). Here is the universal set bibliography (an expansion of the bibliography of Forster's NF book). For information about my claim to have proved the consistency of New Foundations, see below.

Here find the slides for my recent talk at the College of Idaho. I'm very pleased with the construction of the reals given there, using neither ordered pairs nor equivalence classes!

Here is my new separate page on the artificial language Loglan.

**General Information and office hours:**My office is Mathematics 240A. My office telephone number is 426-3011. I am teaching Math 187 and Math 414/514 in Fall 2016. Math 187 meets MWF at 1:30-2:20 pm in Mathematics room 139. Math 414 meets MWF at 10:30-11:45 am in Mathematics room 124. I am planning in general terms to be on campus 9 am-4 pm MWF (specific office hours will be stated later); it remains to be seen at what times (if any) I will be routinely on campus on TTh. There will be office hours on at least one of those days, though.**Math 187:**Foundational and Discrete Mathematics, which I will be teaching this fall. This is your syllabus. This is your class announcements page.**Math 414/514:**Real Analysis, which I will be teaching this fall. This is your syllabus. This is your class announcements page.- Old courses: Follow this link.

**Marcel:**Here is the page for my current theorem proving project Marcel. There is access to documents from the latter two sections.**Lestrade:**Here is my latest theorem proving project, an implementation of a variant of Automath.**Watson:**Here is the link to the page for my old theorem prover project Watson: Watson theorem prover page. I am planning to incorporate some features of this system into my current projects. This project was funded for some time by the Department of Defense; I have not worked directly on it for years, but I have not forgotten about it entirely.

- This (
`clandescription.pdf`) is a full version based on my working notes during my Cambridge visit in May and June 2016. I believe this is the best approach. There is no recursive horror of construction of codes for all the atoms and elements of the parent sets of atoms (if you have read those versions you know what I mean). In fact, this version very much resembles the way I originally thought of the construction -- but with clearer understanding of how it goes, I believe I have avoided circular explanations. It is still nasty. The main construction chapter of this paper is still a very recent draft and may have stupid mistakes of the kind found in early drafts.During this visit I refined my updated version of a class theory with a symmetric comprehension for sets (here

- This (
`lotsofatoms.pdf`) This version contains a construction similar to the construction above but using the recursively horrible coding functions at the outset, and an attempt at a direct construction of a model of tangled type theory. I preserve it because someone was reading it until recently, and also because of the ideas in the tangled type theory section. - Here (
`tellthestory.pdf`) is an older official document (using tangled webs), which uses quite complex coding. This document has been read by Nathan Bowler's group in Hamburg, and they profess to understand most of it. An error in the "elementarity argument" required a correction. In the newer version above the whole issue of the "elementarity argument" is finessed. - If anyone wants information about the status of other versions previously posted here, please ask me.

Here is the talk I gave on New Foundations to the department at Boise State on September 10, 2013. Philosophical interests in NF might be served by these slides, and also by the notes on Frege's logic which appear below.

Here (`theslides.pdf`) are the notes for the talk I
gave at the University of Hamburg on June 24, 2015. These have now been extended to a (quite long) full discussion of the proof -- this
was done by incorporating a large final segment of the current version of the paper, which needs to be further formatted and cut.

This is my most recent explicitly philosophical essay about Quine-style set theory.

6/4/2016 I have removed various items from here. They still exist: in fact, they are still in the directory pointed to by the links. You may also inquire about them if you are interested.

Here find an essay on the ontological commitments of PM and why substitutional quantification does work there and doesn't save you from serious ontological commitments. The flavor of my remarks is admittedly rather bad-tempered; a great deal of nonsense is written about PM.

Here find an outline of how to fix the foundational system of Frege using stratification in the style of Quine. Here find another approach to the same subject.

Here find my current notes on Dana Scott's lovely and weird result that ZFC minus extensionality has the same strength as Zermelo set theory.

Here is the May 19th 2011 (submitted) version of the paper I am writing about Zuhair al-Johar's proposal of "acyclic comprehension", with Zuhair and Nathan Bowler as co-authors, a perhaps surprising reformulation of stratified comprehension.

Here is the Jan 20 2012 draft of the paper I am writing about a simpler form of symmetric comprehension, strong versions of which give extensions of NF with semantic motivation and a weaker version of which gives a new consistent fragment of NF inessentially stronger than NF3, for which I give a model construction. The problem of modelling the versions that yield NF seems to be very hard (as usual). Here is a more recent version with better results on the form of the symmetric comprehension axiom (fewer type levels needed).

Here find the note submitted Dec 30 2013 on my result that the set H(|X|) of all sets hereditarily smaller in size than a set X exists, not using Choice. It is surprising to me that this is not an obvious result, but the references for partial results that I have been able to find are recent, so perhaps it is new.

Here is a recent version of my manual of logical style, a teaching tool (or would-be teaching tool) with which I am constantly tinkering to try to give students some idea how to approach the precipice of writing a proof.

Here is a draft paper on mathematics in three types (mostly, on defining functions in three types) based on a presentation at BEST 2009. Here are the notes for the talk I gave on this subject in Edmonton on Sept 11 2012.Here is a version of my paper on the curious fact that the urelements in the usual models of NFU turn out to be inhomogeous, because the membership relation on the underlying model-with-automorphism of the usual set theory turns out to be definable in NFU terms. This version corrects a couple of annoying typos in the published version.

I will put a link to my SEP article on Alternative Axiomatic Set Theories here.

Here are my notes on efficient bracket abstraction. Here is a brief related note on eliminating bound variables from syntax.

Here are the notes for the visit of Peter Seymour.

Materials relating to the visit of Olivier Esser are here.

Here's a link to the Department of Mathematics and Computer Science Home Page here at Boise State!

Here is a letter of mine discussing the set theory of Ackermann. Here are some not very serious notes on a pocket set theory. Here is a later version (PDF file).

Here is the official web site of the Loglan Institute.. Here is the mirror of the Loglan web site here at Boise State. There is access to a wide variety of information, documents and software through these links.

Here is my new separate page on Loglan, where you can find pointers to my current Loglan projects.