On Fri, Mar 21, 2014 at 9:08 AM, Bill Richter <[email protected]
> wrote:
> Thanks, Konrad! I'll read your proof of NOT_FORALL_THM, and try to find
> Gordon and Melham's book. Two points:
>
> I don't believe that Church ever explained how typed LC implies FOL.
> Church certainly does not explain this in his paper
> A Formulation of the Simple Theory of Types
> http://www.jstor.org/stable/2266170.
> In section 4 "Formal axioms", he lists exactly the FOL axioms that his
> student Peter Andrews lists
> http://plato.stanford.edu/entries/type-theory-church/
> So maybe Gordon and Melham were the first people to figure out how to
> deduce FOL from typed LC and some simple LC axioms like the HOL Light
> axioms Tom Hale cites:
> http://www.ams.org/notices/200811/tx081101370p.pdf
Leon Henkin seems to get the credit for showing that propositional calculus
follows from LC, actually Church's type theory in particular ("A theory of
propositional types", Fundamenta Mathematicae 52:323-344, 1963
http://matwbn.icm.edu.pl/ksiazki/fm/fm52/fm52123.pdf).
In "Reasoning in Simple Type Theory" (Benzmuller, Brown, Siekmann and
Statman eds) 2008, Andrews writes (p. 5)
"Leon Henkin spent some time in Princeton while I was there as a graduate
student. Henkin was writing a paper (referenced above, 1963) in which he
presented a formulation of Church's type theory (with types restricted to
propositional types, though this is incidental to much of the paper) in
which the only primitive logical constant was equality."
Immediately following Henkin's paper in the same volume of the same journal
is an article by Andrews, "A Reduction of the Axioms for the Theory of
Propositional Types", in which he simplified Henkin's axioms.
Whoever may have done what first, Andrews' textbook does lay out
derivations of FOL and more using simple type theory.
Please do remember that "LC", or Andrews' Qο, or the basically equivalent
systems in the HOL family of proof assistants,a re much more than FOL. Not
only FOL but also the natural numbers and a great deal more of math is
derivable from just Church's simple type theory, whichever version you use.
For what it's worth, another attraction of Qο to some of us is that its
axioms are simple expressions of fundamental ideas about functions (axioms
2, 3, and 4), and the boolean type (axiom 1). Axiom 5 is a very simple
expression of the idea of definite description, though admittedly definite
description itself is a subject of some philosophical depth. Andrews uses
only a single rule of inference (Rule R) that replaces equals with equals.
I do find Qο's definitions (much like ones in related proof assistants)
curiously less obvious than his axioms and his rule of inference. Where
they make my head hurt a lot, I have finally come around to viewing his
definitions as true statements and just observing that they can be treated
as abbreviations, which makes them syntactically legal as definitions. T
and F to me are intuitively more fundamental than their definitions, but
that doesn't affect the math, much as it makes the philosophical areas of
my brain hurt.
-Cris
------------------------------------------------------------------------------
Learn Graph Databases - Download FREE O'Reilly Book
"Graph Databases" is the definitive new guide to graph databases and their
applications. Written by three acclaimed leaders in the field,
this first edition is now available. Download your free book today!
http://p.sf.net/sfu/13534_NeoTech
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
