Page 2 Proof Strats

Strategies for Creating Show Lines

Strategy #1: Conditional Show Lines

• Condition: If the Show line immediately above contains a conditional (denoted as PQ).

• Action: Start a new Show line for the consequent of the conditional (denoted as Show Q) on line n.

• Command: Use command to create the new line - "Show cons".

• Goal: After proving Q, the next step will be to box and cancel the Show line containing P-Q. Justification for this step is given as "n CD".

Strategy #2: Handling Negation of Complex Sentences

• Condition: If a previous available line, n, is the negation of a complex sentence such as:

  • $(~(PQ))$

  • $(~(PVQ))$

  • $(~(PAQ))$

• Options: You have two approaches to take:

  • Option 1: Show the unnegation of that line using the command: "Show unneg n"

  • Goal: This approach will yield a contradiction with line n.

  • Option 2: Use a derived rule to break up the negation using the specified strategies below.

Breaking Up Negations Using Derived Rules

• Use Negation Conjunction (NC):

  • Turn $(~(PQ))$ into $(P ext{ and } ~Q)$.

• Use Negation Biconditional (NB):

  • Turn $(~(PQ))$ into $(P ext{ if and only if } Q)$.

• Use De Morgan's (DM):

  • Turn $(~(PVQ))$ into $(~P ext{ and } ~Q)$.

  • Turn $(~(PAQ))$ into $(~P ext{ or } ~Q)$.

Strategy #3: Using Previous Available Lines

• Condition: If a previous available line, n, is a conditional:

  • Options: There are two paths to pursue:

  • Option 1: Show the antecedent of line n.

    • Command: Use "Show ant n".

    • Goal: Assuming your Show line is on line m, after cancelling that Show, modus ponens can be applied using the command notation "m, n MP".

  • Option 2: Try to show the negation of the consequent line n.

    • Command: Use "Show negcons n".

    • Goal: This path allows for the application of modus tollens using the notation "m, n MT".

• Condition with Disjunctions: If a previous available line, n, is a disjunction:

  • Action: Try to show the negation of one of its disjuncts.

  • Command: Use "Show negdisj n".

  • Goal: This enables the application of modus tollendo ponens using the notation "m, n, MTP".