summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Isar_Examples/Peirce.thy

author | wenzelm |

Tue Sep 26 20:54:40 2017 +0200 (23 months ago) | |

changeset 66695 | 91500c024c7f |

parent 63585 | f4a308fdf664 |

permissions | -rw-r--r-- |

tuned;

1 (* Title: HOL/Isar_Examples/Peirce.thy

2 Author: Makarius

3 *)

5 section \<open>Peirce's Law\<close>

7 theory Peirce

8 imports Main

9 begin

11 text \<open>

12 We consider Peirce's Law: \<open>((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A\<close>. This is an inherently

13 non-intuitionistic statement, so its proof will certainly involve some form

14 of classical contradiction.

16 The first proof is again a well-balanced combination of plain backward and

17 forward reasoning. The actual classical step is where the negated goal may

18 be introduced as additional assumption. This eventually leads to a

19 contradiction.\<^footnote>\<open>The rule involved there is negation elimination; it holds in

20 intuitionistic logic as well.\<close>\<close>

22 theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"

23 proof

24 assume "(A \<longrightarrow> B) \<longrightarrow> A"

25 show A

26 proof (rule classical)

27 assume "\<not> A"

28 have "A \<longrightarrow> B"

29 proof

30 assume A

31 with \<open>\<not> A\<close> show B by contradiction

32 qed

33 with \<open>(A \<longrightarrow> B) \<longrightarrow> A\<close> show A ..

34 qed

35 qed

37 text \<open>

38 In the subsequent version the reasoning is rearranged by means of ``weak

39 assumptions'' (as introduced by \<^theory_text>\<open>presume\<close>). Before assuming the negated

40 goal \<open>\<not> A\<close>, its intended consequence \<open>A \<longrightarrow> B\<close> is put into place in order to

41 solve the main problem. Nevertheless, we do not get anything for free, but

42 have to establish \<open>A \<longrightarrow> B\<close> later on. The overall effect is that of a logical

43 \<^emph>\<open>cut\<close>.

45 Technically speaking, whenever some goal is solved by \<^theory_text>\<open>show\<close> in the context

46 of weak assumptions then the latter give rise to new subgoals, which may be

47 established separately. In contrast, strong assumptions (as introduced by

48 \<^theory_text>\<open>assume\<close>) are solved immediately.

49 \<close>

51 theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"

52 proof

53 assume "(A \<longrightarrow> B) \<longrightarrow> A"

54 show A

55 proof (rule classical)

56 presume "A \<longrightarrow> B"

57 with \<open>(A \<longrightarrow> B) \<longrightarrow> A\<close> show A ..

58 next

59 assume "\<not> A"

60 show "A \<longrightarrow> B"

61 proof

62 assume A

63 with \<open>\<not> A\<close> show B by contradiction

64 qed

65 qed

66 qed

68 text \<open>

69 Note that the goals stemming from weak assumptions may be even left until

70 qed time, where they get eventually solved ``by assumption'' as well. In

71 that case there is really no fundamental difference between the two kinds of

72 assumptions, apart from the order of reducing the individual parts of the

73 proof configuration.

75 Nevertheless, the ``strong'' mode of plain assumptions is quite important in

76 practice to achieve robustness of proof text interpretation. By forcing both

77 the conclusion \<^emph>\<open>and\<close> the assumptions to unify with the pending goal to be

78 solved, goal selection becomes quite deterministic. For example,

79 decomposition with rules of the ``case-analysis'' type usually gives rise to

80 several goals that only differ in there local contexts. With strong

81 assumptions these may be still solved in any order in a predictable way,

82 while weak ones would quickly lead to great confusion, eventually demanding

83 even some backtracking.

84 \<close>

86 end