E-intro from Kaye ex 9.10, not all occurrences of bound variable substituted (0) Comment x = x (1) Reflexivity Ev.(v = x) (2) E-Introduction (1) True Erroneous E-intro from Kaye ex 9.10, bound variable does not match (0) Comment x = x (1) Reflexivity Ev.(w = x) (2) E-Introduction (1) Fail: Ev.(w = x) does not match Ev1.S1 with { S1:x = x, v1:v } False A-elim from Kaye ex 9.10 (0) Comment Ax.Ev.(v = x) (1) Given Ev.(v = w) (2) A-Elimination (1) True Erroneous A-elim from Kaye ex 9.10, bound variable does not match (0) Comment Ax.Ev.(v = x) (1) Given Ev.(w = x) (2) A-Elimination (1) Fail: Ev.(w = x) does not match P1 with { v1:x, P1:Ev.(v = x) } False P(t), Ax.(P(x) -> ~Q(x)) |- ~Q(t) using Ae from H&R p. 111 (0) Comment P(t) (1) Given Ax.(P(x) -> ~Q(x)) (2) Given P(t) -> ~Q(t) (3) A-Elimination (2) ~Q(t) (4) Implication-Elimination (Modus Ponens) (3) (1) True Ax.P(x) -> Ex.P(x) using Ae, Ei from H&R p. 114 (0) Comment Ax.P(x) (1) Given P(x) (2) A-Elimination (1) Ex.P(x) (3) E-Introduction (2) True Valid subst. of *free* var into quantified formula, Kay ex 9.9 (0) Comment t = g(y,z) (1) Given Ex.(x = f(t)) (2) Given Ex.(x = f(g(y,z))) (3) Substitution (1) (2) True Valid subst. of *free* var into *some* occurences in quantified formula, Kay ex 9.9 (0) Comment x = y (1) Given Ez.(x = f(x,z)) (2) Given Ez.(x = f(y,z)) (3) Substitution (1) (2) True Erroneous subst. of bound var into quantified formula, Kay ex 9.9 (0) Comment t = x (1) Given Ex.(x = f(t)) (2) Given Ex.(x = f(x)) (3) Substitution (1) (2) Fail: replacement term x includes bound variable in ['x'] False Erroneous subst. of bound var into quantified formula, Kay ex 9.9 (0) Comment t = g(x,y) (1) Given Ex.(x = f(t)) (2) Given Ex.(x = f(g(x,y))) (3) Substitution (1) (2) Fail: replacement term g(x,y) includes bound variable in ['x'] False Erroneous use of bound var as source of subst. into quant. form (0) Comment x = y (1) Given Ex.(x = f(x,z)) (2) Given Ex.(y = f(y,z)) (3) Substitution (1) (2) Fail: source term x includes bound variable in ['x'] False Erroneous appearance of bound var in source of subst. into quant. form (0) Comment f(x,z) = g(y,z) (1) Given Ex.(x = f(x,z)) (2) Given Ex.(x = g(y,z)) (3) Substitution (1) (2) Fail: source term f(x,z) includes bound variable in ['x'] False Correct A-elim similar to erroneous example H&R ex 2.11, R(x,y) is x < y (0) Comment Ax.Ey.R(x,y) (1) Given Ey.R(z,y) (2) A-Elimination (1) True Erroneous A-elim similar to H&R ex 2.11, R(x,y), wrong variable substituted (0) Comment Ax.Ey.R(x,y) (1) Given Ey.R(x,z) (2) A-Elimination (1) Fail: Ey.R(x,z) does not match P1 with { v1:x, P1:Ey.R(x,y) } False Erroneous A-elim similar to H&R ex 2.11, R(x,y), variable order reversed (0) Comment Ax.Ey.R(x,y) (1) Given Ey.R(y,z) (2) A-Elimination (1) Fail: replacement term y includes bound variable in ['y'] False Erroneous A-elim with subst of bound variable into nested quantified formula, H&R ex 2.11 (0) Comment Ax.Ey.R(x,y) (1) Given Ey.R(y,y) (2) A-Elimination (1) Fail: replacement term y includes bound variable in ['y'] False Erroneous E-intro with subst of bound variable into nested quantified formula, similar to H&R ex 2.11 (0) Comment Ay.R(y,z) (1) Given Ex.Ay.R(x,z) (2) E-Introduction (1) Fail: source term y includes bound variable in ['v1', 'y'] False Valid substitution, source variable whose name is bound in inner scope (0) Comment x = z (1) Given ~P(x) & Ax.R(x,y) (2) Given ~P(z) & Ax.R(x,y) (3) Substitution (1) (2) True Erroneous substitution, source variable whose name is bound in inner scope (0) Comment x = z (1) Given ~P(x) & Ax.R(x,y) (2) Given ~P(x) & Ax.R(z,y) (3) Substitution (1) (2) Fail: source term x includes bound variable in ['x'] False Valid substitution, replacements variable whose name is bound in inner scope (0) Comment x = z (1) Given ~P(x) & Az.R(x,z) (2) Given ~P(z) & Az.R(x,z) (3) Substitution (1) (2) True Erroneous substitution, replacement variable whose name is bound in inner scope (0) Comment x = z (1) Given ~P(x) & Az.R(x,z) (2) Given ~P(x) & Az.R(z,z) (3) Substitution (1) (2) Fail: replacement term z includes bound variable in ['z'] False Erroneous E-intro where replacement term includes bound variable (0) Comment Ey.Ex.R(x,y,z) (1) Given Ex.Ey.Ex.R(x,y,x) (2) E-Introduction (1) Fail: replacement term x includes bound variable in ['v1', 'y', 'x'] False Erroneous A-elim where source term includes bound variable (0) Comment Ax.Ey.Ex.R(x,y) (1) Given Ey.Ex.R(t,y) (2) A-Elimination (1) Fail: source term x includes bound variable in ['y', 'x'] False Valid A-elim where all occurences of bound var are replaced with same term (0) Comment x = u (1) Given t = v (2) Given ~(u = v) (3) Given Ax.(x = x) (4) Given t = t (5) A-Elimination (4) True Valid A-elim where all occurences of bound var are replaced with bound var name (0) Comment x = u (1) Given t = v (2) Given ~(u = v) (3) Given Ax.(x = x) (4) Given x = x (5) A-Elimination (4) True Erroneous A-elim where not all occurences of bound var are replaced (0) Comment x = u (1) Given t = v (2) Given ~(u = v) (3) Given Ax.(x = x) (4) Given x = t (5) A-Elimination (4) Fail: Not all occurrences substituted the same way { (x, t) } False Erroneous A-elim where different occurences of bound var are replaced differently (0) Comment y = u (1) Given t = v (2) Given ~(u = v) (3) Given Ax.(x = x) (4) Given y = t (5) A-Elimination (4) Fail: Not all occurrences substituted the same way { (x, y), (x, t) } False Valid A-elim where bound variable does not occur in body (0) Comment Ay.(x = x) (1) Given x = x (2) A-Elimination (1) True Valid A-elim where bound variable does not occur in body (0) Comment x = x (1) Given Ey.(x = x) (2) E-Introduction (1) True