Overview of Randall Holmes's Home Page

There is a section of personal data (with random links), (or you can see my curriculum vita (with publication list) ; also I have a Facebook profile...) a section on my theoretical research in Quine's "New Foundations" and related systems and a section on my theorem prover Watson (formerly Mark2) . Here is the NEW page for my current theorem proving project Marcel. There is access to documents from the latter two sections. Information about my book (including the errata slip) is here. A sketchy section on QED exists.

Here is the Jewish Philosophy Class home page.

Here is the New Foundations Home Page. Here is the universal set bibliography (an expansion of the bibliography of Forster's NF book).

Utilities

Logic and Set Theory Notes

Teaching Stuff

• Summer class: Math 333, section 031: This is Math 333, Differential Equations. A syllabus is here! A schedule is here, containing academic deadlines, test dates, and homework assignments.

  My office hours are officially 10:00-11:30 am MWTh. On Tuesday I have a piano lesson at 10 am. I may add afternoon office hours later, but for the moment I will be leaving campus fairly quickly at 1:30, as my wife is convalescing from surgery.

  I have found the old tests! 2002 test 1; spring 2003 test 1; fall 2003 test 1: happy studying! The test will cover 2.1-6 (exclusive of 2.3 not covered).

  Here are the Test I grades posted by the ID number on your test.

  Here are some sample Test II papers. Coverage cannot be expected to be identical to ours. Our test will go from 2.9 to 4.5 (and of course only cover sections we have actually talked about). first sample paper; second sample paper; third sample paper. I have a couple of other old Test II's that I do not like.

• Old courses: Follow this link

Student Research Project Space

Most resources are now found on the new Marcel home page.

This directory is now the home of current files for this project.

Here is a file of examples for Mark Stewart (though anyone may try them of course). I will add more to this file (further additions July 3).

The Spring 2004 Math 387 lecture notes. This should be useful background material. It contains sequent logic theory (along with a natural deduction system) and some prover examples (no guarantee as to how those would work with the current version!).

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

Since I am currently actively working on editing an official second edition, any comments from readers about errors and infelicities would be very welcome!

Current Research

Here are the talks from my recent visit to Cambridge and Brussels. I spoke to the logic group at ULB (the Free University of Brussels) on a sequent prover for higher order logic (actually NFU) and to the Cameleon meeting at the University of Cambridge on Mathematics in Three Types. Please note that the proposed definition of function in three types in the previous slides is incorrect in its details; a correct treatment is described in this draft paper (presented at BEST 2009 and being prepared for its proceedings).

Here is the latest draft of the inhomogeneity paper in PDF. I'll keep this updated. Updated further on Dec. 9: there is a highest E-rank, of course, and things are rephrased to reflect this; further, definitions, lemmas, and theorems are identified (there's more structure, so it is easier to tell what I am up to). Further updates Dec. 27 and Dec. 29. Here is a completely rewritten version of this material.

Here is the latest draft of my SEP article in PS and PDF.

Here are my notes on efficient bracket abstraction.

Here are my notes on simulating sequent calculus in algebraic logic. This is a preliminary set of notes; it describes the theoretical basis for an actual implementation of sequent calculus under the Watson theorem prover.

Here are the notes for the current visit of Peter Seymour.

Here find the Moscow ML source (version of January, 2007) for a sequent prover using NFU as its logic, adapted from the sequent calculus for SF in Marcel's cut-elimination paper. NEW: here find some documentation (PDF)! Here find the proof of Cantor's theorem (a theoretically human-readable text document of considerable size) recorded by the prover (this was generated as the result of dialogue between myself and an old version of the prover; it is not an automatically generated proof). Here is a proof (also using an old version of the prover) of a quite different result (that Frege natural numbers are finite cardinals) exhibiting new formatting features of the prover output: the proof

Here (Postscript) and here (LaTeX source)) is the latest version of my paper on symmetry as a criterion for sethood which motivates NF. Here is the next to the last version: here (Postscript)) which contains useful notes on recent changes.

Here are my latest thoughts on the interpretation of ZF in double extension set theory in which interesting properties of the ordinals in double extension set theory are uncovered and used to correct a technical problem with Kisielewicz's interpretation of ZF in double extension set theory. As I explain in the latest version of my paper on paradox in double extension set theory (accepted by Studia Logica, so not appearing here), Kisielewicz's weakest system is not yet known to be inconsistent.

Here is my current work on polymorphic type checking in the ramified theory of types (RTT) of Russell and Whitehead's Principia Mathematica (PM). The paper is now out of zeroth draft and into genuine first draft status!

Materials relating to the recent visit of Olivier Esser are here. These are not complete; I am planning to add more to the notes when time permits (I hope soon, but this has been left hanging for quite a while!).

Here are the slides for my talk at BEST 2001, titled "Could ZFC be inconsistent"? Here are the slides for two talks I gave in Belgium Sept. 20th and Sept 21st, 2002. These are respectively on the inconsistency of the double extension set theory proposed by Kisielewicz (presented to the Groupe de Contact of the F.N.R.S. -- I no longer claim that the weakest of the three systems described is inconsistent, but the proof still works for the other two) and on the status of NFU as a foundation for mathematics (presented to the Belgian Society for Logic and Philosophy).

Other Stuff

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

Under "personal data" you can find information about the dungeon adventure game which I wrote in PC-DOS batch files. You can download the Windows 98 version! Here is an interpreter and debugger for Befunge written in Logo (more info in personal data).

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

If you get here the wrong way and none of the local links seem to work, despair not: click here and things should improve dramatically.

Here is an extended draft of a review of a recent book about the set theory of Paul Finsler.

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

Here are some letters of mine to the FOM (Foundations of Mathematics) list.

For my comments on artificial languages, see the personal data page.

Education in Virtual Worlds?

The Definition of Planet