There is a section of personal data (with random links), (or you can see my curriculum vita curriculum vita (with publication list), a section on my theoretical research in Quine's "New Foundations" and related systems. . Here is the page for my current theorem proving project Marcel. There is access to documents from the latter two sections. Here is my latest theorem proving project, an implementation of a variant of Automath. Information about my book (including the errata slip) is here.

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.

### Set theory textbook

Here are the notes from M502, Logic and Set Theory, which constitute my logic textbook under construction. My elementary set theory book using NFU which has been published is discussed below.

utilities

## Teaching Stuff --Spring 2019

• General information and office hours -- to be updated.

• Math 311: Here is the syllabus. Here is the class announcements page.

• Math 287: Here is the syllabus. Here is the class announcements page.

## Theorem Proving Projects

• Marcel: Here is the page for my current theorem proving project Marcel. There is access to documents from the latter two sections.

• Gottlob: Here is the page for my current theorem proving project Gottlob. This is an implementation of the logic of Frege, made consistent by the application of stratification restrictions, as proposed by Nino Cocchiarella. A curious fact is that the underlying logic is almost the same as that of the latest version of Marcel, though notationally it is very different as Frege's 2D notation is supported (for output only).

• 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.

## NF Consistency Proof

I have claimed since 2010 to be in possession of a proof of the consistency of Quine's set theory New Foundations. I maintain various versions of this proof here: every now and then I have had to declutter this space. The proof is complex and I freely admit to having severe problems with seeing how to present it.

Here is a fresh take from January 2019, driven by an abstract picture of a scheme for successively adding desired bijections to a specific kind of FM model. Underneath it is the same argument, but I am trying for less mystery. Currently, I have replaced this with the large type version I am presenting to Thomas Forster in slides (and revising as I go; this is the very latest news as I write 5/23/2019).

Here is a compressed version of the document above, more paper-like (31 pages). Here are the slides for the talk I gave about the proof in Leeds on 5 June 2019.

Here is a purported draft of the proof of the existence of a model of tangled type theory (and thus of Con(NF)).

Here are notes from my summer 2018 visit to Cambridge, involving simplifications of notation, a simplification of the argument, and possibly a reduction in consistency strength to roughly the expected level. These notes are fresh text and so may contain slips and typos, and they are not equipped with the self-contained apparatus of a paper as yet. Here is a further Summer 2018 document in which the FM construction is presented in an abstract way without particular reference to the NF application (and indeed it does have applications to some other related problems).

Here is another rewrite, from January 2018, motivated by a desire to move considerations about clan indices as late as possible in the argument. This is just a zeroth draft of the description of the construction of a tangled web without framing language about how this is used to prove Con(NF), which would be just as in previous versions. The notation in this document is very different from that in the version just below, but the construction and the underlying argument are in fact virtually the same (and could easily be made exactly the same) in a suitable abstract sense: this is strictly a matter of exposition, but improving exposition is a serious issue here.

Here is a completely fresh rewrite of the entire argument, with similar notation and proofs to recent drafts, but an entirely different rhetorical approach: there is no foreshadowing, and on the whole no discussion of intentions. I dive right into the construction and argue forward to the conclusion. This fixes a bug at the very last step of the argument in the just previous draft, it should be noted (which I will fix in the version with repairs). This document is also much shorter than the recent drafts of the submitted paper.

Here is a direct argument for the existence of a model of tangled type theory, similar in approach to the argument just above in some respects, but also similar in essential ways to earlier attempts to build a model of tangled type theory directly. This approach is ghastly in ways which will be evident on reading it, but may have formal advantages.

Here is a possibly useful intuitive overview of the main construction as presented in versions (III(a)) and (IV) below. It's a companion piece to the paper, intended to provide motivations without full arguments whose details become appalling...

As of 3/25/2017, I provide a key to versions. (I) is an ancient version which I preserve because Nathan Bowler's group read it. (II) is the version first submitted to a journal. (IIa) corrects some problems with (II) that I found when preparing (III). (III) is a version with a considerably simplified argument which has been presented to the journal as replacing (II). (IIIa) is a version of (III) with a local correction to one argument. (IV) is a further version with a simplified version of the construction of set parents already suggested in (I).

• This (submissiondraftalt.pdf (III)) is what I think is a notably simplified version of the submitted version just below. The structure built is exactly the same, but the bookkeeping of atoms in clans is slightly different, and the definition of the structure is given in a way which enormously simplifies the recursion in the definition and considerably simplifies the proofs that it works. There still may be some need to revise text carried forward from the version below for compatibility with the new approach. For the moment I am not making such corrections as this is the version now in the hands of referees; a version with such corrections might appear at this point if I become aware of a need for enough of them.

This (aslnfslides.pdf) is my set of slides for the talk I'll give at the ASL meeting. They are too long, but might be handy as an overview of the proof. (Typos found during the actual delivery of the talk corrected: indeed the notes were too long!)

• This (submissiondraftalt-with-a-repair.pdf (IIIa)) is the version at the top with a repair to the argument on pp. 38-42 with changes in the text indicated in the footnotes: reasoning steps valid in submissiondraft.pdf because of global induction hypotheses have to be enforced by requiring that objects discussed be strongly symmetric. Some other minor repairs have been made, indicated by footnotes.

• This (submissiondraftalt-smallparentsets.pdf (IV)) is a version rewritten using the simpler definition of parent sets which is suggested in the other versions after the main construction. There does seem to be some gain from using it. The error fixed in the version just above was discovered while preparing this version (which doesn't have that issue because the argument for sizes of strongly symmetric power sets is a bit simpler).

• This (submissiondraft.pdf (II)) 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. This is the version which has been submitted to a journal.

This (submissiondraft-with-repairs.pdf (IIa)) is a version of the file immediately above which corrects or least remarks on slips in that version which I found in the course of preparing the version now at the top. I commend the version at the top to the reader, but I continue to believe that the argument of this version is basically correct and I'll maintain this for now and update it as required. The argument in the version at the top is simplified, and the bookkeeping is being done differently, but the same system of clans and permutations is intended to be described.

• Here (tellthestory.pdf (I)) 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.
If you have an amateur philosophical interest in NF, I do not think it likely that you will get anything out of these very technical and not yet very polished documents (in any version), and I am not likely to answer your questions about them. Be advised that in my opinion (which I know is not universal) the famed NF consistency problem has nothing at all to do with philosophical issues which Quine's set theory might be taken to address: I think that NFU addresses these issues to exactly the same extent and its consistency and mathematical strength have been settled issues since 1969.

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.

## New: my book to be available on-line in a new edition

I have permission from my publisher to post a revised version of my book Elementary Set Theory with a Universal Set (which has gone out of print) online. This PDF version is the result of a first pass through the text in November 2012 with the aim of preparing an official online second edition. I thank my publishers for their kindness in allowing me to maintain an online version, both to conveniently publicize error corrections and to make the work available now that it is out of print. Since I am currently actively working on editing an official second edition (I really am, as of November 2012), communications about errors and infelicities would be very welcome!

## Drafts of Current Work

Here is the brief demonstration that parameter-free Zermelo set theory is the same as full Zermelo set theory: parameterfree.pdf

Here is my latest draft (summer 2017) on representation of functions in third order logic, in a stable version for those currently reading it. Here is my very latest draft (with ongoing revisions)

Here find an outline of a proposed approach to semantics for the Principia Mathematica (PM) of Russell and Whitehead using the type and substitution algorithms in my paper on automated polymorphic type inference in PM. Here find some notes on PM with page references related to the same analysis.

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 a computer implementation of these ideas.

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 is a still more recent version.

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 find a summary of my thoughts on the correct default foundations in the style of Zermelo. In spite of being an NF-iste, I do think that Zermelo-style foundations are the best. However, I think that the axiom of replacement is so strong that it should not be part of the default foundations. In particular, I do not think that the axiom of replacement is justified by the intuition of the cumulative hierarchy; it is a far stronger principle.

## Miscellaneous Documents

Just what the section title says. These are various drafts I keep in public view. Some very old things have been hanging around here for quite a while: as I update in January 2011 I am removing most of them, but I may add more.

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 my latest draft (summer 2017) on representation of functions in third order logic.

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.

Materials relating to the visit of Olivier Esser are here.

## Other Stuff

If you want to send mail to me at holmes@math.boisestate.edu, feel free!

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).

## Loglan, an artificial human language

For several years, I have been the "chief executive officer" (a grander designation than is perhaps appropriate) of The Loglan Institute, the nonprofit organization which attempts to guide the development of the artificial language Loglan. This language was originally proposed by James Cooke Brown in the 1950's as a vehicle for testing the Sapir-Whorf hypothesis (look it up!) A specific peculiarity of this language is that it is (at least in intention) syntactically unambiguous: the official version of the language is unambiguously machine parsable. The language is intended to be highly logical: it is to some extent an implementation of first-order logic in a spoken language.

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.

## Watson Theorem Prover Project

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 project. 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.

## Education in Virtual Worlds?

Note the question mark. I'm not gung ho on this subject, but I have spent some time investigating the question of whether and how well mathematics (and other content) could be taught in online environments such as Second Life. I participated in the class Teaching and Learning in Second Life taught by Lisa Dawley in the Boise State Educational Technology Program in 2009 (?). I think a major (perhaps the major) technical problem with teaching math in SL has to do with the difficulty of freehand drawing in SL, and I developed a tool in Second Life which (almost) addresses this. There is a blog entry about a presentation on this problem. In spring 2010 I taught a class in SL called Teaching Mathematics in Virtual Worlds, through the Educational Technology Department here. I'm currently practicing my Loglan in weekly conversation meetings in Second Life, but not there much otherwise; I remain interested in doing some experiments on representing Calculus III concepts in the 3D virtual world.

## The Strictly False Programming Language (frivolous)

I have designed an eccentric programming language (Strictly False) an extension of Wouter van Oortmerssen's elegant False programming language. The source (in Standard ML) is here and the documentation (PDF) is here.. Any BSU student who writes a program in False or Strictly False which does something interesting can come and see me for praise [you can get a DOS False interpreter off the site I cite; to run my interpreter (and my language is definitely more powerful), you need Moscow ML].

## The Definition of Planet (frivolous)

Definitions are important to mathematicians, and fools rush in where angels fear to tread, so here find my modest proposal for the definition of "planet" with comments on why the definitions lately proposed by the IAU are not so good.