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).
Time Commitments: I have a class 12:40-1:30 pm MWF and a class 7-8:50 pm TTh. I have a piano lesson T 1:30-2. I have logic seminar T 2:40-3:30: it is best to assume I am not available 2:40-5 T. There are often department meetings 2:30 Th. I am not available 4-6 Th, whether in my office or not: I am participating in an online class at that time.
Official Office Hours: I have office hours for M170 6:15-6:45 pm and 9-9:30 pm TTh. I have office hours for M314 11-12 am MWF. Students from one class are welcome to attend the hours of the other but notice that hours for a class are cancelled on the day of a test for that class.
Other Times: I may work at home some days; I will try to make it clearer what my habits are in that respect as things develop. At this point I am expecting (usually but not always) to be on campus by 9:30 am if not earlier on MWF. I may sometimes work at home unless and until I need to come to campus for a meeting or seminar on TTh, but I am now leaning toward coming in at 9 or 9:30 most days.
If you want to look at likely future homework (or if I'm behind on posting it) you can look at my fall 2007 assignment schedule.
I post some Test I papers from past semesters. These will not have pictures in them! summer 2003; spring 2005; fall 2007.
Don't expect graded papers to appear: I have been ill for the last two days, and I have asked Dr. Kerr to proctor the exam tonight. Do note that there are no office hours today: this is in the syllabus...but in fact I will not be there at all, as I am ill...
The grades for Test I are here, posted by the ID number on your test.
Here is the most recent Test II. another. another. another. None of these have exactly the same coverage as our Test II, but they are similar.
Here are the Test II grades. Sorry these took so long to get out; I have been distracted by personal things and very tired.
Here are some sample Test III papers. Test III, spring 2005; Test III, summer 2003; Test III, fall 2002; Test III, summer 2002; Test III, fall 2007; Test III makeup from Fall 2007; Test III makeup review problems with solutions as usual solutions requiring pics are not there;I will do them in class, on request.
Here are the solutions to the worksheet (problems assigned from sample tests). The illustrations are not very good.
Here are the Test III grades. It's been graded since Sunday; I seem to have zoned out when I went to put up the link...if you want to know your current standing in the course, you can visit me at the office or inquire using your offical Boise State email.
Here find the lecture notes for my Spring 2009 Math 387 course. Readings may be assigned from here (for logic). Look at the course schedule for specific assignments.
Here is a set of notes on proof strategy I wrote for an earlier M314 class.
Here is your first homework assignment, assigned the 28th and due in a week.
Here are some examples of propositional logic proofs. The examples from Monday's lecture will appear later.
Here are NOTES COMPLETE UP TO FRIDAY THE 4TH (except that I didnt put in the proof of the associative law). You also might want to look at the Math 502 notes (above in my web page) and the 2004 Math 387 notes (below in my web page).
Here is Homework II, due on the 11th.
The due date for Homework II has been extended to Wednesday, and I will be in my office MT 9-12 to consult about Homework II and about Homework I rewrites.
Here are the solutions to Homework I.
Here are the solutions to Homework 2
Here is Practice Test I. I might add more problems during the week.
Writing at 1230 pm, Sunday, I have finished marking Homework 4. There is one nameless paper; if you think it is yours get in touch with me. Your percentage homework grade is written on your H4 paper. The papers will be at the door of my office as soon as I get to the university: I will leave soon after I write this. I will mark the H3 updates later this afternoon. I am sorry that this was such a slow process. You can turn in rewrites of H4 up to 1:15 T (and I will be in my office 10:40-1:15 T): looking at the inclass activity, I think some of you should be able to rewrite the limit proofs profitably. Solutions to H3 will be posted soon, and solutions to the practice test when I have typeset them.
Here are the Homework 3 solutions.
Practice test solutions will appear this afternoon. All outstanding homework is at my door.
Practice test now has some but not all solutions. Here are solutions to Homework 4.
Here are the Test I grades posted by the ID number on your paper.
Here are some notes on the least upper bound concept. The notes are now complete up to a discussion of problem 14 section 8.
Here are notes on the bisection method (problems 15 and 16 from chapter 8). Here are the homework 5 solutions; no notes on the proof of the Chain Rule yet (soon); I hope you don't bring rotten fruit to throw at me ;-)
Here are the practice problems for Test II. Some of these may literally be questions on Test II. Be aware that Test II will now be on the Monday after break; a take-home portion of Test II may be posted on Friday. Please note that when the solutions to Homework 6 are posted, they will include some practice work (I state some parts of solutions and ask you to fill in others).
Homework 6 papers are at my door, as are the remaining H5 rewrites. Note that I changed the grading base from 30 to 25 (but did not give grades over 100). The Homework 6 solutions for problems not graded will be posted shortly (except for 11.6). I'm thinking of accepting rewrites until some point during the break when I will post the solutions to the graded problems.
Here are the solutions to bits of Homework 6 which are not graded and not takehome bits of the exam. 11.6 will be the basis for the takehome problem on Test II: I will talk about this today. I will post a document with hints and instructions about the takehome today or tomorrow. Rewrites will be accepted (either under my door or electronically) until Wednesday 5 pm during break: Wednesday night I will post the complete Homework 6 solutions (except for 11.6). The inclass exam is Monday after break, if you haven't noticed yet. I still owe you a few more notes on various things.
Here is the text of the Test II takehome problem (now with typo pointed out by alert student corrected). You may not ask anyone but me for help or advice on this problem. Please note that I have made the instructions more precise: I expect you to fill in the exact partial proof outline I gave in class, which is reproduced on this document. This is due at the beginning of the inclass exam Monday after break.
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!).
Since I am currently actively working on editing an official second edition, any comments from readers about errors and infelicities would be very welcome!
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).
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.