home *** CD-ROM | disk | FTP | other *** search
- Path: sparky!uunet!ogicse!das-news.harvard.edu!husc-news.harvard.edu!husc10.harvard.edu!zeleny
- From: zeleny@husc10.harvard.edu (Michael Zeleny)
- Newsgroups: sci.logic
- Subject: Re: Types of type theory
- Message-ID: <1992Nov13.123046.17412@husc3.harvard.edu>
- Date: 13 Nov 92 17:30:45 GMT
- Article-I.D.: husc3.1992Nov13.123046.17412
- References: <BxIxGz.D7x@access.digex.com> <1992Nov12.144654.7493@ucthpx.uct.ac.za> <ALTI.92Nov13131546@tanera.dcs.ed.ac.uk>
- Organization: The Phallogocentric Cabal
- Lines: 71
- Nntp-Posting-Host: husc10.harvard.edu
-
- In article <ALTI.92Nov13131546@tanera.dcs.ed.ac.uk>
- alti@dcs.ed.ac.uk (Thorsten Altenkirch) writes:
-
- >In article <1992Nov12.144654.7493@ucthpx.uct.ac.za>
- >gavan@elc.mth.uct.ac.za (Gavan Tredoux) writes:
-
- >>dzik@access.digex.com (Joseph Dzikiewicz) writes:
-
- JD:
- >>>I have come across two uses of the term "type theory" in logic that seem
- >>>to be referring to different things.
-
- GT:
- >>Type theory *is* higher-order logic, where the types are used to
- >>avoid the paradoxes. One version -- the one Andrews explains --
- >>is Church's Simple Theory of Types. There are others -- the Ramified
- >>Theory of types (Ramsey) and the original, Russell's type theory.
-
- That's backwards: Russell discovered the ramified type theory, designed to
- avoid the eponymous antinomy, as well as the semantic paradoxes, while
- Ramsey made the observation that, since mathematics was not concerned with
- truth or other such picayunish semantic notions, the ramification into
- levels was superfluous. Alonzo Church is the foremost living authority on
- type-theoretic matters. See his papers "A Formulation of the Simple Theory
- of Types" (JSL, 1940), "Russellian Simple Type Theory" (APA, 1975), and
- "Comparison of Russell's Resolution of the Semantical Antinomies with that
- of Tarski" (JSL, 1977). Also see Girard's elegant formulation of typed
- \lambda-calculus, likewise indebted to Church, in his book _Proofs and
- Types_. The latest formulation of Church's Logic of Sense and Denotation,
- in effect an intensional hierarchy of type theories, is forthcoming in
- _Nous_, which also contains the earlier version in the 1973-4 volumes.
-
- GT:
- >>The Simple Theory of Types is just Predicate Calculus
- >>enriched with typed lambda calculus.
-
- Not so. The addition of \lambda-calculus is in no way essential; all that
- is needed is a semantics that supports the recursively defined hierarchical
- partition of quantified variables as ranging over the types of individuals,
- as well as functional types with arbitrary choices of domain and range
- types; alternatively, relations may be used in place of functions, and a
- silly set version of type theory may be formulated to look like a
- non-cumulative version of ZF(U), or any other well-founded (or not!) set
- theory with (or without!) ur-elements.
-
- TA:
- >There is still another type of type theory for which the most famous
- >example is Martin-L"of's Type Theory. Here types and propositions are
- >identified, i.e. a proposition is the type of its proofs. This may
- >seem unusual but it leads to a very elegant formalisation of
- >mathematical concepts. This sort of Type Theory is inherently
- >intuitionistic because every proof has to have a constructive content.
- >(I should mention that there is some work going on in extending this
- >to classical reasoning).
-
- I would prefer not to conflate intuitionism with constructivism; otherwise
- your final remark is misleading, as the results of G\"odel and Tarski imply
- that any proof-theoretic conception of mathematical truth will fall short
- of the bivalence required by the classical reasoning. See the remarks of
- Tarski in his original paper on the concept of truth.
-
- >--
- >
- > Thorsten Altenkirch And there's a hand, my trusty fiere,
- > Laboratory for Foundations And gie's a hand o' thine,
- > of Computer Science And we'll tak a right guid-willie waught
- > University of Edinburgh For auld lang syne!
-
- cordially,
- mikhail zeleny@husc.harvard.edu
- " -- I shall speak bluntly, because life is short."
-