Entering and Leaving Contexts

Suppose we have the sentence $ist(c,p)$. We can then enter the context $c$ and infer the sentence $p$. We can regard $ist(c,p)$ as analogous to $c \supset p$, and the operation of entering $c$ as analogous to assuming $c$ 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, $ist(c,p)$ 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 $enter\ c$. Having done this, one could then write any $p$ for which one already had $ist(c,p)$. 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 $ist(c,p)$, one could immediately write $p$, and the system would keep track of the dependence on $c$. To avoid ambiguity as to where an occurrence of $ist(\ ,p)$ came from, one might have to refer to a line number in the derivation. Having obtained $p$ by entering $c$ and then inferring some sentence $q$, one can leave $c$ and get $ist(c,q)$. In natural deduction, this would be called discharging the assumption $c$.

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 $present(c,exp)$, where $exp$ names an object. If we have

$$\forall x(present(c,x) \supset P(x)),$$

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

$$\forall x P(x).$$

Likewise if we have shown

$$\exists x P(x)$$

within the context $c$, we can infer

$$\exists x(present(c,x) \land P(x)).$$

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

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 $ist(c,p)$ can themselves be true in contexts, e.g. we can have $ist(c0,ist(c1,p))$. 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 $ist(c0,Ist(c1,p))$, where $Ist(c,p)$ is a term rather than a wff. We plan to fix this up in some way later, either by introducing terms like $Ist(c,p)$ or by using a modified logic. Actually the same problem arises for $p$ itself; the occurrence of $p$ in $ist(c,p)$ might have to be syntactically distinct from the occurence of $p$ standing by itself.