Classical Reasoning

It is best to have this hypothesis in the form of the xmiddle abstraction:  

The Decide tactic recognizes whenever the xmiddle abstraction occurs as some hypothesis, and in this case is trivially able to justify decidability. Also, the D tactic on set types, maybe with abstractions wrapped around them, always yields an unhidden set predicate, whether or not there is an abstraction with a properties lemma.

If you want to prove a non-constructive theorem, it is simplest to add the xmiddle proposition as a precondition of the theorem, so that the theorem is of form .

There are two common cases when in proving a part of a constructive theorem, classical reasoning becomes admissable. These cases, and a recommended method in each case for adding an xmiddle hypothesis are as follows:

1. If the conclusion is the squashed exists term and you are about to apply the tactic With t (D 0). Squashed exists  is defined in core_1 as:

   

   First use the tactic AddXM  :

   

   AddXM 1 alone adds the hypothesis as a hidden hypothesis, so there are no soundness problems here. becomes unhidden in the first and third subgoals since here the conclusion is recognized as being trivially squash stable. becomes unhidden in the second subgoal since from here on, any computational content in the proof cannot contribute to the computational content of the original goal of the theorem.

2. If the conclusion is squash stable. Again first run the tactic AddXM 1. If the conclusion is obviously squash stable, then is added unhidden. If the conclusion is not obviously squash stable and gets added hidden, you should then run the Unhide tactic.

The AddXM tactic assumes that the proposition is true; that is, the corresponding type is inhabited. This is a very reasonable assumption to make, but it is not true according to the semantics given for Nuprl 's type theory in S. Allen's thesis.