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

• Math 333, Differential Equations, section 030: Here is the schedule of assignments and academic deadlines. Here is the syllabus.

  Here are some sample test papers. fall 2003; spring 2002; spring 2003; summer 2009. Fully worked out solutions to the 2009 test are here.

  The grades for Test I are here. (really, I fixed the broken link I put up originally)

  Here are some sample Test II papers. No guarantees that they have the exact same coverage! fall 03; summer 09 (likely to be most like yours); spring 03; an old practice test (some of this will look unfamiliar, some of it will be useful); spring 2002; another fall 03.

  (writing Saturday at noon) Just so you know, the homework is at my door. I put it out last night but forgot to post the fact. I kept the few 4.7 papers; I'm checking them off (and not penalizing those who didn't turn in 4.7) but I may want to look them over. Happy studying, and Happy Fourth of July!

  Here are the solutions to the Summer 09 test.

  Here are the Test II grades.

  Here are some sample Test III papers. summer 2009; fall 03; spring 2003. These are all excellent practice papers with the right coverage (except no variation of parameters). The older ones are better in that they have varieties of problem you are likely to see which I did not put on the summer 2009 test. I may post solutions to some or all of these tests; no guarantees.

  Here are the Test III grades.

  Sample test 4 and final exam papers: summer 2009 test 4 and final; fall 2003 final; test 4 fall 2003 (has some stuff in it we haven't done); test 4 spring 2003.

• 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