EXAMPLE OF USING THE PROGRAM
You can enter in proofs bit by bit and check as you go. However, you must always close subproofs, whether completed or not, in order to avoid syntax errors. For instance one might enter in the following and then hit "Check proof"
Var 0 x;
Var 0 y;
Var 0 z;
Var 0 a;
Var 0 b;
Var 0 c;
Const 0 x+y;
Const 0 -x;
T0: ∀x(∀y(∀z(x+(y+z)=(x+y)+z))),∀x(x+-x=0),∀x(x+0=x)
⊨ ∀x(∀y(∀z(x+z=y+z→x=y))) {
Var 0 u;
Var 0 v;
but the result will be the message, "Position: 10,0: syntax error, unexpected $end" in the message pane. Therefore the user should have added a closing brace and a semi-colon before hitting check proof, in which case the result would be as follows:
Var 0 x;OK.
Var 0 y;OK.
Var 0 z;OK.
Var 0 a;OK.
Var 0 b;OK.
Var 0 c;OK.
Const 0 x+y;OK.
Const 0 -x;OK.
T0: ∀x(∀y(∀z(x+(y+z)=(x+y)+z))),∀x(x+-x=0),∀x(x+0=x)
⊨ ∀x(∀y(∀z(x+z=y+z→x=y))) {
Var 0 u;OK.
Var 0 v;OK.
};Last line of subproof is not result step.
The user might proceed to enter in some more lines, hit check proof, and this time some errors might be found.
Var 0 x;OK.
Var 0 y;OK.
Var 0 z;OK.
Var 0 a;OK.
Var 0 b;OK.
Var 0 c;OK.
Const 0 x+y;OK.
Const 0 -x;OK.
T0: ∀x(∀y(∀z(x+(y+z)=(x+y)+z))),∀x(x+-x=0),∀x(x+0=x)
⊨ ∀x(∀y(∀z(x+z=y+z→x=y))) {
Var 0 u;OK.
Var 0 v;OK.
Var 0 w;OK.
T4: u+w=v+w ⊨ u=v {
T1: ⊨ (u+w)+-w=(u+w)+-w Id;OK.
T2: ⊨ u+w=v+w Asm;OK.
T3: ⊨ (u+w)+-w=(v+w)+-w SubLR(T1,T2);OK.
T4: ⊨ u+(w+-w)=(u+w)+-w{
T4A: ⊨ ∀x(∀y(∀z(x+(y+z)=(x+y)+z))) Asm;OK.
T4B: ⊨ ∀y(∀z(u+(y+z)=(u+y)+z)) UI(T4A);OK.
T4C: ⊨ ∀z(u+(w+z)=(u+w)+z) UI(T4B);OK.
: ⊨ u+(w+-w)=(u+w)+-w UI(T4C);OK.
};OK.
T5: ⊨ v+(w+-w)=(v+w)+-w{
T5A: ⊨ ∀x(∀y(∀z(x+(y+z)=(x+y)+z))) Asm;OK.
T5B: ⊨ ∀y(∀z(v+(y+z)=(v+y)+z)) UI(T5A);OK.
T5C: ⊨ ∀z(v+(z+z)=(v+z)+z) UI(T5B);Variable capture after θ in expression '∀z((v+(θ+z))=((v+θ)+z))' replaced with expression 'z'.
: ⊨ v+(w+-w)=(v+w)+-w UI(T5C);Atom 'T5C' is not defined.
};Incorrect line inside subproof.
T6: ⊨ u+(w+-w)=(v+w)+-w SubRL(T3,T4);OK.
T7: ⊨ u+(w+-w)=v+(w+-w) SubRL(T6,T5);Atom 'T5' is not defined.
};Incorrect line inside subproof.
};Incorrect line inside subproof.
When the user is done, if her or his proof is correct, when she or he hits check proof, the result will look something like this:
Var 0 x;OK.
Var 0 y;OK.
Var 0 z;OK.
Var 0 a;OK.
Var 0 b;OK.
Var 0 c;OK.
Const 0 x+y;OK.
Const 0 -x;OK.
T0: ∀x(∀y(∀z(x+(y+z)=(x+y)+z))),∀x(x+-x=0),∀x(x+0=x)
⊨ ∀x(∀y(∀z(x+z=y+z→x=y))) {
Var 0 u;OK.
Var 0 v;OK.
Var 0 w;OK.
T4: u+w=v+w ⊨ u=v {
T1: ⊨ (u+w)+-w=(u+w)+-w Id;OK.
T2: ⊨ u+w=v+w Asm;OK.
T3: ⊨ (u+w)+-w=(v+w)+-w SubLR(T1,T2);OK.
T4: ⊨ u+(w+-w)=(u+w)+-w{
T4A: ⊨ ∀x(∀y(∀z(x+(y+z)=(x+y)+z))) Asm;OK.
T4B: ⊨ ∀y(∀z(u+(y+z)=(u+y)+z)) UI(T4A);OK.
T4C: ⊨ ∀z(u+(w+z)=(u+w)+z) UI(T4B);OK.
: ⊨ u+(w+-w)=(u+w)+-w UI(T4C);OK.
};OK.
T5: ⊨ v+(w+-w)=(v+w)+-w{
T5A: ⊨ ∀x(∀y(∀z(x+(y+z)=(x+y)+z))) Asm;OK.
T5B: ⊨ ∀y(∀z(v+(y+z)=(v+y)+z)) UI(T5A);OK.
T5C: ⊨ ∀z(v+(w+z)=(v+w)+z) UI(T5B);OK.
: ⊨ v+(w+-w)=(v+w)+-w UI(T5C);OK.
};OK.
T6: ⊨ u+(w+-w)=(v+w)+-w SubRL(T3,T4);OK.
T7: ⊨ u+(w+-w)=v+(w+-w) SubRL(T6,T5);OK.
T8: ⊨ ∀x(x+-x=0) Asm;OK.
T9: ⊨ w+-w=0 UI(T8);OK.
T10: ⊨ u+0=v+0 SubLR(T7,T9);OK.
T11: ⊨ ∀x(x+0=x) Asm;OK.
T12: ⊨ u+0=u UI(T11);OK.
T13: ⊨ v+0=v UI(T11);OK.
T14: ⊨ u=v+0 SubLR(T10,T12);OK.
: ⊨ u=v SubLR(T14,T13);OK.
};OK.
T5: ⊨ u+w=v+w → u=v Ded(T4);OK.
T6: ⊨ ∀w(u+w=v+w→u=v) UG(T5,w);OK.
T7: ⊨ ∀v(∀w(u+w=v+w→u=v)) UG(T6,v);OK.
T8: ⊨ ∀u(∀v(∀w(u+w=v+w→u=v))) UG(T7,u);OK.
: ⊨ ∀x(∀y(∀z(x+z=y+z→x=y))) AV(T8);OK.
};OK.
