# В точности vml2010
types
bool.
judgment
Trueprop :: bool => prop (conv 5)
symbols
implies :: [bool, bool] => bool (infixr "-->" 25)
conj :: [bool, bool] => bool (infixr "&" 35)
disj :: [bool, bool] => bool (infixr "|" 30)
Not :: bool => bool (prefix "~" 40)
schemes
A1: "A --> (B --> A)"
A2: "(A --> (B --> C)) --> ((A --> B) --> (A --> C))"
A3: "A & B --> A"
A4: "A & B --> B"
A5: "A --> (B --> A & B)"
A6: "A --> A | B"
A7: "B --> A | B"
A8: "(A --> C) --> ((B --> C) --> (A | B --> C))"
A9: "(A --> B) --> ((A --> ~ B) --> ~ A)"
A10: "~ ~ A --> A"
MP: [|"A --> B"; "A"|] ==> "B"
theorems
theorem exam2_5:
shows "P | Q --> Q | P"
proof
s1: "P --> Q | P" by A7
s2: "Q --> Q | P" by A6
s3: "(P --> Q | P) --> ((Q --> Q | P) --> (P | Q --> Q | P))" by A8
s4: "(Q --> Q | P) --> (P | Q --> Q | P)" using s3 and s1 by MP
s5: "P | Q --> Q | P" using s4 and s2 by MP
qed
theorem exam2_6:
shows "A --> A"
proof
s1: "(A --> ((A --> A) --> A)) --> ((A --> (A --> A)) --> (A --> A))" by A2
s2: "A --> ((A --> A) --> A)" by A1
s3: "(A --> (A --> A)) --> (A --> A)" using s1 and s2 by MP
s4: "A --> (A --> A)" by A1
s5: "A --> A" using s3 and s4 by MP
qed
theorem exam2_11:
assumes h1: "P & Q"
shows "Q & P"
proof
s1: "P & Q --> P" by A3
s2: "P" using s1 and h1 by MP
s3: "P & Q --> Q" by A4
s4: "Q" using s3 and h1 by MP
s5: "Q --> (P --> Q & P)" by A5
s6: "P --> Q & P" using s5 and s4 by MP
s7: "Q & P" using s6 and s2 by MP
qed
theorem for_exam2_19:
assumes h1: "A"
assumes h2: "A --> B"
assumes h3: "B --> C"
shows "C"
proof
s1: "B" using h2 and h1 by MP
s2: "C" using h3 and s1 by MP
qed
theorem for_exam2_20:
assumes not_b: "~ B"
assumes a_impl_b: "A --> B"
shows "~ A"
proof
s1: "(A --> B) --> ((A --> ~ B) --> ~ A)" by A9
s2: "(A --> ~ B) --> ~ A" using s1 and a_impl_b by MP
s3: "~ B --> (A --> ~ B)" by A1
s4: "A --> ~ B" using s3 and not_b by MP
s5: "~ A" using s2 and s4 by MP
qed
theorem exam2_21:
assumes a: "A"
assumes not_a: "~ A"
shows "B"
proof
s1: "A --> (~ B --> A)" by A1
s2: "~ A --> (~ B --> ~ A)" by A1
s3: "~ B --> A" using s1 and a by MP
s4: "~ B --> ~ A" using s2 and not_a by MP
s5: "(~ B --> A) --> ((~ B --> ~ A) --> ~ ~ B)" by A9
s6: "(~ B --> ~ A) --> ~ ~ B" using s5 and s3 by MP
s7: "~ ~ B" using s6 and s4 by MP
s8: "~ ~ B --> B" by A10
s9: "B" using s8 and s7 by MP
qed
theorem a_and_b_infers_a:
assumes h1: "A & B"
shows "A"
proof
s1: "A & B --> A" by A3
s2: "A" using s1 and h1 by MP
qed
theorem a_and_b_infers_b:
assumes h1: "A & B"
shows "B"
proof
s1: "A & B --> B" by A4
s2: "B" using s1 and h1 by MP
qed
theorem a_impl_false_infers_not_a:
assumes h1: "A --> B & ~ B"
shows "~ A"
proof
s1: "B & ~ B --> B" by A3
s2: "B & ~ B --> ~ B" by A4
s3: "(B & ~ B --> B) --> A --> (B & ~ B --> B)" by A1
s4: "(B & ~ B --> ~ B) --> A --> (B & ~ B --> ~ B)" by A1
s5: "A --> (B & ~ B --> B)" using s3 and s1 by MP
s6: "A --> (B & ~ B --> ~ B)" using s4 and s2 by MP
s7: "(A --> (B & ~ B --> B)) --> (A --> B & ~ B) --> (A --> B)" by A2
s8: "(A --> (B & ~ B --> ~ B)) --> (A --> B & ~ B) --> (A --> ~ B)" by A2
s9: "(A --> B & ~ B) --> (A --> B)" using s7 and s5 by MP
s10: "(A --> B & ~ B) --> (A --> ~ B)" using s8 and s6 by MP
s11: "A --> B" using s9 and h1 by MP
s12: "A --> ~ B" using s10 and h1 by MP
s13: "(A --> B) --> (A --> ~ B) --> ~ A" by A9
s14: "(A --> ~ B) --> ~ A" using s13 and s11 by MP
s15: "~ A" using s14 and s12 by MP
qed
theorem a_b_infers_a_and_b:
assumes a: "A"
assumes b: "B"
shows "A & B"
proof
s1: "A --> B --> A & B" by A5
s2: "B --> A & B" using s1 and a by MP
s3: "A & B" using s2 and b by MP
qed
theorem a_or_b_a_impl_c_b_impl_c_infers_c:
assumes ab: "A | B"
assumes a: "A --> C"
assumes b: "B --> C"
shows "C"
proof
s1: "(A --> C) --> (B --> C) --> (A | B --> C)" by A8
s2: "(B --> C) --> (A | B --> C)" using s1 and a by MP
s3: "A | B --> C" using s2 and b by MP
s4: "C" using s3 and ab by MP
qed
theorem a_infers_a_or_b:
assumes h1: "A"
shows "A | B"
proof
s1: "A --> A | B" by A6
s2: "A | B" using s1 and h1 by MP
qed
theorem b_infers_a_or_b:
assumes h1: "B"
shows "A | B"
proof
s1: "B --> A | B" by A7
s2: "A | B" using s1 and h1 by MP
qed
theorem mp:
assumes ab: "A --> B"
assumes a: "A"
shows "B"
proof
s1: "B" using ab and a by MP
qed
theorem a_infers_b_impl_a:
assumes h1: "A"
shows "B --> A"
proof
s1: "A --> (B --> A)" by A1
s2: "B --> A" using s1 and h1 by MP
qed
theorem not_not_a_infers_a:
assumes h1: "~ ~ A"
shows "A"
proof
s1: "~ ~ A --> A" by A10
s2: "A" using s1 and h1 by MP
qed