[Prev][Next][Index][Thread]
A question for Martin-L\"of disciples
The definition of "intensional" Martin-L\"of type theory used
by the Swedes (Nordstr\"om, Petersson, Smith, et al.) in their book
_Programming_in_Martin-L\"of's_Type_Theory_ and Simon Thompson in
_Type_Theory_and_Functional_Programming_ does not look
much like that used by Troelstra and van Dalen in _Constructivism_in_
_Mathematics,_Volume_II_. The former group eschews the rule IExt:
p : I(A, a, b)
(IExt) --------------
a = b : A
while the latter cheerfully include it but omit \eta and \xi.
Simon Thompson claims the decidability of judgements [british spelling]
in ML^i; Troelstra and van Dalen seem to make no claim either way about
their system, although there is a cryptic note on page 633 which refers
to the former formulation.
My questions are:
1. Are the two systems "equivalent" (are the sets of theorems in any sense
the same)?
2. If so, how so, and if not, how solvable are judgements in the
Troelstra/van Dalen formulation?