forked from Randall-Holmes/Randall-Holmes.github.io
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathholmesvita.tex
484 lines (319 loc) · 23.2 KB
/
holmesvita.tex
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
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
\documentstyle[12pt]{article}
\begin{document}
\begin{centering}
{\bf MELVIN RANDALL HOLMES} \\
Dept.\ of Mathematics , Boise State University, Boise ID 83725 \\
Telephone: (208)-426-3011; e-mail {\tt rholmes@boisestate.edu} \\
WWW home page {\tt https://Randall-Holmes.github.io} \\
\end{centering}
\begin{description}
\item[Citizenship:] U.S.A.
\item[Education]
\begin{description}
\item
\item[University of Mons-Hainaut, Mons, Belgium] Postdoctoral Research
with Maurice Boffa, 1990-91.
\item[Cornell University, Ithaca, N.Y.] Postdoctoral Research with
Anil Nerode, 1989-90
\item[State University of New York at Binghamton] Ph.D. in Mathematics
(1990)
\begin{description}
\item[Advisor:] Louis F. McAuley
\item[Dissertation:] Systems of Combinatory Logic Related to Quine's
``New Foundations''
\end{description}
\item[State University of New York at Binghamton] M. A. in Mathematics
(1985)
\begin{description}
\item[Advisor:] Prabir Roy
\item[Thesis:] The Universal Separable Metric
Space of Urysohn
\end{description}
\end{description}
\item[Employment History]
\begin{description}
\item
\item[Boise State University, Boise, Idaho] Associate Professor of
Mathematics, 1997-
\item[Hughes Hall, Cambridge, UK] Visiting Scholar, fall 1998 (sabbatical appointment).
\item[Boise State University, Boise, Idaho] Assistant Professor of
Mathematics, 1991-7
\item[Cornell University, Ithaca, N.Y.] Teaching Associate, Department
of Mathematics 1989-90
\item[State University of New York at Binghamton] Adjunct Lecturer,
Teaching Assistant, Department of Mathematics 1983-89
\end{description}
\newpage
\item[Recent Teaching Assignments]
\begin{enumerate}
\item[]
\item[\bf SP 2013:]
\begin{enumerate}
\item Math 311, Foundations of Geometry. 3 credits, 30 students.
\item Math 187, Discrete and Foundational Mathematics, 4 credits, 28 students.
\end{enumerate}
\item[\bf FA 2012:] In Fall 2012 I was on sabbatical.
\item[\bf SP 2012:]
\begin{enumerate}
\item Math 311, Foundations of Geometry. 3 credits, 23 students.
\item Math 187, Discrete and Foundational Mathematics, 4 credits, 22 students.
\end{enumerate}
\item[\bf FA 2011:]
\begin{enumerate}
\item Math 170, Calculus I, 4 credits, 37 students.
\item Math 314, Foundations of Analysis, 3 credits, 22 students.
\end{enumerate}
\item[\bf SP 2011:]
\begin{enumerate}
\item Math 314, Foundations of Analysis, 3 credits, 30 students.
\item Math 333, Differential Equations, 4 credits, 40 students.
\end{enumerate}
\item[\bf FA 2010:]
\begin{enumerate}
\item Math 170, Calculus I, 4 credits, 40 students.
\item Math 333, Differential Equations, 4 credits, 40 students.
\end{enumerate}
\item[\bf Summers:]
\begin{enumerate} \item[]
\item[\bf SU 2013:] Math 275, Calculus III, 4 credits, 34 students.
\item[\bf SU 2012:] Math 333, Differential Equations, 4 credits, 34 students.
\item[\bf SU 2011:] Math 175, Calculus II, 4 credits, 26 students.
\end{enumerate}
\end{enumerate}
\item[Masters Students Supervised:]
\begin{description}
\item[]
\item[advisor to Joanna Guild:] who defended a thesis titled ``Theorem Proving in Elementary Analysis" successfully on June 7, 2007.
\item[advisor to Cap Petschulat:] who defended a thesis titled ``Transparency in Formal Proof" successfully on May 7, 2009.
\item[on the committee for another Masters student:] I was a member of the committee that examined Trevor Jack May 16, 2008.
\end{description}
\newpage
\item[Service Activities:]
\begin{description}
\item[]
\item[Professional:] I referee papers for journals regularly (I estimate typically three or four referee reports to journals per year). I am a reviewer for Mathematical Reviews. I have served as an external reviewer for a number of tenure and promotion applications at other institutions, and I have been an external examiner for three Ph.D. candidates at other institutions. I maintain web resources, including an extensive online bibliography, for the community of researchers on New Foundations.
\item[Community:] I was invited to give a talk to a seminar for math and physics undergraduates at the College of Idaho on November 8, 2012: my slides for this talk are on my home page. The title was ``A brief history of type theory (or, more honestly, implementing mathematical objects as sets)".
In 2005 I volunteered in the mathematics help room after school at Riverstone Community School weekly for a considerable period. A lot of the help I gave was to the calculus teacher.
\item[Institutional:]
\begin{description}
\item[]
\item[Department:] I am the chair of the Department Concurrent Enrollment Committee, in charge of overseeing evaluation of 11 high school teachers teaching various Boise State classes for dual credit. This involves managing a small budget
and scheduling visits by committee members to many locations each year (many made by me), as well as reviewing new applications to teach Boise State math courses for dual credit. I am the chair of the department Outcomes Assessment committee. I am on the Calculus Curriculum committee. I served two three year terms on the Tenure Progress Review Committee ending in 2012 and in 2004: this committee reviews the progress of untenured tenure track faculty members toward tenure and promotion; part of the duty of a committee member is to observe classes taught by each candidate. I have been on the Math Major committee. I was on the ad hoc steering committee which prepared the department Strategic Plan in 2008.
I was on the Salary and Professional Assignment Committee in 2001. I was on the department Tenure Recommendation Committee in 2000 (at which time I was also on the college tenure and promotion committee).
\item[College:] I was on the Science Division Curriculum Committee from 2005 to 2008. I was on the College Tenure and Promotion Committee in 1999 and 2000.
\item[University:] I was on the University Core Curriculum Committee 2000--2002 and participated in the Core Online project 2000--2001. I was chair of the Honors Program Committee of the Faculty Senate in 1997-8 and participated in the search committee that chose Greg Raymond as Honors Program Director and participated in other Honors Program related service activities at that time.
\end{description}
\end{description}
\newpage
\item[Research Grants]
\begin{description}
\item
\item[1.] ``EFTTP: an interactive equational theorem prover and programming
language'', Army Research Office proposal no. P-33580-MA-DPS (funded
by grant no. DAAH04-93-G-0247, starting date July 1, 1994)
\item[2.] An REU (Research Experience for Undergraduates) award through NSF
EPSCoR during summer 1995, supporting a BSU computer science
undergraduate who implemented an important subset of the prover in
C++.
\item[3.] (with Jim Alves-Foss of the University of Idaho): ``Automated Reasoning using the Mark2 Theorem Prover'', Army Research Office proposal no. P-36291-MA-DPS (funded
by grant no. DAAH04-96-1-0397, starting date August 1, 1996)
\item[4.] ``The Mark2 Theorem Prover'', Army Research Office proposal
number P-37735-MA-DPS (funded by grant no. DAAG55-98-1-0263, starting
date May 15, 1998).
\end{description}
\newpage
\item[Invited Research Presentations]
I have confined myself to presentations of papers given by invitation.
\begin{description}
\item[NF76 workshop, Cambridge University, 27 Mar-2 April 2013:] This workshop at Cambridge University was organized by Thomas Forster; I was the principal speaker, and spoke for several days, as the primary purpose was for me to outline my claimed solution of the consistency problem for New Foundations.
\item[NF 75th Anniversary Workshop, 26-31 March 2012, University of Cambridge:] I gave an invited talk titled "On the Canonical Model of a Symmetric Fragment of New Foundations".
\item[University of Alberta, Sept 11 2012:] I was invited to give a talk on a paper in preparation to the Department of Philosophy at the University of Alberta. I presented ``A treatment of (some) functions in three types".
\item[University of Cambridge, June 26-27 2010] I was invited to serve as external examiner at the PhD defense of Dang Vu and give a talk to a seminar on New Foundations, titled "Symmetry Motivates a New Consistent Fragment of NF and an Extension of NF with Semantic Motivation".
\item[PM 100th Anniversary Workshop, Cambridge, November 27th-28th 2010:] This was held at Trinity College, Cambridge, in honor of the 100th anniversary of the publication of the {\em Principia Mathematica\/} of Russell and Whitehead, a historical milestone for mathematical logic. I was surprised and very honored to be invited to this occasion, and gave a
presentation titled ``Automating the ramified theory of types of Principia", reporting on information found in my publication 20 below, which I believe earned me the invitation.
\item[NF in the Bay Area, Stanford, June 25-27 2008:] Invited to participate, and gave talks on ``Symmetry as a criterion for comprehension motivating NF" (item 24 in my pubs list) and on the paper now titled ``The usual model construction for NFU preserves information" (item 29).
\item[NF 70th Anniversary Meeting, 25-27 May 2007, University of Cambridge:] I presented the paper ``A Forster Term Model of TST" (item 27).
\item[Workshop on the Urysohn Space, 21-24 May 2006] The invitation to this workshop came as a bolt from the blue. I had not thought much about this topic since submitting the research paper summarizing the results of my Masters thesis in 1992, but apparently it has attracted a fair amount of interest. My presentation titled ``The Urysohn Space embeds in Banach Spaces in Just One Way"
(item 25) was an exposition based on my research paper from 1992 on this topic (item 2).
\item[presentation on New Foundations at Idaho State, 2005:] Given by invitation from the COLD project there.
\item[AMS SE section meeting, Atlanta, March 8-10 2002:] ``Mechanization of the System of the Principia Mathematica of Russell and Whitehead (preliminary report)'', invited talk given to a special session on Automated Reasoning.
\item[Istanbul Bilgi University, Istanbul, May 2002:] invited to give talks on NF, ``Two talks on an alternative set theory"
(``Set Theory with a Universal Set
The Quine-Jensen Theory NFU" and ``Foundations of Mathematics in Polymorphic Type Theory" (given May 31; one of these was pitched toward students and one toward faculty) and a talk titled ``The Watson Theorem Prover" for computer scientists. I was there for a week.
\item[Free University of Brussels, Belgium Sept. 18-22, 2002:] I was invited by the university to serve as an examiner at the Ph.D. defense of Armin Rigo and gave two talks -- ``The double extension set theory of Kiseielewicz is inconsistent" to the Logic Contact Group of the FNRS (Belgian national research organization) and ``Foundations of mathematics in polymorphic type theory" to the Belgian Society for Logic and Philosophy.
\end{description}
%\item[Research Interests]
%\begin{description} \item
%\item[Automated reasoning:] now developing a theorem prover under a second successive grant from
%the Army Research Office (source and documentation found on Web page).
%\item[Consistent
%subsystems of Quine's set theory ``New Foundations'';] \item[combinatory
%logic and $\lambda$-calculus:] these and other theoretical interests are combined in the
%higher order logic implemented in the prover.
%\end{description}
\newpage
\item [List of Publications] \begin{description} \item
\item[1.] ``There is a Continuum which is Connected by
Uniformly Short Paths but not Uniformly Path Connected''.
{\em Topology and Its Applications}, 42 (1991) pp. 17-23.
\item[2.] ``The Universal Separable Metric Space of Urysohn
and Isometric Embeddings Thereof in Banach Spaces'', {\em
Fundamenta Mathematicae} 140 (1992), pp. 199-223. \item[3.]
``Systems of Combinatory Logic Related to Quine's `New
Foundations'\,'', {\em Annals of Pure and Applied Logic}, 53
(1991), pp. 103-33. \item[4.] ``The Axiom of Anti-Foundation
in Jensen's `New Foundations with Ur-Elements'\,'', {\em
Bulletin de la Societe Mathematique de la Belgique}, series B,
43 (1991), no. 2, pp. 167-79. \item[5.] ``Modelling Fragments
of Quine's `New Foundations'\,'', {\em Cahiers du Centre de
Logique}, no. 7, Institut Sup\'{e}rieur de Philosophie,
Universit\'{e} Catholique de Louvain, Louvain-la-Neuve, 1992,
pp. 97-112.
\item[6.] ``Systems of combinatory logic related to
predicative and `mildly impredicative' fragments of Quine's `New
Foundations'\,''. {\em Annals of Pure and Applied Logic\/} 59 (1993),
45-53.
\item[7.] The set theoretical program of Quine
succeeded (but nobody noticed), {\em Modern Logic\/}, vol. 4 (1994),
pp. 1-47.
\item[8.] The equivalence of {\em NF\/}-style set theories with
``tangled'' type theories; the construction of $\omega$-models of
predicative {\em NF\/} (and more), {\em Journal of Symbolic Logic\/},
vol. 60, no. 1 (1995), pp. 178-190.
\item [9.] ``Untyped $\lambda$-calculus with relative typing'', in Dezani
and Plotkin, eds., {\em Typed Lambda-Calculi and Applications\/},
the proceedings of TLCA '95, Springer, 1995.
\item[10.] ``Disguising recursively chained rewrite rules as equational
theorems'', in Hsiang, ed., {\em Rewriting Techniques and
Applications\/}, the proceedings of RTA '95, Springer, 1995.
\item[11.] ``Brief observations on software architecture and an
examination of the type system of Spec'', in the proceedings of the
Monterey Workshop on software architecture at the Naval Postgraduate
School, 1995.
\item [12.] {\em Elementary Set Theory with a
Universal Set\/}, volume 10 of the Cahiers du Centre de logique,
Academia, Louvain-la-Neuve (Belgium), 1998. 241 pages. ISBN
2-87209-488-1. This book is an elementary set theory text at the
advanced undergraduate or graduate level using {\em NFU\/}.
\item[13.] ``Subsystems of Quine's ``New Foundations'' with
Predicativity Restrictions'', {\em Notre Dame Journal of
Formal Logic\/}, vol. 40, no. 2 (spring 1999), pp. 183-196.
\item[14.] ``A strong and mechanizable grand logic'', in {\em Theorem
Proving in Higher Order Logics: 13th International Conference, TPHOLs
2000"\/}, {\em Lecture Notes in Computer Science\/}, vol. 1869,
Springer-Verlag, 2000, pp. 283-300. (refereed conference
proceedings).
\item[15.] ``Strong axioms of infinity in {\em NFU\/}'', {\em Journal
of Symbolic Logic\/}, vol. 66, no. 1 (March 2001), pp. 87-116. (``Errata in `Strong Axioms of Infinity in {\em NFU\/}'\,'', {\em JSL\/}, vol. 66, no. 4 (December 2001), p. 1974, reports some errata and provides corrections).
\item[16.] (with Jim Alves-Foss) ``The Watson theorem prover'', {\em
Journal of Automated Reasoning\/}, vol. 26 (2001), no. 4, pp. 357-408.
\item[17.] ``Foundations of mathematics in polymorphic type theory'',
{\em Topoi\/}, vol. 20 (2001), pp. 29-52.
\item[18.] ``Tarski's Theorem and {\em NFU\/}'', in C. Anthony
Anderson and M Zeleny (eds.), {\em Logic, Meaning and Computation\/},
Kluwer, 2001, pp. 469--478.
\item[19.] ``Forcing in {\em NFU\/} and {\em NF\/}'', in M. Crabb\'e,
C. Michaux and F. Point, eds., {\em A tribute to Maurice Boffa\/},
Belgian Mathematical Society, 2002. (refereed proceedings of a
conference in honor of the 60th birthday of Maurice Boffa).
\item[20.] ``Polymorphic type-checking for the ramified theory of
types of {\em Principia Mathematica\/}'', in Fairouz Kamareddine, ed.,
{\em Thirty-five Years of Automating Mathematics\/}, Kluwer, 2003,
pp. 173-215.
\item[21.] ``Paradoxes in double extension set theories'', {\em Studia Logica\/}, vol. 77 (2004), pp. 41-57.
\item[22.] ``The structure of the ordinals and the interpretation of
{\em ZF\/} in double extension set theory'', {\em Studia
Logica\/}, vol. 79 (2005), pp. 357-372.
\item[23.] ``Alternative Axiomatic Set Theories'', article in the
Stanford Encyclopedia of Philosophy (online) at the URL {\tt
http://plato.stanford.edu}. The exact URL for the article is \newline {\tt
http://plato.stanford.edu/entries/settheory-alternative/}. This
article was refereed and accepted by the editors for inclusion in
2006. It was reviewed and slightly revised in 2010.
\item[24.] ``Symmetry as a criterion for comprehension motivating
Quine's ``New Foundations'', {\em Studia Logica\/}, vol. 88, no. 2
(March 2008).
\item[25.] ``The Urysohn Space Embeds in Banach Spaces in Just One
Way'', {\em Topology and its Applications\/} Volume 155, Issue 14, 15
August 2008, Pages 1479-1482 Special Issue: Workshop on the Urysohn
space. I was invited to give a talk on my work on the Urysohn space
at this workshop, which was held in May 2006 at the University of the
Negev in Beersheba. This is not a new research paper, but an
exposition of my older results in this area.
\item[26.] ``Permutation methods in {\em NF\/} and {\em NFU\/}'', with
Thomas Forster, in {\em Proceedings of the 70th anniversary NF meeting
in Cambridge\/}, {\em Cahiers du Centre de Logique\/} no. 16,
Academia-Bruylant, Louvain-la-Neuve, 2009.
\item[27.] ``There is a Forster model of simple type theory'' in {\em
Proceedings of the 70th anniversary NF meeting in Cambridge\/}, {\em
Cahiers du Centre de Logique\/} no. 16, Academia-Bruylant,
Louvain-la-Neuve, 2009.
\item[28.]
M. Randall Holmes, Thomas Forster and Thierry Libert. ``Alternative Set Theories", in {\em Handbook of the History of Logic\/}, vol. 6, ``Sets and Extensions in the Twentieth Century", 2012, Elsevier/North-Holland, Dov Gabbay, Akihiro Kanamori, and John Woods, eds., pp. 559-632.
\item[29.] ``The usual model construction for {\em NFU\/} preserves information". {\em Notre Dame Journal of Formal Logic\/}, vol 53, no 4 (2012), 571-580.
\item[30.] ``The Axiom Scheme of Acyclic Comprehension'', with Zuhair al-Johar and Nathan Bowler, {\em Notre Dame J. Formal Logic\/}
Volume 55, Number 1 (2014), 11-24.
\item[31.] M. Randall Holmes, ``On hereditarily small sets in ZF", {\em Mathematical Logic Quarterly\/} vol 60 issue 3 pp. 228-229.
\item[32.] M. Randall Holmes, ``Representation of functions and total antisymmetric relations in third-order logic", {\em Journal of Philosophic Logic\/}, vol. 48 (2019), pp.263-278.
\item[33.] M. Randall Holmes, ``Symmetric comprehension revisited", accepted for inclusion in (refereed) College Publications multi-volume collection titled {\em Research Trends in Contemporary Logic\/} (edited by Melvin Fitting, Dov Gabbay, Massoud Pourmahdian, Adrian Rezus, and Ali Sadegh Daghighi), to appear.
\end{description}
\newpage
\item[Work in Progress]
These notes are miscellaneous and of varying levels of importance in my mind.
\begin{enumerate}
\item ``New Foundations is consistent". I claim a proof of the consistency of New Foundations, which I presented at a meeting in Cambridge in March 2013. It is not yet generally accepted that this is correct. I am actively working in improvement of my presentation. Professionals in the area are welcome to ask for access to the document; it is not to be shared further without informing me.
In this connection (2022) I have a new paper presenting a model of tangled type theory, as perhaps a more direct approach than the older approach using a tangled web.
\item I have produced a theorem prover based on dependent types, similar to Automath, called Lestrade,
for which I have papers and extensive sample proofs in preparation. In connection with this project, I also
have an implementation of the old Automath system itself.
\item I am planning to write a paper and have been writing testing
software on an efficient algorithm for bracket abstraction
(implementation of lambda calculus using combinators) which I
developed in 2005. I have already communicated with Henk Barendregt,
an expert in this field, who seems to think that my approach has some
interest.
\item I have developed a sequent calculus prover implementing {\em
NFU\/} (following a formal presentation by Marcel Crabb\'e). I used
this prover extensively (the logical rather than the set theoretical
aspects) in teaching Math 502, the graduate Logic and Set Theory
course, and in our second logic and discrete math course. I used it
to a lesser extent to reinforce the initial review of formal proof in
our introductory real analysis course, and introduced it briefly in
our first logic and discrete math course. I directed a graduate
student who wrote a Master's thesis about proof development in
elementary real analysis using the prover. My
experience suggests that the prover does help at least some students to understand
formal proof, both in propositional logic and in the logic of
quantifiers. The built in set theory has had some applications for
some students, but the fact that it is {\em NFU\/} has never actually
been important to a student user. I have a project in mind to develop
a formal proof of Specker's theorem that Choice is false in {\em NF\/}
under the prover.
\item I have a project of implementation of the logic of Frege in a stratified version which avoids paradox,
with an associated theorem prover. It is interesting to observe that the underlying type system used in this prover is essentially the same as that of Marcel though the provers appear quite different. These two systems might be covered in a single paper.
\item An expanded version of ``Forcing in {\em NFU\/} and {\em
NF\/}'', listed above as appearing in a Festschrift in honor of
Maurice Boffa, should at some point be submitted to a refereed
journal.
\item I project a revision of my book {\em Elementary set theory with
a universal set\/}: currently it is out of print but I have permission
from the publishers to post it on the web. The web version contains
various revisions and I am soliciting advice from others about needed
corrections. I do not intend to extend this book, but write a second
monograph on a higher level; see the next item. I did substantial revisions and corrections to the book in fall 2012, and will continue working on this.
\item A book on the consistent subsystems of {\em NF\/}: my current
plan is to write this as an extension of the existing notes I used to
teach foundations of mathematics to Boise State graduate students
starting with type theory rather than set theory. I made some additions to this text during my sabbatical in Fall 2012.
\item The paper on the ramified theory of types of {\em Principia\/}
is accompanied by software implementing a complete polymorphic type
checker for the ramified theory of types. I have considered writing a
proposal to implement some significant part of {\em Principia\/} using
this system. I was invited in November 2010 to speak at a workshop
commemorating the 100th anniversary of the publication of {\em
Principia Mathematica\/}, due to my work in this area, and gave a
presentation whose slides should soon appear on my web page.
\item I have a new paper in preparation (2022) presenting models of NFU related to the very strong rank-into-rank large cardinal axioms.
\end{enumerate}
\end{description}
\end{document}