> 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).
Yes to all this. The HOL4 Description does spell out how to derive the
standard logical inference rules from the
HOL4 primitive inference rules. See Chapter 2 of
kananaskis-9-description.pdf
available from the SourceForge site. Derivations start on page 45.
Although this
portion of the Description is out of
date, and doesn't start from the same basis as HOL Light, it should still
be able to help you on your quest.
Konrad.
On Mon, Mar 24, 2014 at 6:49 AM, Rob Arthan <r...@lemma-one.com> wrote:
> 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
>
>
------------------------------------------------------------------------------
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
