Entering the Main Goal of a Theorem

Click on <main proof goal>. Nuprl opens up a term editor window. The window initially looks like:

The main goal is entered in a structural top-down fashion. Enter:

After the , the display should look like:

$$\forall$$

The [var] slot of the all term is a text slot. The [type], and [prop] slots are term slots. Try clicking at each of of the slots. Notice how you get a text cursor for a text slot and a term cursor for the term slots.

Click on var and enter:

The character $\ulcorner$A$\urcorner$ gets inserted in the variable slot, and on keying , the cursor moves onto the [type] slot. Enter:

The term ${\Bbb{P}}${[level]} gets inserted, and a text cursor is positioned at the start of [level].

The display should now look like:

$$\forall {\Bbb{P}}$$

The prop you just entered has nothing to do with the prop in the [prop] place-holder. prop happens to be a name for the propositional universe term.

In a similar way, you should now be able to enter a second universal quantifier to give the following situation:

$$\forall {\Bbb{P}} \forall {\Bbb{P}}$$

Now enter:

The display should now look like:

$$\forall {\Bbb{P}} \forall {\Bbb{P}} \neg \wedge \Longleftrightarrow$$

Note that Nuprl automatically inserted parentheses around the [prop] $\wedge$ [prop] term. We have given Nuprl a precedence for each term that might need parenthesizing. Nuprl uses this precedence information to always automatically insert parentheses as appropriate. Related to precedence, we can optionally give binary infix terms an associativity of either `L' or `R'. `L' means that parentheses should not be used when the term associates to the left. Similarly, `R' suppresses the use of parentheses when the term associates to the right. For example, $\ulcorner$$\wedge$$\urcorner$ associates to the left, so Nuprl displays $(A\ \wedge\ B)\ \wedge C$ as

A $\wedge$ B $\wedge$ C

but $A\ \wedge\ (B\ \wedge\ C)$ as:

A $\wedge$ (B $\wedge$ C)

To continue, with the cursor at the left [prop] of [prop] $\wedge$ [prop], enter:

to insert the variable term A.

You should now know enough to complete entering the main goal, and correct any mistakes you make. The completed main goal should look like:

$$\forall {\Bbb{P}} \forall {\Bbb{P}} \neg \wedge \Longleftrightarrow \neg \vee \neg$$

If a term won't fit on one line, Nuprl inserts linebreaks and indentation as appropriate. Sometimes a window can be made easier to read by resizing it. Nuprl automatically adjusts the formatting when the window is resized. Occasionally, some subterm is elided, and shown as

(...)

In this event, the elided subterm can often be made visible by widening the window.

Once you have finished entering the main goal, close the main goal window by keying $\langle$C-Z$\rangle$.