PCP Theories

PCP: Brief Instructions and Description

Peter Jipsen, 2001

The PCP system splits the browser window vertically into two frames. The left frame contains the (partial) proof, and the narrower right frame contains the possible choices available for the next step.

Initially the proof frame contains a list of axioms and formulas to be proved, with the latter preceded by a line of the form ...^...v...

This line indicates a gap in a proof and the two arrow symbols point at the line above and below the gap respectively. Each symbol is a button that can be clicked to direct the focus of subsequent actions to that line of the proof. The line with the current focus has an undo button instead of one of the arrow symbols, and also a hide/show button.

The undo button deletes the focus step of the proof (although main level proof steps cannot be undone presently).

The hide/show button allows subproofs and other gaps to be hidden so that the user can focus on the part of the proof that is currently of interest.

Each proof step is numbered, and subproofs are numbered like subsections in a book. Proof steps with a numbered button correspond to a rule which can be applied at the current focus step.

Clicking a numbered button (which does not correspond to a gap) applies the rule and produces in the choose frame a list of possible expressions (perhaps none) to be inserted at the focus. In some case one may need to apply a substitution to the possible expressions. Variables are substituted by terms that have to be typed in a fairly natural ascii syntax (e.g. x ^^ (y vv x), spaces are optional; ^^ is the meet symbol, ^ is for superscripts, vv is the join symbol, v is a variable). A more complete description of the syntax for formulas is in preparation. A look at the HTML source of the main frame of a PCP proof page may be helpful.

Selecting one of these expressions modifies the proof at the focus. If the focus was above the gap, the rule is applied in a forward reasoning fashion. If the focus is below the gap, each conjunct of the selected expression that still needs to be proved is inserted with a new gap above it.

Clicking a numbered button of a gap inserts a new subproof. The type of the subproof depends on what expression is below the gap:

Standard Subproof: If the expression below the gap is an implication, then the premises are inserted as separate proof steps at the start of the subproof, and the conclusion is inserted at the end. (If the conclusion is a conjunction it is currently not split into separate conjuncts). Also the variables x, y, z, w are replaced by constants a, b, c, d to prevent the premises being applied as if they were universally quantified.
Iff Subproof: If the expression below the gap is an if and only if, then the left hand side formula is inserted at the start of the subproof, and the right hand side formula is inserted at the end.
(In)equational Subproof: If the expression below the gap is an equation or inequation, then the left hand side term is inserted at the start of the subproof, and the right hand side term is inserted at the end.

(Standard subproofs are similar to subproofs in Hilbert style or Fitch style natural deduction proof systems, and can themselves have subproofs. Iff subproofs and (In)equational subproofs are similar to linear proofs of Backhouse, Gries and Schneider. They cannot have further subproofs.)

The proof format

Here is an example of a main PCP page that shows the JavaScript syntax for a partial proof (always assigned to the global variable currentProof). Look at PCPsemilattices.html to see how this proof is displayed in the PCP environment. To implement and explore your own theories, the simplest is currently to copy and modify such an example webpage.

proofHeader="\
<b>Proposition:</b> Every semilattice is a meet-semilattice.<br>\
<b>Proof:</b><br>";

currentProof=[
  {expr:"x*y*z=x*(y*z)",  axiom:true, name:"associativity"},
  {expr:"x*y=y*x",        axiom:true, name:"commutativity"},
  {expr:"x*x=x",          axiom:true, name:"idempotence"},
  {expr:"x<=y iff x*y=x", axiom:true, name:"leq definition"},
  {expr:"...",                          gap:true},
  {expr:"x<=x",                         name:"reflexivity"},
  {expr:"...",                          gap:true},
  {expr:"x<=y and y<=x implies x=y",    name:"antisymmetry"},
  {expr:"...",                          gap:true},
  {expr:"x<=y and y<=z implies x<=z",   name:"transitivity"},
  {expr:"...",                          gap:true},
  {expr:"x*y<=x",                       name:"lower bound"},
  {expr:"...",                          gap:true},
  {expr:"x*y<=y",                       name:"lower bound"},
  {expr:"...",                          gap:true},
  {expr:"z<=x and z<=y implies z<=x*y", name:"infimum"}
];

parseProof(currentProof);

The JavaScript Code

The PCP system consists of two parts:

a parser for the ascii syntax of mathematical formulas and the output of HTML (math2html.js), and
the interactive proof editor (PCPproof.js)

Each part is about 500 lines of code, although the parser is considerably more general than it needs to be for the current version of PCP. (It is usable for translating a simplified TeX-like webpage into mathematical HTML.) On the other hand the parser also still has some significant shortcomings in how it handles syntactically incorrect input. Neither of these files is properly documented at this point.

A functioning PCP webpage (like PCPsemilattices.html) contains the initial partial proof, and also requires the two frame pages PCPproof.html and PCPchoose.html (which remain the same for all PCP webpages).