re: judgement notation

• To: types <types@uk.ac.glasgow.dcs>
• Subject: re: judgement notation
• From: Dean Rosenzweig <dean.rosenzweig@yu.mail.ac.uni-zg>
• Date: Thu, 19 Nov 1992 15:30:31 +0000
• Approved: types@dcs.gla.ac.uk

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

• Prev: Sconing and Relators
• Next: European Association for Computer Science Logic
• Index(es):
  • Main
  • Thread