- AV
-
Meaning: Alphabetic Variation
Schema: None
Antecedent strength requirement: Ω<arg0>⊆Ω0
Examples:
-
Var 0 t;OK.
T1: ∀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))) Rep(T0);OK.
T2: ∀x(∀y(∀z(x+(y+z)=(x+y)+z))),∀x(x+-x=0),∀x(x+0=x)
⊨ ∀t(∀y(∀z(t+z=y+z→t=y))) AV(T1);OK.
-
Var 0 t;OK.
T1: ∀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))) Rep(T0);OK.
T2: ∀x(∀y(∀z(x+(y+z)=(x+y)+z))),∀x(x+-x=0),∀x(x+0=x)
⊨ ∀x(∀y(∀z(y+z=y+z→y=y))) AV(T1);Δ0 does not have form '∀χ0(∀χ1(∀χ2(((χ0+χ2)=(χ1+χ2))→(χ0=χ1))))' where the bound variables are typed as follows: χ0:0,χ1:0,χ2:0.
-
Var 0 t;OK.
T1: ∀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))) Rep(T0);OK.
T2: ∀x(x+-x=0),∀x(x+0=x)
⊨ ∀x(∀y(∀z(x+z=y+z→x=y))) AV(T1);ΩT1⊈Ω0. ΩT1 contains proposition '∀x(∀y(∀z((x+(y+z))=((x+y)+z))))' but Ω0 does not.
- Add1
-
Meaning:Addition (form 1)
Schema: ψ:θ∨ψ
Antecedent strength requirement: Ω<arg0>⊆Ω0
Examples:
-
T12: ⊨ ∀x(x∈N→x+1∈N) Rep(TS);OK.
T13: ⊨ ∀x(x∈N→x+1∈N)∨0≠0 Add1(T12);OK.
T12: ⊨ ∀x(x∈N→x+1∈N) Rep(TS);OK.
T13: ⊨ ∀x(x∈N→x+1∈N) Add1(T12);ΔT12:Δ0 does not match scheme θ:θ∨ψ.
- Add2
-
Meaning: Addition (form 2)
Schema: θ:θ∨ψ
Antecedent strength requirement: Ω<arg0>⊆Ω0
- Adj
-
Meaning: Adjunction
Schema: θ,ψ:θ∧ψ
Antecedent strength requirement: Ω<arg0>⋃Ω<arg1>⊆Ω0
- Asm
-
Meaning: Assumption
Schema: None
Antecedent strength requirement: None
Examples:
-
T1: Omega2a, Omega2b⊨ Delta2 {
T2:Omega1a, Omega1b, Omega1c ⊨Delta1{
T3: ⊨Omega2a Asm;OK.
T4: ⊨ Omega1a Asm;OK.
T5: Omega0 ⊨ Omega0 Asm;OK.
: ⊨Delta1 Rep(TA);OK.
};OK.
: ⊨Delta2 Rep(TB);OK.
} ;OK.
-
T1: Omega2a, Omega2b⊨ Delta2 {
T2:Omega1a, Omega1b, Omega1c ⊨Delta1{
T5: Omega0 ⊨ P Asm;Δ0 is not in (Ω0⋃Ω1)⋃Ω2.
: ⊨Delta1 Rep(TA);OK.
};Incorrect line inside subproof.
:⊨Delta2 Rep(TB);OK.
} ;Incorrect line inside subproof.
- BC1
-
Meaning: Biconditional-Conditional (form 1);
Schema: θ↔ψ:θ→ψ
Antecedent strength requirement: Ω<arg0>⊆Ω0
- BC2
-
Meaning: Biconditional-Conditional (form 2);
Schema: θ↔ψ:ψ→θ
Antecedent strength requirement: Ω<arg0>⊆Ω0
- CB
-
Meaning: Conditional-Biconditional;
Schema: θ→ψ,ψ→θ:θ↔ψ
Antecedent strength requirement: Ω<arg0>⋃Ω<arg1>⊆Ω0
- CD
-
Meaning: Conditional Disjunction;
Schema: (¬θ)→ψ:θ∨ψ
Antecedent strength requirement: Ω<arg0>⊆Ω0
- DN1
-
Meaning: Double Negation (Form 1);
Schema: θ:¬¬θ
Antecedent strength requirement: Ω<arg0>⊆Ω0
- DN2
-
Meaning: Double Negation (Form 2);
Schema: ¬¬θ:θ
Antecedent strength requirement: Ω<arg0>⊆Ω0
- Ded
-
Meaning: Deduction;
Schema: ψ:θ→ψ
Antecedent strength requirement: (Ω<arg0>∖θ)⊆Ω0
Examples:
-
T16: ∀x(∀y(∀z(x+(+z)=(x+y)+z))),∀x(x+-x=0),∀x(x+0=x)
⊨ ∀x(∀y(∀z(x+z=y+z→x=y))) Rep(T0);OK.
T17: ∀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))) Ded(T16);OK.
-
T16: ∀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))) Rep(T0);OK.
T17: ∀x(∀y(∀z(x+(y+z)=(x+y)+z)))
⊨ ∀x(x+0=x) →∀x(∀y(∀z(x+z=y+z→x=y))) Ded(T16);For underlined subexpression θ of Δ0, (ΩT16∖θ)⊈Ω0. (Proposition '∀x((x+(-x))=0)' is in ΩT16∖θ, but is not in Ω0).
- DeepSubLR
-
Meaning: Δarg1 must either have form ∀χ0(…(∀χn(θ≡ψ))) or form θ≡ψ. Subexpressions of Δ<arg0> are considered relatively free if they are generally free or if the only variables that would be captured from the outside are among ∀χ0…∀χn. Δ0 should be Δ<arg0> after some relatively free occurences of θ are replaced by ψ, which must also remain relatively free within Δ0. This rule completely subsumes the SubLR rule.
Schema: None
Antecedent strength requirement: Ω<arg0>⋃Ω<arg1>⊆Ω0
Examples:
-
Var 0 x;OK.
Var 0 y;OK.
Const 1 P(x);OK.
Const 1 Q(x);OK.
T0: ⊨ ∀x(P(x)) Cheat;OK.
T1: ⊨ ∀x(∀y(P(x)↔Q(y))) Cheat;OK.
T2: ⊨ ∀x(Q(y)) DeepSubLR(T0,T1);OK.
-
Var 0 x;OK.
Var 0 y;OK.
Var 0 u;OK.
Const 1 P(x,u);OK.
Const 1 Q(x,u);OK.
T0: ⊨ ∀x(∀y(P(x,u))) Cheat;OK.
T1: ⊨ ∀u(∀x(P(x,u))) Cheat;OK.
T2: ⊨ ∀x(∀y(Q(y,u))) DeepSubLR(T0,T1);ΔT1 does not have form ∀χ0(…(∀χn(θ≡ψ))) or form θ≡ψ.
-
Var 0 x;OK.
Var 0 y;OK.
Var 0 u;OK.
Const 1 P(x,u);OK.
Const 1 Q(x,u);OK.
T0: ⊨ ∀u(∀x(P(x,u))) Cheat;OK.
T1: ⊨ ∀u(∀x(P(x,u)↔Q(y,u))) Cheat;OK.
T2: ⊨ ∀u(∀x(Q(u,u))) DeepSubLR(T0,T1);ΔT1 has form ∀χ0(…(∀χn(θ≡ψ))) or form θ≡ψ, but Δ0 was not formed by replacing some relatively free occurences of θ in ΔT0 with ψ.
-
Var 0 x;OK.
Var 0 y;OK.
Var 0 u;OK.
Const 1 P(x,u);OK.
Const 1 Q(x,u);OK.
T0: ⊨ ∀x(∀y(P(x,u))) Cheat;OK.
T1: ⊨ ∀u(∀x(P(x,u)↔Q(y,u))) Cheat;OK.
T2: ⊨ ∀x(∀y(Q(y,u))) DeepSubLR(T0,T1);Variable capture after relatively free occurence 0 of expression 'P(x,u)' in ΔT0 replaced with expression 'Q(y,u)'.
- DeepSubRL
-
Meaning: Δarg1 must either have form ∀χ0(…(∀χn(θ≡ψ))) or form θ≡ψ. Subexpressions of Δ<arg0> are considered relatively free if they are generally free or if the only variables that would be captured from the outside are among ∀χ0…∀χn. Δ0 should be Δ<arg0> after some relatively free occurences of ψ are replaced by θ, which must also remain relatively free within Δ0. This rule completely subsumes the SubRL rule.
Schema: None
Antecedent strength requirement: Ω<arg0>⋃Ω<arg1>⊆Ω0
- Def
-
Meaning: Apply Definition;
Schema: None
Antecedent strength requirement: None
Example:
T18:⊨x∈N→x+0=x Cheat;OK.
Const 0 sum(x,y)≜x+y;OK.
T19: ⊨ sum(a,b)=a+b Def(sum);OK.
- E2EScream
-
Meaning: Existential quantifier to unique quantifier;
Schema: None
Antecedent strength requirement: Ω<arg0>⊆Ω0
Example:
T3:⊨∃z((z=z)∧∀y((y=y)→(y=z))) Cheat;OK.
T2:⊨∃!z(z=z) E2EScream(T3);OK.
- EG
-
Meaning: Existential Generalisation;
Schema: None
Antecedent strength requirement: Ω<arg0>⊆Ω0
Example:
T1:⊨y=ιx(y=y→y=x) Cheat;OK.
T5:⊨∃z(z=ιx(y=z→y=x)) EG(T1);OK.
- EI
-
Meaning: Existential Instantiation;
Schema: None
Antecedent strength requirement: Ω<arg0>⊆Ω0
Examples:
-
T1:⊨∃x(x=x) Cheat;OK.
T4:⊨ιx(x=x)=ιx(x=x) EI(T1);OK.
-
T1:⊨∃x(∀y(x=y)) Cheat;OK.
T4:⊨∀y(x=y) EI(T1);Δ0 does not have form '∀y(θ=y)' after θ replaced with expression 'ιx(∀y(x=y))'.
- EScream2E
-
Meaning: Exists to Uniquely exists
Schema: None
Antecedent strength requirement: Ω<arg0>⊆Ω0
Examples:
T2:⊨∃!z(z=z) Cheat;OK.
T3:⊨∃!z(z=z) Rep(T2);OK.
T1:⊨∃z((z=z)∧∀y((y=y)→(y≡z))) EScream2E(T2,y);OK.
-
T3:⊨∃!z(z=z) Rep(T2);OK.
T4:⊨∃z((z=z)∧∀z((z=z)→(z≡z))) EScream2E(T2,z);ΔT2 has form ∃!χ(θ), but z occurs free in θ.
- FuncId
-
Meaning: Identity of functions that map to the same values.
Schema: None
Antecedent strength requirement: Ω<arg0>⊆Ω0
Example:
T1: ⊨∀x(∀y((q(h))(x,y)≡(f(x,y)))) Cheat;OK.
T2: ⊨q(h)≡f Funcid(T1);OK.
- Id
-
Meaning: Identity Law
Schema: θ≡θ
Antecedent strength requirement: None
Example:
T20: ⊨ x=x Id;OK.
T21: ⊨ sum≡sum Id;OK.
T22: ⊨ x∈N↔x∈N Id;OK.
- Lambda
-
Meaning: Lambda Reduction;
Schema: None
Antecedent strength requirement: None
Example:
T1:⊨λt(y(u,f(f(t))))(u)= y(u,f(f(u)))Lambda;OK.
- MP
-
Meaning: Modus Ponens
Schema: θ→ψ,θ:ψ
Antecedent strength requirement: Ω<arg0>⋃Ω<arg1>⊆Ω0
- MT
-
Meaning: Modus Tollens
Schema: θ→ψ,¬ψ:¬θ
Antecedent strength requirement: Ω<arg0>⋃Ω<arg1>⊆Ω0
- MTP1
-
Meaning: Modus Tollendo Ponens (Form 1)
Schema: θ∨ψ,¬θ:ψ
Antecedent strength requirement: Ω<arg0>⋃Ω<arg1>⊆Ω0
- MTP2
-
Meaning: Modus Tollendo Ponens (Form 2)
Schema: θ∨ψ,¬ψ:θ
Antecedent strength requirement: Ω<arg0>⋃Ω<arg1>⊆Ω0
- NC1
-
Meaning: Non-Contradiction (Law 1)
Schema: θ→(¬θ):¬θ
Antecedent strength requirement: Ω<arg0>⊆Ω0
Example:
Const 1 P;OK.
T1:⊨ P→¬P Cheat;OK.
T2:⊨ ¬P NC1(T1);OK.
- NC2
-
Meaning: Non-Contradiction (Law 2)
Schema: θ,¬θ:ψ
Antecedent strength requirement: Ω<arg0>⋃Ω<arg1>⊆Ω0
Example:
Const 1 P;OK.
Const 1 Q;OK.
T1:⊨ P Cheat;OK.
T2:⊨ ¬P Cheat;OK.
T3:⊨ Q NC2(T1,T2);OK.
- QN1
-
Meaning: Quantifier Negation (Form 1)
Schema: None
Antecedent strength requirement: Ω<arg0>⊆Ω0
Example:
T15: ⊨ ∀x(¬(x=3)) Cheat;OK.
T16: ⊨ ¬∃x(x=3) QN1(T15);OK.
- QN2
-
Meaning: Quantifier Negation (Form 2)
Schema: None
Antecedent strength requirement: Ω<arg0>⊆Ω0
Example:
T15: ⊨ ∃x(¬(x=3)) Cheat;OK.
T16: ⊨ ¬∀x(x=3) QN2(T15);OK.
- QN3
-
Meaning: Quantifier Negation (Form 3)
Schema: None
Antecedent strength requirement: Ω<arg0>⊆Ω0
Example:
T15: ⊨ ¬∀x(x=3) Cheat;OK.
T16: ⊨ ∃x(¬(x=3)) QN3(T15);OK.
- QN4
-
Meaning: Quantifier Negation (Form 4)
Schema: None
Antecedent strength requirement: Ω<arg0>⊆Ω0
Example:
T15: ⊨ ¬∃x(x=3) Cheat;OK.
T16: ⊨ ∀x(¬(x=3)) QN4(T15);OK.
- SC1
-
Meaning: Separation of Cases (Form 1)
Schema: θ→ψ,(¬θ)→ψ:ψ
Antecedent strength requirement: Ω<arg0>⋃Ω<arg1>⊆Ω0
- SC2
-
Meaning: Separation of Cases (Form 2)
Schema: θ∨ψ,θ→χ,ψ→χ:χ
Antecedent strength requirement: Ω<arg0>⋃Ω<arg1>⋃Ω<arg2>⊆Ω0
- SC3
-
Meaning: Separation of Cases (Form 3)
Schema: θ→χ,ψ→χ:(θ∨ψ)→χ
Antecedent strength requirement: Ω<arg0>⊆Ω0
- SubLR
-
Meaning: In Δ<arg0>, replace some free occurences of left side of Δ<arg1> with right side of Δ<arg1>.
Schema: None
Antecedent strength requirement: Ω<arg0>⋃Ω<arg1>⊆Ω0
Example:
Const 0 c;OK.
Var 0 d;OK.
T0:⊨∀d(d=[c,d,c,d])∨c=d Cheat;OK.
T1:⊨c≡[d,d,c,d] Cheat;OK.
T2:⊨∀d(d=[c,d,c,d])∨[d,d,c,d]=d SubLR(T0,T1);OK.
- SubRL
-
Meaning: In Δ<arg0>, replace some free occurences of right side of Δ<arg1> with left side of Δ<arg1>.
Schema: None
Antecedent strength requirement: Ω<arg0>⋃Ω<arg1>⊆Ω0
- UG
-
Meaning: Universal Generalisation
Schema: None
Antecedent strength requirement: Ω<arg0>⊆Ω0
Examples:
-
Var 0 x;OK.
Var 0 z;OK.
T1:⊨x=x Cheat;OK.
T2:⊨∀z(x=x) {
Var 0 y;OK.
T3: ⊨∀y(x=x) UG(T1,y);OK.
: ⊨ ∀z(x=x) AV(T3);OK.
};OK.
-
Var 0 x;OK.
Var 0 z;OK.
T1:⊨x=x Cheat;OK.
T2:⊨∀z(x=x) {
Var 0 y;OK.
T3: ⊨∀y(x=x) UG(T1,z);Variable z was defined in a lower context, and therefore not universally genereraliseable.
: ⊨ ∀z(x=x) AV(T3);Atom 'T3' is not defined.
};Incorrect line inside subproof.
- UI
-
Meaning: Universal Instantiation
Schema: None
Antecedent strength requirement: Ω<arg0>⊆Ω0
Example:
T12: ∀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))) Rep(T0);OK.
T13: ∀x(∀y(∀z(x+(y+z)=(x+y)+z))),∀x(x+-x=0),∀x(x+0=x)
⊨ ∀y(∀z((6+3)+z=y+z→(6+3)=y)) UI(T12);OK.