Current location - Training Enrollment Network - Mathematics courses - Predicate mathematization
Predicate mathematization
Proof: x(F(x)∧? Y(G(y)→H(x, y)) is equivalent to? x? y(F(x)∧(G(y)→H(x,y)))

1, the sufficiency of a priori proof:? x(F(x)∧? y(G(y)→H(x,y)))→? x? y(F(x)∧(G(y)→H(x,y)))

( 1)? x(F(x)∧? y(G(y)→H(x,y))) P

(2)P F(α)∧? y(G(y)→H(α,y))? -( 1)

(3)P? y(G(y)→H(α,y)) T(2)

(4)P G(y)→H(α,y)? -(3)

(5)P F(α) T(2)

(6)P F(α)∧(G(y)→H(α,y) ) T(4)(5)

(7)P? y(F(α)∧(G(y)→H(α,y)))? +(6)

(8)P? x? y(F(x)∧(G(y)→H(x,y)))? +(7)

(9){} ? x(F(x)∧? y(G(y)→H(x,y)))→? x? y(F(x)∧(G(y)→H(x,y))) D( 1)(8)

2. The necessity of recertification: x? y(F(x)∧(G(y)→H(x,y)))→? x(F(x)∧? y(G(y)→H(x,y)))

( 1)P? x? y(F(x)∧(G(y)→H(x,y))) P

(2)P? y(F(α)∧(G(y)→H(α,y)))? -( 1)

(3)P F(α)∧(G(y)→H(α,y))? -(2)

(4)P G(y)→H(α,y) T(2)

(5)P? y(G(y)→H(α,y))? +(4)

(6)P F(α) T(2)

(7)P F(α)∧? y(G(y)→H(α,y)) T(5)(6)

(8)P? x? y(F(x)∧(G(y)→H(x,y)))? +(7)

(9){} ? x? y(F(x)∧(G(y)→H(x,y)))→? x(F(x)∧? y(G(y)→H(x,y))D( 1)(8)

So it can be proved that they are equivalent.