Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav07_lecture_5 [2007/04/03 17:37] vaibhav.rajan |
sav07_lecture_5 [2007/04/03 17:40] vaibhav.rajan |
||
|---|---|---|---|
| Line 143: | Line 143: | ||
| * Basic idea, and in the above example (name i from the ∃i as i0, then instantiate ∀i also with i=i0) | * Basic idea, and in the above example (name i from the ∃i as i0, then instantiate ∀i also with i=i0) | ||
| - | * examples of incompleteness: | + | * example: |
| Given: f(0) > 0 & ∀x:x > 0. (f(x)>0) --> f(x+1)>0 | Given: f(0) > 0 & ∀x:x > 0. (f(x)>0) --> f(x+1)>0 | ||
| + | |||
| Prove: ∀x. (x >= 0) --> f(x+1)>0 | Prove: ∀x. (x >= 0) --> f(x+1)>0 | ||
| + | |||
| Proof: | Proof: | ||
| - | * f(5) > 0 | + | * f(5) > 0\\ |
| f(5): can be derived by deriving f(1), f(2), f(3) and f(4). | f(5): can be derived by deriving f(1), f(2), f(3) and f(4). | ||
| * Then its straightforward to use ∀x:x > 0. (f(x)>0) --> f(x+1)>0 and arrive at the proof. | * Then its straightforward to use ∀x:x > 0. (f(x)>0) --> f(x+1)>0 and arrive at the proof. | ||
| For formulas with quantifiers, example: (∀x.F1) & F2, substitute values for x in F1. | For formulas with quantifiers, example: (∀x.F1) & F2, substitute values for x in F1. | ||
| + | |||
| A heuristic that could be used is: Look at constants in F2 and try substituting them. | A heuristic that could be used is: Look at constants in F2 and try substituting them. | ||