Fix formatting in Socrates example and illustrate a problem.
Chris Pressey
8 years ago
277 | 277 | Let = exists(X, P) ; V{unique local atom} |- P[X -> V] |
278 | 278 | end |
279 | 279 | |
280 | Premise_1 = |- forall(x, impl(man(x), mortal(x))) | |
281 | Premise_2 = |- exists(x, and(man(x), socrates(x))) | |
280 | Premise_1 = |- forall(x, impl(man(x), mortal(x))) | |
281 | Premise_2 = |- exists(x, and(man(x), socrates(x))) | |
282 | 282 | show |
283 | 283 | exists(x, and(mortal(x), socrates(x))) |
284 | 284 | proof |
285 | 285 | Step_1 = forall(x, impl(man(x), mortal(x))) by Premise_1 |
286 | 286 | Step_2 = exists(x, and(man(x), socrates(x))) by Premise_2 |
287 | 287 | block Existential_Instantiation |
288 | Step_4 = and(man(k), socrates(k)) by Let with Step_2, k | |
289 | Step_5 = man(k) by Simplification_Left with Step_4 | |
290 | Step_6 = impl(man(k), mortal(k)) by Universal_Instantiation with Step_1, k | |
291 | Step_7 = mortal(k) by Modus_Ponens with Step_6, Step_5 | |
292 | Step_8 = socrates(k) by Simplification_Right with Step_4 | |
293 | Step_9 = and(mortal(k), socrates(k)) by Conjunction with Step_7, Step_8 | |
294 | Step_10 = exists(x, and(mortal(x), socrates(x))) by Existential_Generalization with Step_9, k, x | |
295 | end | |
296 | Step_11 = exists(x, and(mortal(x), socrates(x))) by Tautology with Step_10 | |
288 | Step_3 = and(man(k), socrates(k)) by Let with Step_2, k | |
289 | Step_4 = man(k) by Simplification_Left with Step_3 | |
290 | Step_5 = impl(man(k), mortal(k)) by Universal_Instantiation with Step_1, k | |
291 | Step_6 = mortal(k) by Modus_Ponens with Step_5, Step_4 | |
292 | Step_7 = socrates(k) by Simplification_Right with Step_3 | |
293 | Step_8 = and(mortal(k), socrates(k)) by Conjunction with Step_6, Step_7 | |
294 | Step_9 = exists(x, and(mortal(x), socrates(x))) by Existential_Generalization with Step_8, k, x | |
295 | end | |
296 | Step_10 = exists(x, and(mortal(x), socrates(x))) by Tautology with Step_9 | |
297 | 297 | qed |
298 | 298 | ===> ok |
299 | 299 | |
306 | 306 | block EI |
307 | 307 | Let = exists(X, P) ; V{unique local atom} |- P[X -> V] |
308 | 308 | end |
309 | ||
310 | ### A problem ### | |
311 | ||
312 | There still seems to be something missing, because I can "prove" that all men are Socrates: | |
313 | ||
314 | given | |
315 | Simplification_Right = and(P, Q) |- Q | |
316 | Tautology = P |- P | |
317 | ||
318 | UG = P ; X{term} ; V{atom} |- forall(V, P[X -> V]) | |
319 | UI = forall(X, P) ; V{term} |- P[X -> V] | |
320 | EG = P ; X{term} ; V{atom} |- exists(V, P[X -> V]) | |
321 | block EI | |
322 | Let = exists(X, P) ; V{unique local atom} |- P[X -> V] | |
323 | end | |
324 | ||
325 | Premise = |- exists(x, and(man(x), socrates(x))) | |
326 | show | |
327 | forall(x, socrates(x)) | |
328 | proof | |
329 | Step_1 = exists(x, and(man(x), socrates(x))) by Premise | |
330 | block EI | |
331 | Step_2 = and(man(k), socrates(k)) by Let with Step_1, k | |
332 | Step_3 = socrates(k) by Simplification_Right with Step_2 | |
333 | Step_4 = forall(x, socrates(x)) by UG with Step_3, k, x | |
334 | end | |
335 | Step_5 = forall(x, socrates(x)) by Tautology with Step_4 | |
336 | qed | |
337 | ===> ok | |
338 | ||
339 | The problem is that you should only be able to lift *arbitrary* (that is, *non* local) | |
340 | variables into a forall. So we'll need something like `X{nonlocal}` in the UI. | |
309 | 341 | |
310 | 342 | Equational Reasoning |
311 | 343 | -------------------- |