THE DERIVATION RULES

AV

Meaning: Alphabetic Variation
Schema: None
Antecedent strength requirement: Ω_<arg0>⊆Ω₀
Examples:

1. 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.
2. 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.
3. 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>⊆Ω₀
Examples:

1. 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>⊆Ω₀

Adj

Meaning: Adjunction
Schema: θ,ψ:θ∧ψ
Antecedent strength requirement: Ω_<arg0>⋃Ω_<arg1>⊆Ω₀

Asm

Meaning: Assumption
Schema: None
Antecedent strength requirement: None
Examples:

1. 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.
2. 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>⊆Ω₀

BC2

Meaning: Biconditional-Conditional (form 2);
Schema: θ↔ψ:ψ→θ
Antecedent strength requirement: Ω_<arg0>⊆Ω₀

CB

Meaning: Conditional-Biconditional;
Schema: θ→ψ,ψ→θ:θ↔ψ
Antecedent strength requirement: Ω_<arg0>⋃Ω_<arg1>⊆Ω₀

CD

Meaning: Conditional Disjunction;
Schema: (¬θ)→ψ:θ∨ψ
Antecedent strength requirement: Ω_<arg0>⊆Ω₀

DN1

Meaning: Double Negation (Form 1);
Schema: θ:¬¬θ
Antecedent strength requirement: Ω_<arg0>⊆Ω₀

DN2

Meaning: Double Negation (Form 2);
Schema: ¬¬θ:θ
Antecedent strength requirement: Ω_<arg0>⊆Ω₀

Ded

Meaning: Deduction;
Schema: ψ:θ→ψ
Antecedent strength requirement: (Ω_<arg0>∖θ)⊆Ω₀
Examples:

1. 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.
2. 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. Δ₀ should be Δ_<arg0> after some relatively free occurences of θ are replaced by ψ, which must also remain relatively free within Δ₀. This rule completely subsumes the SubLR rule.
Schema: None
Antecedent strength requirement: Ω_<arg0>⋃Ω_<arg1>⊆Ω₀
Examples:

1. 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.
2. 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 θ≡ψ.
3. 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 ψ.
4. 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. Δ₀ should be Δ_<arg0> after some relatively free occurences of ψ are replaced by θ, which must also remain relatively free within Δ₀. This rule completely subsumes the SubRL rule.
Schema: None
Antecedent strength requirement: Ω_<arg0>⋃Ω_<arg1>⊆Ω₀

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>⊆Ω₀
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>⊆Ω₀
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>⊆Ω₀
Examples:

1. T1:⊨∃x(x=x) Cheat;OK. T4:⊨ιx(x=x)=ιx(x=x) EI(T1);OK.
2. 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>⊆Ω₀
Examples:

1. 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.
2. 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>⊆Ω₀
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>⊆Ω₀

MT

Meaning: Modus Tollens
Schema: θ→ψ,¬ψ:¬θ
Antecedent strength requirement: Ω_<arg0>⋃Ω_<arg1>⊆Ω₀

MTP1

Meaning: Modus Tollendo Ponens (Form 1)
Schema: θ∨ψ,¬θ:ψ
Antecedent strength requirement: Ω_<arg0>⋃Ω_<arg1>⊆Ω₀

MTP2

Meaning: Modus Tollendo Ponens (Form 2)
Schema: θ∨ψ,¬ψ:θ
Antecedent strength requirement: Ω_<arg0>⋃Ω_<arg1>⊆Ω₀

NC1

Meaning: Non-Contradiction (Law 1)
Schema: θ→(¬θ):¬θ
Antecedent strength requirement: Ω_<arg0>⊆Ω₀
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>⊆Ω₀
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>⊆Ω₀
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>⊆Ω₀
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>⊆Ω₀
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>⊆Ω₀
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>⊆Ω₀

SC2

Meaning: Separation of Cases (Form 2)
Schema: θ∨ψ,θ→χ,ψ→χ:χ
Antecedent strength requirement: Ω_<arg0>⋃Ω_<arg1>⋃Ω_<arg2>⊆Ω₀

SC3

Meaning: Separation of Cases (Form 3)
Schema: θ→χ,ψ→χ:(θ∨ψ)→χ
Antecedent strength requirement: Ω_<arg0>⊆Ω₀

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>⊆Ω₀
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>⊆Ω₀

UG

Meaning: Universal Generalisation
Schema: None
Antecedent strength requirement: Ω_<arg0>⊆Ω₀
Examples:

1. 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.
2. 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>⊆Ω₀
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.