Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
sav08:proofs_and_induction [2008/02/21 11:21] vkuncak |
sav08:proofs_and_induction [2008/02/21 16:49] vkuncak |
||
|---|---|---|---|
| Line 77: | Line 77: | ||
| Instead of proving a goal, you can assume its negation and prove any remaining goals (this generalizes proof by contradiction). | Instead of proving a goal, you can assume its negation and prove any remaining goals (this generalizes proof by contradiction). | ||
| \[ | \[ | ||
| - | \frac{\lnot P \vdash\} | + | \frac{\lnot P \vdash} |
| {\vdash P} | {\vdash P} | ||
| \] | \] | ||
| Line 109: | Line 109: | ||
| When you have an existentially quantified assumption, you can pick a witness for existential statement and denote it by fresh variable "x_0". Informally we would say "let $x_0$ be such $x$". | When you have an existentially quantified assumption, you can pick a witness for existential statement and denote it by fresh variable "x_0". Informally we would say "let $x_0$ be such $x$". | ||
| \[ | \[ | ||
| - | \frac{P(x_0)} | + | \frac{P(x_0) \vdash} |
| {\exists x. P(x) \vdash} | {\exists x. P(x) \vdash} | ||
| \] | \] | ||