Hypothetical judgment

A judgment is a statement derivable in a particular object logic. A hypothetical judgment is a judgment that makes use of hypothetical assumptions. On paper, we often represent a set of hypothetical assumptions using a context:

$${ \Gamma, A \textrm{ true} \vdash B \textrm{ true} \over \Gamma \vdash A \Rightarrow B \textrm{ true} }$$

We name the judgment that proves the truth of a proposition $\Gamma \vdash C\textrm{ true}$, which can be read as “Under the assumptions $\Gamma$, $A$ is true.” The context is the sequence of assumptions $\Gamma = A_1\textrm{ true}, \ldots, A_n\textrm{ true}$.

With an ordinary hypothetical context, we may freely coalesce repeated assumptions, add extra unused assumptions, and to reorder the assumptions in the context. (Formally, these are the properties of contraction, weakening, and exchange.)

Additionally, a context in a hypothetical judgment should satisfy the identity and substitution properties. Identity simply means that we should be able to use our hypotheses — $\Gamma, A\textrm{ true} \vdash A\textrm{ true}$. Substitution means that if we have a proof tree showing $\Gamma, A\textrm{ true} \vdash B\textrm{ true}$, and another proof tree $\Gamma \vdash A\textrm{ true}$, then we should be able to substitute the second tree into the first, replacing hypothesis $A\textrm{ true}$ and producing a new tree proving $\Gamma \vdash B\textrm{ true}$.

This sample rule is the implication introduction rule, which says that $A \Rightarrow B$ is true if we can show $B$ is true under the hypothetical assumption $A\textrm{ true}$.

In the LF methodology, we represent the hypothetical context of our object language’s judgment using the LF context itself. (See higher-order judgment.)

For example, we can represent the introduction rule as follows:

%sort prop %.
%term ==> %pi prop %-> prop %-> prop %.
%prec %none 10 ==> %.
%sort true {_ prop} %.
%term imp/intro %pi (true (A ==> B)) %<- (%pi (true A) %-> (true B)) %.

Here, we represent the hypothetical assumption that $A\textrm{ true}$ using an LF hypothesis of type A true. We can see this clearly if we write down the proof term for the proof of the tautology P ==> P:

%define taut (true (P ==> P)) imp/intro ([ptrue true P] ptrue) %.

Within the scope of the function argument to imp/intro, we assume that we have a proof of P true (which we creatively named ptrue). This assumption lets us show that P true holds, and that lets us show that (P ==> P) true.