[Prev][Next][Index][Thread]

re: judgement notation





John Mitchell writes:

==========================================================================

Although a slight digression, I might comment that in Martin-Lof's systems 
(at least historically), the distinction between well-formed and provable
judgements does not arise.  There was never, to my knowledge,
a notion of ``well-formed but not provable judgement.'' However,
in a logical treatment of typed lambda calculus (of any kind),
I beleive there is a place for this distinction.

=========================================================================

The judgement

	0 = 1 : N

is well formed (but not provable) in most (all?) versions of
Martin-Lof's systems.

Dean Rosenzweig