This help does neither explain the "mechanics" of the proof builder nor the syntax of the formal language the applet uses. Both topics are covered separately.

The Peirce-style Proof Builder covers the derivation rules for the Alpha part of Peirce's Existential Graphs, i.e. their propositional subset. The rules are used just like presented by Don D. Roberts in his book The Existential Graphs of Charles S. Peirce (chapter 3.2, The Alpha rules of transformation, pp. 40-44, and again summarized in appendix 3, pp. 137-138). Both the short overview I am about to give and the numbering of the rules follow closely Robert's presentation.

*Definition:* The level of a proposition (be it simple or complex)
be defined as the number of cuts this proposition is part of. E.g. in the
proposition `PQ(RS(TU))`

, there are the following propositions
occuring at the following levels:

Proposition | Level |
---|---|

`P` | 0 |

`Q` | 0 |

`(RS(TU))` | 0 |

`PQ` | 0 |

`PQ(RS(TU))` | 0 |

`R` | 1 |

`S` | 1 |

`(TU)` | 1 |

`RS` | 1 |

`S(TU)` | 1 |

`T` | 2 |

`U` | 2 |

`TU` | 2 |

The rule of assertion is kind of a pseudo rule, its sole purpuse lying in allowing you to start your derivation by writing down the premiss. Just enter the premiss in the text field "Proposition entry" and select "Assertion" to start your derivation. Remember that in Peirce's system, asserting more than one proposition means to concatenate them. So, if you have more than one premiss to derive from, concatenate them all and assert the whole thing.

Every proposition, be it simple
or complex, may be dropped *if it occurs at an even level*.
Example: from `PQ(RS(TU))`

, *erasure* allows to
derive each of the following propositions: `Q(RS(TU))`

(erasing `P`

), `P(RS(TU))`

(erasing
`Q`

), and `PQ`

(erasing `(RS(TU))`

).
Erasing more than one proposition at the same time by e.g.
directly deriving `P`

from the above example
(thereby erasing `Q(RS(TU))`

in a single step)
is supported, but should be avoided.

You may insert any proposition, be it simple or complex, provided
the insertion is taking place *at odd level*. Given the proposition
`P(Q(R(S)))`

, you may insert any proposition `X`

at
the level of Q (odd level 1), and at the level of S (odd level 3), thereby
deriving e.g. `P(XQ(R(S)))`

or `P(Q(R(XS)))`

.

The rule of iteration simply states that you may repeat any occurring
proposition `X`

at the same level or at a deeper level,
but not within `X`

itself. Hence, from `P(Q(R(S)))`

,
you may iterate `P`

, deriving e.g. `PP(Q(R(S)))`

,
`P(PQ(R(S)))`

, `P(Q(PR(S)))`

, or
`P(Q(R(PS)))`

; you may iterate `Q`

, deriving
e.g. `P(QQ(R(S)))`

, `P(Q(QR(S)))`

, or
`P(Q(R(QR)))`

; you may iterate `R`

, thereby
deriving e.g. `P(Q(RR(S)))`

or `P(Q(R(RS)))`

;
and you may iterate `S`

, thus deriving
`P(Q(R(SS)))`

.

This rule simply inverts R3 (i.e. iteration). It states that if
(and only if) it is possible to derive `Y`

from
`X`

by R3 (i.e. iteration), it is allowed to derive
`X`

from `Y`

, calling this step an application
of R4, deiteration.

The rule of the double cut is probably the simplest of all derivation rules. It states that you may at liberty insert and remove double cuts, wherever and whenever you like.

© Christian Gottschall / christian.gottschall@posteo.de / 2012-03-31 01:19:53