Constructive Reasoning

The constructivity of Nuprl 's logic manifests itself in two main ways with the tactics:

1. For any proposition P, the goal is not in general provable.
2. When applying the D tactic to a hypothesis that has a set term outermost, the predicate part of the set term becomes a hidden hypothesis . For example:

   

   Here, the surrounding the hypothesis number i+1 indicate that this hypothesis is hidden. A hidden hypothesis is not immediately usable though there are ways in which it might become usable later in a proof.

Tactics to simplify dealing with these issues are described in the next two sections.