🚀 go-pugleaf

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."