doc-src/ZF/FOL.tex
 changeset 8249 3fc32155372c parent 6121 5fe77b9b5185 child 9695 ec7d7f877712
equal inserted replaced
8248:d7e85fd09291 8249:3fc32155372c
   576 {\out Level 4}
   576 {\out Level 4}
   577 {\out EX y. ALL x. P(y) --> P(x)}
   577 {\out EX y. ALL x. P(y) --> P(x)}
   578 {\out  1. !!x. [| P(?a); ~ (ALL xa. P(?y3(x)) --> P(xa)) |] ==> P(x)}
   578 {\out  1. !!x. [| P(?a); ~ (ALL xa. P(?y3(x)) --> P(xa)) |] ==> P(x)}
   579 \end{ttbox}
   579 \end{ttbox}
   580 In classical logic, a negated assumption is equivalent to a conclusion.  To
   580 In classical logic, a negated assumption is equivalent to a conclusion.  To
   581 get this effect, we create a swapped version of~$(\forall I)$ and apply it
   581 get this effect, we create a swapped version of $(\forall I)$ and apply it
   582 using \ttindex{eresolve_tac}; we could equivalently have applied~$(\forall  582 using \ttindex{eresolve_tac}; we could equivalently have applied$(\forall
   583 I)$using \ttindex{swap_res_tac}.  583 I)$ using \ttindex{swap_res_tac}.
   584 \begin{ttbox}
   584 \begin{ttbox}
   585 allI RSN (2,swap);
   585 allI RSN (2,swap);
   586 {\out val it = "[| ~ (ALL x. ?P1(x)); !!x. ~ ?Q ==> ?P1(x) |] ==> ?Q" : thm}
   586 {\out val it = "[| ~(ALL x. ?P1(x)); !!x. ~ ?Q ==> ?P1(x) |] ==> ?Q" : thm}
   587 by (eresolve_tac [it] 1);
   587 by (eresolve_tac [it] 1);
   588 {\out Level 5}
   588 {\out Level 5}
   589 {\out EX y. ALL x. P(y) --> P(x)}
   589 {\out EX y. ALL x. P(y) --> P(x)}
   590 {\out  1. !!x xa. [| P(?a); ~ P(x) |] ==> P(?y3(x)) --> P(xa)}
   590 {\out  1. !!x xa. [| P(?a); ~ P(x) |] ==> P(?y3(x)) --> P(xa)}
   591 \end{ttbox}
   591 \end{ttbox}