My personal feelings on this foundational aspect are that the
actual set of axioms isn't that important provided the usual
introduction and elimination rules of predicate calculus can be
derived from them.
My recollection (don't have citations to hand) is that Church originally
wanted the untyped lambda calculus to serve as a foundation for logic,
but that was discovered to be inconsistent. Something like
Russell's paradox would be easy to code up in it. However, the simply
typed lambda calculus worked better, i.e., it supports the derivation of
the expected FOL-like rules, as we see in HOL theorem provers, and it
is sound.
Konrad.
On Thu, Mar 20, 2014 at 7:31 PM, Bill Richter <rich...@math.northwestern.edu
> wrote:
> Thanks, Rob! I don't Andrew's book to hand either, but his on-line
> article is causing me real trouble:
> http://plato.stanford.edu/entries/type-theory-church/
>
> 1.3.2 Elementary Type Theory
>
> We start by listing the axioms for what we shall call elementary type
> theory.
> (1) [pο ∨ pο] ⊃ pο
> (2) pο ⊃ [pο ∨ qο]
> (3) [pο ∨ qο] ⊃ [qο ∨ pο]
> (4) [pο ⊃ qο] ⊃ [[rο ∨ pο] ⊃ [rο ∨ qο] ]
> (5α) Πο(οα) f(οα) ⊃ f(οα) xα
> (6α) ∀xα[pο ∨ f(οα)xα] ⊃ [pο ∨ Πο(οα) f(οα)]
>
> The theorems of elementary type theory are those theorems which can
> be derived from Axioms 1–6α (for all type symbols α). We shall
> sometimes refer to elementary type theory as T . It embodies the
> logic of propositional connectives, quantifiers, and λ-conversion
> in the context of type theory.
>
> But in HOL, I think these Prop Logic results are theorems and not axioms.
> My feeling is that Andrews's book is great because it clearly establishes
> the fact that HOL (which Andrews says is a synonym for Church's type
> theory) is "the same" as Church's work which is "almost the same" as
> Russell-Whitehead. This is an important point relating to the homotopy
> type theory that Vladimir Voevodsky is doing. I don't feel that Andrews's
> book is readable enough to be satisfactory documentation.
>
> The primitive rules and axioms in HOL4 (and ProofPower) are
> different from HOL Light, but prove the same set of theorems.
>
> Thanks. Could you respond to my last disjointed post about the HOL
> meaning of typed Lambda calculus? That (perhaps) Church's typed LC allows
> us to elegantly deduce all the FOL we need (such as Andrews's axioms above)
> from some simple LC axioms?
>
> --
> Best,
> Bill
>
>
> ------------------------------------------------------------------------------
> 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
