Entering and Leaving Contexts

Suppose we have the sentence . We can then *enter* the context and *infer* the sentence . We can
regard as analogous to , and the operation of
entering as analogous to *assuming* in a system of *natural deduction* as invented by Gentzen and described in many
logic texts. Indeed a context is a generalization of a
collection of assumptions, but there are important differences. For
example, contexts contain linguistic *assumptions* as well as
declarative and a context may correspond to an infinite and only
partially known collection of assumptions. Moreover, because
relations among contexts are expressed as sentences in the language,
allows inferences within the language that could only be
done at the meta-level of the usual natural deduction systems.

There are various ways of handling the reasoning step of
entering a context. The way most analogous to the usual natural
deduction systems is to have an operation . Having done
this, one could then write any for which one already had
. However, it seems more convenient in an interactive
theorem proving to use the style of Jussi Ketonen's EKL
interactive theorem prover [Ketonen and Weening, 1984]. In
the style of that system, if one had , one could immediately
write , and the system would keep track of the dependence on .
To avoid ambiguity as to where an occurrence of came from,
one might have to refer to a line number in the derivation. Having
obtained by entering and then inferring some sentence , one
can *leave* and get . In natural deduction, this
would be called discharging the assumption .

Human natural language risks ambiguity by not always specifying such
assumptions, relying on the hearer or reader to guess what contexts
makes sense. The hearer employs a *principle of charity* and
chooses an interpretation that assumes the speaker is making sense.
In AI usage we probably don't usually want computers to make
assertions that depend on principles of charity for their
interpretation.

Another application of entering a context has to do with
quantifiers. It involves a distinguished predicate
,
where names an object. If we have

then when we enter , then a special inference rule associated with the predicate gives

Likewise if we have shown

within the context , we can infer

We could get similar effects by associating a domain (call it ) with each context .

I'm presently doubtful that the reasoning we will want our programs to do on their own will correspond closely to using an interactive theorem prover. Therefore, it isn't clear whether the above ideas for implementing entering and leaving contexts will be what we want.

Sentences of the form can themselves be true in contexts, e.g. we can have . In this draft, we will ignore the fact that if we want to stay in first order logic, we should reify assertions and write something like , where is a term rather than a wff. We plan to fix this up in some way later, either by introducing terms like or by using a modified logic. Actually the same problem arises for itself; the occurrence of in might have to be syntactically distinct from the occurence of standing by itself.

2005-04-13