Proof by contradiction and proof by cases are two common forms for mathematical proofs. Recalling the general node format (Listing 7), both of these proof structures are encoded using node `MODIFIERS`.

Proofs by contradiction use the `contra` modifier.

To encode a proof by contradiction:

• Deduce a `flse` node from a set of nodes (often just two) that are mutually contradictory.

• Link the `flse` node to a `supp` node using the `contra` modifier.

Example:

Listing 14 A proof by contradiction#
```deduc Thm {
supp S {
sy="\$S\$"
}
asrt A {
sy="\$A\$"
}
meson="Suppose S. Then A."
}

deduc Pf of Thm.A {

supp T {
en="Suppose not \$A\$."
}

asrt B {
sy="\$B\$"
}

asrt C {
sy="\$C\$"
}

asrt D {
sy="\$D\$"
}

flse F contra T {}

meson = "
Suppose T. Then B and C. From C get D, using Thm.S, hence F, by B.
Therefore Thm.A.
"
}
```

When a proof is displayed in PISE, the `contra` modifier activates the “up tack” or falsum symbol on the `flse` node, so that hovering highlights the contradicted `supp` node, and clicking brings it on screen.

## Proof by cases#

Proofs by cases use the `versus` modifier.

To encode a proof by cases:

• Use a set of `subdeduc` nodes, one for each case.

• Start each `subdeduc` with a `supp` node, indicating the assumption that defines the case.

• On one of these `supp` nodes, use the `versus` modifier to link it with the alternative cases.

• Deduce the common conclusion, citing each of the `subdeduc` nodes as reason.

Example:

Listing 15 A proof by cases#
```deduc Thm {
supp S {
sy="\$S\$"
}
asrt A {
sy="\$A\$"
}
meson="Suppose S. Then A."
}

deduc Pf of Thm.A {

subdeduc caseX {
supp X {
sy="\$X\$"
}
asrt B {
sy="\$B\$"
}
asrt A {
sy="\$A\$"
}
meson = "Suppose X. Then B, hence A, by Thm.S."
}

subdeduc caseY {
supp Y versus caseX.X {
sy="\$Y\$"
}
asrt C {
sy="\$C\$"
}
asrt A {
sy="\$A\$"
}
meson = "Suppose Y. Then C by Thm.S, hence A."
}

meson = "Thm.A by caseX and caseY."

}
```
When a proof is displayed in PISE, the `versus` modifier adds a “CASE” label to each of the `supp` nodes that define the cases. The “CASE” label is activated, so that hovering highlights the case `supp` nodes, and clicking brings them on screen.