forked from Randall-Holmes/Randall-Holmes.github.io
-
Notifications
You must be signed in to change notification settings - Fork 0
/
index.html
333 lines (214 loc) · 23.2 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
<!-- saved from url=(0035)http://math.boisestate.edu/~holmes/ -->
<html><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8"></head><body>
<H3> Redirect Notice</H3>
<B>If this is not where you expected to find yourself, this is because my university page has been abandoned and now redirects to here. The directory structure of the new page is different, so you have been directed to the top of the page. The visible structure of the page and its subpages are similar to the old one, so you should be able to find the resource you want. Send me email if you have trouble. The university page with its redirect will disappear in the next few months some time.</B>
<h1>Overview of Randall Holmes's Home Page</h1>
<p>
<p>
<img src="mini-me.jpg" width="200" align="top"> Just so you know who you are really dealing with...
<p>
I'm (Melvin) Randall Holmes, a professor of mathematics at Boise State University in Boise Idaho since 1991.
My research is in systems of set theory or combinatory logic related to Quine's set theory New Foundations,
with a sideline in computer-assisted reasoning. I have a general somewhat more than amateur interest in the
history and philosophy of mathematics, particularly mathematical logic.<p>
This is a version of my home page under my own control. It largely mirrors but does not exactly mirror
my former university home page.
It will contain some material found in my page at the university
which will appear familiar; other material (either outdated or inconvenient to import to the new location) will
not be reproduced. The original page is now redirected to here (queries to most subdirectories of the original page will come right here, because the internal structure of this page is different). Queries to my Loglan resources at Boise State will go to the root Loglan page here.<p>
Here is my very ancient <a href = "Personal/personaldata.html">personal data page</a>,
which is not very serious and has a lot of broken links because it is ancient and needs to be fixed.<p>
You can see my curriculum vita <a href="https://Randall-Holmes.github.io/holmesvita.pdf">curriculum vita
(with publication list</a>)<p>
Here is the <a href="https://Randall-Holmes.github.io/Bibliography/setbiblio.html">universal set
bibliography</a> (an expansion of the bibliography of Forster's NF book).
I have an obligation to do some updating here.<p>
<a href = "nfsummary.html">Here</a> is a <b>largely outdated</b> blurb about my NF activities, which I preserve for revision.
</p><p>
<A href="nf.html">Here</a> is my old home page for New Foundations, which is referenced here just so I can go in and fix it. It is very old...<p>
<a href="https://Randall-Holmes.github.io/Loglan/cefli.html">Here</a> is my new separate page on the artificial language Loglan.
<H3>Set theory textbook</H3>
<a href="https://Randall-Holmes.github.io/proofsetslogic.pdf">Here</a> 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.
</p><p>
<H2>Teaching Stuff --Fall 2020</H2>
<UL>
<p> Information about my fall 2020 classes is pending.
</p></li><li>Old courses: Follow <a href="http://math.boisestate.edu/~holmes/portfolios.html">this link</a>.
</li></ul>
<H2>Theorem Proving Projects</H2>
<UL>
<LI><B>Marcel:</B> Here is the page for my current theorem proving project <a href="https://Randall-Holmes.github.io/Marcel/marcel.html">Marcel</a>. There is access to documents from the latter two sections.<p>
<LI><B>Gottlob:</B> Here is the page for my current theorem proving project <a href="https://Randall-Holmes.github.io/Gottlob/gottlob.html">Gottlob</a>. This is an implementation of the logic of Frege, made consistent by the application of stratification restrictions, as proposed by Nino Cocchiarella. A curious fact is that the underlying logic is almost the same as that of the latest version of Marcel, though notationally it is very different as Frege's 2D notation is supported (for output only).<p>
<LI><B>Lestrade: </B> <a href="https://Randall-Holmes.github.io/Lestrade/automath.html">Here</a> is my latest theorem proving project, an implementation of a variant of Automath.<p>
<LI><B>Watson:</B> Here is the link to the page for my old theorem prover project Watson:
<a href="https://Randall-Holmes.github.io/Watson/proverpage.html">Watson theorem prover page.</a>
I am planning to incorporate some features of this system into my current projects.
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.<p>
<LI><B>RTT:</B> <a href = "RTT/rttcover.html">Here</a> is the material on my polymorphic typechecker for the ramified type theory of Principia Mathematica.<p>
</UL>
<h2>NF Consistency Proof</h2>
<CENTER><EM>I have discovered the consistency of New Foundations -- it is like custard!</EM>: Jesse Holmes</CENTER><p>
I have claimed since 2010 to be in possession of a proof of the consistency of Quine's set theory New Foundations. I maintain various versions of this proof here: every now and then I have had to declutter this space. The proof is complex and I freely admit to having severe problems with seeing how to present it.<p>
<A HREF="https://Randall-Holmes.github.io/Nfproof/newattempt.pdf">Here</A> is a fresh version from April 2020.
I am hoping this will be a bit easier to follow than earlier versions;
I do some clearly indicated foreshadowing of impossible things that turn out to be all true in the end,
which might help with motivation when I am doing the honest construction.<p>
<A HREF="https://Randall-Holmes.github.io/Nfproof/tangles.pdf">Here</A> is a purported draft of the proof of the existence of a model of tangled type theory (and thus of Con(NF)).<p>
As of 3/25/2017, I provide a key to versions. (I) is an ancient version which I preserve because Nathan Bowler's group read it.
(II) is the version first submitted to a journal.
(IIa) corrects some problems with (II) that I found when preparing (III).
(III) is a version with a considerably simplified argument which has been presented to the journal as replacing (II).
(IIIa) is a version of (III) with a local correction to one argument.
(IV) is a further version with a simplified version of the construction of set parents already suggested in (I).<p>
These numbered versions are all quite old now, and I would recommend sticking to the April 2020 version.<p>
<UL>
<LI> <A HREF ="https://Randall-Holmes.github.io/Nfproof/submissiondraftalt.pdf">This (<TT>submissiondraftalt.pdf</TT> (III))</A> is what I think is a notably simplified version of the submitted version just below. The structure built is exactly the same, but the bookkeeping of atoms in clans is slightly different, and the definition of the structure is given in a way which enormously simplifies the recursion in the definition and considerably simplifies the proofs that it works. There still may be some need to revise text carried forward from the version below for compatibility with the new approach. For the moment I am not making such corrections as this is the version now in the hands of referees; a version with such corrections might appear at this point if I become aware of a need for enough of them.<p>
<LI> <A HREF ="https://Randall-Holmes.github.io/Nfproof/submissiondraftalt-with-a-repair.pdf">This (<TT>submissiondraftalt-with-a-repair.pdf</TT> (IIIa))</A> is the version at the top with a repair to the argument on pp. 38-42 with changes in the text indicated in the footnotes: reasoning steps valid in <TT>submissiondraft.pdf</TT> because of global induction hypotheses have to be enforced by requiring that objects discussed be strongly symmetric. Some other minor repairs have been made, indicated by footnotes.<p>
<LI> <A HREF ="https://Randall-Holmes.github.io/Nfproof/submissiondraftalt-smallparentsets.pdf">This (<TT>submissiondraftalt-smallparentsets.pdf</TT> (IV))</A> is a version rewritten using the simpler definition of parent sets which is suggested in the other versions after the main construction. There does seem to be some gain from using it. The error fixed in the version just above was discovered while preparing this version (which doesn't have that issue because the argument for sizes of strongly symmetric power sets is a bit simpler).<p>
<p>
<LI> <A HREF ="https://Randall-Holmes.github.io/Nfproof/submissiondraft.pdf">This (<TT>submissiondraft.pdf</TT> (II))</A> is a full version based on my working notes during my Cambridge visit in May and June 2016. I believe this is the best approach. There is no recursive horror of construction of codes for all the atoms and elements of the parent sets of atoms (if you have read those versions you know what I mean). In fact, this version very much resembles the way I originally thought of the construction -- but with clearer understanding of how it goes, I believe I have avoided circular explanations. It is still nasty. This is the version which has been submitted to a journal.<p>
<A HREF ="https/Randall-Holmes.github.io/Nfproof/submissiondraft-with-repairs.pdf">This (<TT>submissiondraft-with-repairs.pdf</TT> (IIa))</A> is a version of the file immediately above which corrects or least remarks on slips in that version which I found in the course of preparing the version now at the top. I commend the version at the top to the reader, but I continue to believe that the argument of this version is basically correct and I'll maintain this for now and update it as required. The argument in the version at the top is simplified, and the bookkeeping is being done differently, but the same system of clans and permutations is intended to be described.<p>
<p>
<LI> <a href="http://Randall-Holmes.github.io/Nfproof/tellthestory.pdf">Here (<TT>tellthestory.pdf</TT> (I))</a> 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.<p>
<LI> If anyone wants information about the status of other versions previously posted here, please ask me. I reduced them again in preparing the Github version of this page.
</UL>
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.
</p><p>
<a href="https://Randall-Holmes.github.io/Nfproof/nftalk2013.pdf">Here</a> 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.
<p><a href="https://Randall-Holmes.github.io/Nfproof/thehamburgslides.pdf">Here (<TT>theslides.pdf</TT>)</a> 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.<p>
<p><a href="https://Randall-Holmes.github.io/Papers/foundations3.pdf">This</a> is my most recent explicitly philosophical essay about Quine-style set theory.
<p> I have removed a lot of links to various drafts in constructing the new page. Such drafts still exist on my university computer but are not present here. You may inquire about them if necessary.
</p><p>
</p><h2>My published book is available on-line in a corrected edition</h2>
<p>
<img src="Lecahier10.gif" width="200" align="top"> Look Mom, I wrote a <EM>book</EM>! (jumps up and down)
<p>
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 <a href="https://Randall-Holmes.github.io/head.pdf">PDF version</a>
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.<p>
Communications about errors and infelicities would be very welcome!<p>
<h2>Drafts of Current Work (and not so current work)</h2>
Here are <A HREF="Drafts/naivecategories.pdf">some notes on category theory in NF</a>, a current preoccupation of mine. <a href="Drafts/tstjcat.pdf">Here</a> is another draft on the same subject.<p>
Here is <A HREF="Drafts/nfuexplanation.pdf">a talk</A> I gave recently to the local seminar on resolving the paradoxes in NFU.
There isn't anything very novel about it: it was really intended as an example to address questions by a philosopher about
whether discussions of avoidance of the paradoxes are explanations of why we regard a theory as reliable (the usual way in
which resolutions of the paradoxes in NFU are discussed is not really motivated in this way).
Here are <A HREF="Drafts/typedfoundations.pdf">some notes</A> about foundations in type theory and NF(U) which are
altogether more serious in intent, although they should be regarded as a negative indexed draft which might contain
genuine howlers ;-)<p>
Here is the brief demonstration that parameter-free Zermelo set theory is the same as full Zermelo set theory:
<a href="Drafts/parameterfree.pdf">parameterfree.pdf</a><p>
Here is <a href="Drafts/functionsin3dorder-submitted.pdf">my submitted draft (2018)</a>
on representation of functions in third order logic (this paper has appeared).
<a href="Drafts/functionsin3dorder-best-slides.pdf">Here</a>
are the slides for my BEST talk about this.<p>
<p>
<a href="Drafts/pmsemantics.pdf">Here</a> 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.
<a href="Drafts/notesonpm.pdf">Here</a> find some notes on PM with page references related to the same analysis.<p>
<A HREF = "Drafts/pm-no-compromise.pdf">Here</A> 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.
<p>
<a href="Gottlob/fregenote.pdf">Here</a> find an outline of how to fix the foundational system of Frege
using stratification in the style of Quine. <a href="Gottlob/frege2.pdf">Here</a>
find another approach to the same subject.
<a href="Gottlob/gottlob.html">Here</a> find a computer implementation of these ideas.
</p><p>
<a href="Drafts/zfcminusext.pdf">Here</a> find my current notes on Dana Scott's
lovely and weird result that ZFC minus extensionality has the same strength as Zermelo set theory.
</p><p>
<a href="Drafts/acyclic_abstract_final_revision.pdf">Here</a>
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.
</p><p>
<a href="Drafts/symmetryrevisited.pdf">Here</a> is the submitted (2020) draft of the paper I am writing about
a simpler form of symmetric comprehension equivalent to NF. <a href="Drafts/symmetryrevisited2.pdf">Here</a> is a companion piece
describing a weaker version of symmetric comprehension which gives a theory inessentially stronger than NF3, with a model construction.<p>
</p><p>
<a href="Drafts/hereditary.pdf">Here</a>
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.
</p><p>
</p><p>
<a href="Drafts/hierarchy.pdf">Here</a> find a summary of my thoughts
on the correct default foundations in the style of Zermelo.
In spite of being an NF-iste, I do think that Zermelo-style foundations are the best.
However, I think that the axiom of replacement is so strong that it should not be part of the default foundations.
In particular, I do not think that the axiom of replacement is justified by the intuition of the cumulative hierarchy;
it is a far stronger principle.
</p><p>
Here is a <a href="Drafts/preserves3.pdf">version</a> 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.
</p><p>
I should put a link to my SEP article on Alternative Axiomatic Set Theories here.
</p><p>
<a href = "coislides.pdf">Here</a> are the slides for a talk I gave for students at the College of Idaho, which includes a cleverly minimalist representation of the reals.<p>
Here are my notes on <a href="Drafts/newbracket.pdf">efficient
bracket abstraction</a>. Here is a brief related note on
<a href="Drafts/thereisnoproblemofvariables.pdf">eliminating bound variables from syntax</a>.
<p> Here is a very old note on <a href="Drafts/concepts.pdf">Quine's calculus of concepts</a> which perhaps should be dusted off. Here is <a href="Drafts/concepts_sequent.pdf">another</a><p>
<p> <A HREF="Drafts/define_equality.pdf">Here</a> is a note on defining equality as indiscernibility in NF and related theories.<p>
Here is a <a href="http://math.boisestate.edu/~holmes/holmes/ackermann.txt">letter</a>
of mine discussing the set theory of Ackermann. Here are some not very serious notes on a <a href="http://math.boisestate.edu/~holmes/holmes/pocket.txt">pocket
set theory</a>. Here is a <a href="http://math.boisestate.edu/~holmes/holmes/pocket.pdf">later version (PDF
file)</a>.
<h2> Repository of papers </h2>
<a href = "Papers/papers.html">Here</a> find a
rather disorganized directory of PDFs of my papers, some published versions and some late drafts.<p>
</p><h2>Loglan, an artificial human language</h2>
<p>
<img src="cover-art.png" width="200" align="top"> The place to start...
<p>
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.
<p>
Here is <a href="http://www.loglan.org/">the official web site of the Loglan
Institute</a>. Here is <a href="http://math.boisestate.edu/~holmes/loglan.org/welcome.html">the mirror of
the Loglan web site at Boise State</a>. There is access to a wide variety of information, documents and software through these links.
</p><p>
<a href="Loglan/cefli.html">Here</a>
is my new separate page on Loglan, where you can find pointers to my current Loglan projects.
</p><h2>Watson Theorem Prover Project</h2>
Here is the link to the page for my old theorem prover project Watson: <a href="Watson/proverpage.html">Watson
theorem prover page.</a> 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.
<h2>Education in Virtual Worlds?</h2>
<!-- <p>
<img src="Teacher 1.png" width="200" align="top"> Professor Leslie Beaumont examines a
student creation on EdTech Island, the former Boise State extension in Second Life.
<p> -->
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 <a href="http://www.secondlife.com/">Second Life</a>. I participated in the class <a href="http://lisadawley.googlepages.com/597SLsyllabus.htm">Teaching and
Learning in Second Life</a> taught by Lisa <span class="SpellE">Dawley</span> 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. In spring 2010 I taught a class in SL
called <a href ="Teaching Math in Virtual Worlds.html">Teaching Mathematics in Virtual Worlds</a>, through the Educational
Technology Department here. Here are <a href = "TMVW talk slides.odp">the slides</a> for a talk I gave about this class at the VWBPE conference in SL in 2011(?). I'm currently practicing my <span class="SpellE">Loglan</span>
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.
<h2>The Strictly False Programming Language (frivolous)</h2>
I have designed an eccentric programming language (Strictly False) an
extension of Wouter van Oortmerssen's
elegant <a href="http://wouter.fov120.com/false/">False
programming language</a>. The source (in Standard ML) is <a href="purefalse.sml">here</a> and the
documentation (PDF) is <a href="sfdocs.pdf">here.</a>. 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 <a href="http://www.itu.dk/~sestoft/mosml.html">Moscow ML</a>].
<h2>The Definition of Planet (frivolous)</h2>
Definitions are important to mathematicians, and fools rush in where angels fear to tread, so
<a href="planet.html">here</a> find my modest proposal for the definition of "planet" with
comments on why the definitions lately proposed by the IAU are not so good.
</body></html>