Example 1
(Continued)

Suppose P and Q are logical propositions.

We want to prove that if the statement

	P & Q

is true, then so is the statement

	Q & P

This is nothing very profound. We are just showing that the AND-operator ( &) is reversible or commutative. We want to prove that the statement "P & Q" implies the statement "Q & P." Or, in the notation of DC Proof, we want to prove

	P & Q => Q & P

where "=>" is the IMPLIES-operator.

We begin our proof by asking, what if the statement "P & Q" is true. That is, we begin by generating an initial premise, "P & Q." A premise is just a statement that is assumed to be true. Most proofs begin with one or more premises.

To enter a premise, click the Prem (Premise) button below the menu bar of the main screen:

	
                               
This will bring up the Premise form:

	

In the text box, as shown, key in

	P & Q
Click the Continue button on the Premise form. This will close the Premise form. In the text box on the main screen, you should then  have:
1	P & Q
	Premise
The number 1 in the left margin is the line number. It indicates that this is the first statement of your proof. The comment, "Premise," (in grey) indicates the rule of inference used to generate this statement – the Premise Rule in this case.
 

Continued