Bill,
On 24 Mar 2014, at 06:28, Bill Richter <rich...@math.northwestern.edu> wrote:
> Thanks, Rob! You're right, I hadn't looked at Section 1.4 "A Formulation
> Based on Equality" of Andrew's link
>> http://plato.stanford.edu/entries/type-theory-church/ and more to the point,
>> I didn't read the longer version Andrew's wrote in his book To Truth Through
>> Proof:
> More details about Q0 can be found in Andrews 2002.
> So you're right, that's not a fair reading of mine.
>
> But I don't see anywhere in Andrews's very readable Section 1.4 where he says
> that we can recover all the FOL we need from some simple typed LC axioms, why
> he's not going to need the 6 axioms he listed in section 1.3.2 Elementary
> Type Theory.
It’s clearly readable but not very clear! When Andrews writes:
"Q0 is based on these ideas, and can be shown to be equivalent to a formulation
of Church's type theory using Axioms 1–8 of the preceding sections”.
he means the system Q0 with just the one inference rule can be shown to be
equivalent to the system given by the axioms and rules of the previous
sections. I.e., “using …” doesn’t mean you need to assume the axioms in the
proof. I believe this is all covered in his book.
> Can you get to the bottom of this? Obviously you know how to deduce FOL
> from something like the HOL Light axioms, because you needed to to write your
> proof assistant ProofPower. So where did you learn it? From Konrad's book
> Gordon and Melham? From Andrews's book?
Osmosis. The original HOL documentation/code included schematic derivations of
the derived rules of inference (didn’t that make it into Gordon and Melham?).
However, the starting point for that is the rather ad hoc collection of
primitive rules and axioms that evolved into the ones currently used in HOL4
and ProofPower. Andrews’ book shows how to do it with an even leaner set of
rules and axioms than HOL Light and his article that you have been reading
points back to Tarski, Quine and Henkin as the original sources. It also
follows from abstract nonsense about the internal logic of a topos that you can
derive the properties of the logical connectives and the quantifiers given a
model of the typed lambda-calculus (like the one described in the HOL4 Logic
manual).
Regards,
Rob.
------------------------------------------------------------------------------
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
