[CST-2] Types: y2000p9q13

[Andy Wilson]

On Sun, 2 Jun 2002, George van den Driessche wrote:

> ----- Original Message -----
> From: "David Singleton" <dps29@hermes.cam.ac.uk>
> To: <cst-2@srcf.ucam.org>
> Sent: Sunday, June 02, 2002 11:44 AM
> Subject: [CST-2] Types: y2000p9q13
>
>
> >
> > Has anyone done this question, and could they tell me how to do the
> > proof?
>
> Rule induction. Prove that phi holds for the axioms, and also that for each
> rule, if it holds for the premises then it holds for the conclusion. You
> need to cope with several different implications to get the rules to work,
> because there's implication internal to phi, and also from premises to
> conclusion. It gets a bit confusing.

See the section 2.4 starting on page 18 of the IB Semantics notes
(http://www.cl.cam.ac.uk/Teaching/2001/Semantics/sempl.ps.gz) for an
explanation of Rule Induction...

Andy.