Overview of Randall Holmes's Home Page
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
utilities
Teaching Stuff
- General Information and office hours: My office is Mathematics 240A. My office telephone number is 426-3011.
I am teaching Math 314, Real Analysis, TTh 12--1:15 MB 124 and Math 406, Advanced Number Theory, WF 10:30--11:45 MB 139. I am also the "instructor" for Math 488, the outcomes assessment exam; if you are enrolled for this, you will get email about it.
I participate in the logic seminar, which meets 3-4 PM W in MB124. I am tentatively defining my office hours as 9:15 -- 11:45 am TTh, 9:15 -- 10:15 am WF, 3 -- 5 pm TF (not WTh). I expect not to be routinely on campus at all on Mondays, though you are welcome to request an appointment if you need to meet me on a Monday. I expect to be around most of the day TWThF.
- Math 314: More information about this course I am teaching in Spring 2016 as it develops.
Here is the syllabus. Please note that the electronic syllabus is the official syllabus (paper copies will not be distributed) and is subject to change at my discretion (with reasonable notice).
Here is the Math 314 class announcements page. Information and course materials for this class will be posted here: it is a good idea to look at this page frequently.
- Math 406: More information about this course I am teaching in Spring 2016 as it develops.
Here is the syllabus. Please note that the electronic syllabus is the official syllabus (paper copies will not be distributed) and is subject to change at my discretion (with reasonable notice).
Here is the Math 406 class announcements page. Information and course materials for this class will be posted here: it is a good idea to look at this page frequently.
- Old courses: Follow this link.
NF Consistency Proof
I currently claim to have a proof of the consistency of New Foundations. As of 11/5/2015, I reduced the clutter of Versions to two, the version read earlier by Nathan Bowler's group, and my then latest version which takes a similar approach, but there is a newer one that I am working on
in January 2016, and new clutter of slides and working notes at the bottom.
- This (abstractclans.pdf) is a version I have been working on most recently. See the remarks for the description of differences: this looks quite different because we do not need to construct codes for atoms and parent sets before introducing them.
- This (lotsofatoms.pdf) is my pending main version. It includes a construction of a model of tangled type theory and a construction of the traditional sort of FM model with clans and parent sets: the traditional construction is Improved (less coding) and presented first.
- This (thepaper.pdf) is my current main version. It includes a construction of a model of tangled type theory and a construction of the traditional sort of FM model with clans and parent sets. This version and various slides provided below were infected by some errors I introduced in attempts to simplify the construction. These documents should be corrected: the one above should be better.
- This (basicfm.pdf) is a new version of the "traditional" argument (as exemplified by the last paper below, the one read by Nathan Bowler and his group). This version reduces the difficulty of the "elementarity argument" by suitably exploiting the fact that most parent sets are the same size to replace elementary embeddings with isomorphisms. Latest update 11/5/2015, with a considerable modification of the core construction of codes and clans in parallel. I no longer consider it the main version: it needs serious updating re the termination of the recursion involved in the definition of equivalence of codes (which is supplied, at least in intention in the version above).
- 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.
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.
Here (newslides1-working.pdf) are the slides for the presentation I recently gave to the Boise set theory group. The soundness of the recursive definition of equivalence of codes is not adequately explained (it is sound, but requires more attention).
Here are a set of slides for the lecture to the Boise state logic group on 2/3/2016, a better organized account of the basic construction of codes for atoms and elements of parent sets. The construction is fine but the argument that the recursion defining equivalence of codes is sound requires more work. This is addressed in the first paper above, which uses basically the same construction in the second part.
Here is an older and here is a newer account of the central recursive construction of codes for atoms and elements of parent sets, including the current version of the proof of soundness of the definition of equivalence between codes.
Here are some working notes of mine, on ``tangled types" and on the construction of the system of clans, parent sets, litters and atoms. No guarantees are attached to these notes. They might reveal something about my motivations, and the second sketches a different order of presentation of the main proof (dependent on importing some proofs given in the main papers).
Here is another set of working notes, on a direct construction of a model of tangled type theory.
This is my most recent explicitly philosophical essay about Quine-style set theory.
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 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 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). This version is ready for submission.
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.
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 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.
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 (DVI
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.