🚀 go-pugleaf

dzik@access.digex.com (Joseph Dzikiewicz) writes:
: I have come across two uses of the term "type theory" in logic that seem
: to be referring to different things.
: 
: In one, Type Theory seems to relate to the rules for higher-order-logics
: (ie, second order logic and up).  This is discussed in Peter Andrews'
: book "An Introduction to Logic and Type Theory: To Truth through Proof."
: I have also seen it referred to as "Church's Type Theory."
: 
: In the other, types are sets of formulas in first order logic.  This
: is discussed in some detail in Chang and Keisler's book "Model Theory."
: 
: Am I correct in thinking that these are two different things with the same
: name, or are they the same thing presented differently by two
: different groups of authors?

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.

The Simple Theory of Types is just Predicate Calculus 
enriched with typed lambda calculus. 

Types themselves can be thought of as sets, with a little care, 
depending on how you want to give the *semantics*. Chang and Kreisler
deal with models, Andrews with the logic. 

But, ahem, types pitch up all over the place: they just prevent certain
things (eg. applying a function to the wrong arguments) from happening.
Eg. types of variables in computer languages.

Gavan Tredoux
UCT

In a previous article, dzik@access.digex.com (Joseph Dzikiewicz) says:

>I have come across two uses of the term "type theory" in logic that seem
>to be referring to different things.
>
	Yes, there are two different sense of "type"-- no doubt 
relatable on some level but I don't know of any reason toe relate
them.  
	The name "type theory" always means the first, i.e. 
higher order logics.

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:
   : I have come across two uses of the term "type theory" in logic that seem
   : to be referring to different things.

   ...

   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.

   The Simple Theory of Types is just Predicate Calculus 
   enriched with typed lambda calculus. 

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

--

 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!

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

In article <1992Nov13.123046.17412@husc3.harvard.edu> zeleny@husc10.harvard.edu (Michael Zeleny) writes:

   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;

Sorry, if I gave this impression. Although Type Theory (in the sense
of Martin-L"of) is constructive it is not necessarily intuitionistic,
i.e. we may accept Markov's principle.  This would be particularly
useful if you use Type Theory for program verification. However, all
the Type Theories I know are actually intuitionistic.

   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.

Certainly, but this just means that you have to give up something to
get classical reasoning AND propositions as types. I am not an expert
in this area but as I understand it: You may have a computational
interpretation of type theory if you 'fix' your evaluation strategy
(i.e. you decide to use only the equations of the call-by-value
\lambda calculus). 

I suppose the most famous person working in this direction is Girard
who last year wrote a paper entitled "A New Constructive Logic:
Classical Logic". However, I should also mention Parigot's "Free
Deductions" and Vilinsky's categorical account of continuations.
--

 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!

In article <ALTI.92Nov16194749@tanera.dcs.ed.ac.uk> alti@dcs.ed.ac.uk (Thorsten Altenkirch) writes:

   Certainly, but this just means that you have to give up something to
   get classical reasoning AND propositions as types. I am not an expert
   in this area but as I understand it: You may have a computational
   interpretation of type theory if you 'fix' your evaluation strategy
		     ^^^^^^^^^^^
Should read: classical logic

   (i.e. you decide to use only the equations of the call-by-value
   \lambda calculus). 

Sorry.
--

 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!