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

No Subject

On Type-assignment terminology (John Mitchell's note)
         From Roger Hindley

Some suggestions for notetion:

In a Natural Deduction system (whose formulae have form
                 |- M:sigma
and whose deductions are trees):

  |- M:sigma ------- type-assignment (TA) statement;
  Gamma |- M:sigma ------- deducibility statement;
  <Gamma's types, sigma> or <Gamma, sigma> -------
                                                pair
          (as suggested by John and others, and used
           already, for example in "principal pair")
  Tree-form deductions ------- type-deductions.

In a Sequenzen-based system (whose formulae have form
                Gamma |- M:sigma ):

   Gamma |- M:sigma ------- TA-statement, judgement, or
                            assertion, as suggested (by Albert?)

By the way, some remarks.

(1)  I agree with John's point that we sould be careful to
distinguish between deducibility statements
                   Gamma |- M:sigma
in Natural-deduction systems, and assertions in Sequenzen-
systems.  Perhaps the latter should even have a different
notation, like
                   Gamma ==> M:sigma
instead of
                   Gamma |- M:sigma,
to emphasise the distinction.
    My impression is that many people are not clear just
what this distinction is, so here are some words on this.

    In a Natural Deduction system, we build tree-form
deductions from formulae
                   M:sigma,
and a statement
                Gamma |- M:sigma
is not part of the formal system, but a comment in the meta-
language saying that we have built a deduction whose
assumptions are included in the set Gamma, and whose conclusion
is M:sigma.  Thus the "|-" symbol is not part of the forma system.

In contrast, in a Sequenzen-system, a statement
                  Gamma |- M:sigma
is part of the formal system, and does not assert deducibility,
unless the Sequenzen-system is the meta-theory of a previously-
given Natural Deduction system.

This might seem to be labouring the obvious, but I have seen
written papers in which the author does not seem to understand
the difference here.

The main formal effect of this difference is that when
a statement
                Gamma |- M:sigma
is used in the meta-theory of a N.D. system, we can, by tradition,
assume without stating them, rules such as permutability of
premises, transitivity of "|-", etc.   But when we describe a
Sequenzen-system, we must include such rules explicitly as part
of the formalism, or prove them admissible; they are the
rules called "structural rules" by proof-theorists; permutation
of premises, duplication of premises, weakening, and cut.
A Sequenzen-system without such rules is extremely weak, although
they are sometimes omitted in error from type-manuscripts using
the Sequenzen-formulation.

It is to emphasise the above distinctions that I suggest using "==>"
instead of "|-" in Sequenzen systems.  If one uses "|-", then what
symbol will one use when one comes to talk about deducibility in
the Sequenzen-system?

  (2)  On deductions, a question.
We all know that deductions are trees, "defined in the usual way",(?),
but does anyone know of a reference, say at graduate-student level,
where deduction-trees are defined or explained in any detail or
clarity?   I know the graph-theorists have precise definitions of
"tree", but it seems to confuse rather than clarify, to try to
apply them in this context.  Are there any good references?  With
simple examples of deductions?

                       Roger Hindley,
                         majrh%uk.ac.swansea.pyramid@rl.earn