Re: Simple Question regarding Simply Typed Lambda Calculus

The context Gamma embraces the
free variables in the term.

The inference rules state in
the same time what happens with
the term and with the free
variables.

So there is no need to define
a predicate varof, separate from
a predicate proof. Here is an
example:

Take the rule:

G |- s:A
--------
G\x:B |- lambda x s:B->A

Looking at the proof we know:

if we have a proof of A via a term s,
and if x represents a proof of B,
then we can construct a proof of B->A via a term lambda x s.

Looking at the varof we know:

The free variables of the proof of A via the term s are subset of G,
then the free variables of the proof of B->A via the term lambda x s
are subset of G\x:B, thus x will not be free anymore.

Instead of free variable you can also
call these things assumptions. Here is
an example proof, in inference style:

1) x:A |- x:A (given)
2) |- lambda x x:A->A (from 1)

Or in fitch style, which makes more
explicit the introduction and
elimination of assumptions:

x:A (assumption)
1) x:A (given)
lambda x x:A (discharge)

Bye
Debajit Adhikary wrote:
Why exactly do we need to define a context (indicated using Gamma) in
Simply Typed Lambda Calculus?

What happens if we left out the Gamma?

This is something I'm not too clear about.. I'd appreciate any help at
all -- I'm looking for examples in particular -- pointers to web
resources would be great.

.