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

The Definition of Planet

Teaching Stuff

• General Information: A schedule of assignments and academic deadlines for both classes is here. Information about my schedule and office hours will appear here. Some preliminary information: I will have my main office hours 10:15--11:15 MTWF (please note -- this is changed (again)). Additonal hours will be 1-2 MWF: my graduate student has priority for the use of these hours and may bump you. I have a piano lesson W 2:30-3 pm which will often go until 3:15 or so. I may sometimes have to deliver my child to school at 8:30 or pick him up at 3:30 pm; this is unpredictable. I plan to normally walk to school (arriving 7:40 or so) on MWF, and take driving duty followed by a trip to the gym on TTh (so I might not be here until 10 am or so on T and even later on Th).

• Math 175, Calculus II: Here is the syllabus.

  Here is an old test I and another old Test I. You should be able to recognize problems which are not on our agenda. There will be some definite integration by substitution on our test which was not on these tests: for that your homework is not a bad model.

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

  Here is a test II review document. No test I had looked in the least like the one you are going to have, so I selected all questions that looked reasonable.

  Here are the Test II grades posted by the ID number on your paper.

  Here is a test III review document.

  Handwritten solutions to the Test III review and your 8.2 homework are at my door (4:30 pm Tuesday)

  Here are the Test III grades.

  Here is an additional worksheet for section 8.3.

  Here is the practice exam for Test IV, NOW WITH SOLUTIONS. I've just finished marking 8.7 and the papers will be by my office door by 8:30 or so. I graded number 8 (hint: check the endpoints: it also converges at -1) and number 40 (hint: in number 39 you can find an exact value for the series; the series in 40 has as its exact value the integral of the exact value found in 39). The results were not encouraging: you need to study similar problems found in the practice exam... I remind you that I will be out of town all day Friday: Dr. Kerr is proctoring the exam.

  Test IV grades are here...

  sample final 1, sample final 2

  Here is a detailed review sheet for the final, reviewing what you should cover in each section and containing recommended problems from the book to review for a couple of sections. Good luck on the final! I will be holding regular office hours (and some extended hours) during the early part of next week.

• Math 502, Logic and Set Theory: Here is the syllabus.

  Here find the draft lecture notes for the class. These notes are the textbook (and will continue to develop).

  Jan 27: I've changed strategy for notes updates: I've added a first subsection to the notes themselves describing version changes with dates. And of course the date of the current version is on the title page. All notes updates that were on the web page have been copied into the file.

  Here is Homework 1. It is due next Tuesday. Two refinements to the instructions (REVISED!): do not use de Morgan's laws (or the corresponding rules about negation of quantifiers); I originally said here you couldn't use equivalence of an implication with its contrapositive, but I have changed my mind: you may use modus tollens and you may prove an implication by proving its contrapositive. Reason directly rather than indirectly where possible (problem 1 can be done with no mention of any negation at all; problems 2 and 3 do need some proof by contradiction or other indirection). Bring proofs around to show to me at least once in the coming week.

  Here is Homework 2. It was originally due Tuesday Feb. 12 but is now due Thursday Feb. 14: not enough people have been to see me and those who have needed advice. There is also another slight update: the stated type of the set of natural numbers was wrong (it should be k+3). I will rewrite the handout; check for a new version.

  Here is Homework 3. This will be due Tuesday, February 26th. Please note the statement that you do not need to do all the problems on this sheet to get a good grade on the assignment. But there is quite a lot to do; start right away!

  Here is Homework 4. This will be due Tuesday, March 11, after your exam on Thursday, March 6, but please note that this material is fair game for that exam!

  Here is Homework 5. This will be due Thursday after Spring Break. It is not impossible that I will add additional material to this assignment during this week, so keep an eye on it.

  Here is the belated Homework 6. This will be due Tuesday, April 22.

  Here is Homework 7, which will be due the last day of class. I'm hoping to give one more assignment which will be due at the final.

  Here is the computer lab. The assigned exercises are due electronically by the end of finals week.

  Here is Test II, a take home due the last day of finals. Please read the instructions carefully before concluding that you have an absurd amount to do: there are 7 questions but you only need to do 4 of them (not an arbitrarily chosen 4, though, thus read the directions). I encourage you to finish up Homework 6 and 7.

  Here is the catalog statement:

  Math 502 Logic and Set Theory (3-0-3)(S)(even-numbered years). This course is structured as three 5-week components: formal logic, set theory, and topics to be determined by the instructor. The logic component will include: formalization of language and proof, the completeness theorem, the Lowenheim-Skolem Theorem. The set theory component will include: cardinality, Cantor's theorem, well-orderings, ordinals, the transfinite recursion theorem, the Axiom of Choice and its equivalents. PREREQ: Math 314.

• Math 593, Thesis: I am supervising 5 credits of thesis for a graduate student, who will receive his instructions here.

  set theory sequent rules with assignment

• Fall 2007 classes: Look at the end of the old courses document (follow the link just below).

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

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 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?