大小関係、最小限と足し算との協調性

最小元

• ∃a.∀x.a≦x

準備

• Γ |-? ∃a.∀x.∃z.(a + z = x)

証明

証明要求： Γ |-? ∃a.∀x.a≦x

BEGIN ∀-BOX
  var u

  0 + u = u
   --[●∃導入 t:←左辺のu]
  ∃t.0 + t = u
  0 ≦ u
   --[●∀導入 x:←u]
  ∀x.(0 ≦ x)
END
∀x.(0 ≦ x)
 --[●∃導入 a:←0]
∃a.∀x.(a ≦ x)

最大元

ない。

足し算と協調

• a≦b, c≦d ⇒ a + c ≦ b + d

準備

 Γ |-? ∀a, b, c, d.(a≦b ∧ c≦d ⇒ a + c ≦ b + d)
 --------------------------------------------------------
 Γ, (a, b, c, d∈<b>N</b>) |-? a≦b ∧ c≦d ⇒ a + c ≦ b + d
 --------------------------------------------------------
 Γ, (a, b, c, d∈<b>N</b>), (a≦b ∧ c≦d) |-? a + c ≦ b + d
 --------------------------------------------------------
 Γ, (a, b, c, d∈<b>N</b>), a≦b, c≦d |-? a + c ≦ b + d
 --------------------------------------------------------
 Γ, (a, b, c, d∈<b>N</b>), ∃z.(a + z = b), ∃z.(c + z = d) |-?
    ∃z.(a + c + z = b + d)

証明

証明要求： Γ, (a, b, c, d∈<b>N</b>), ∃z.(a + z = b), ∃z.(c + z = d) |-?
    ∃z.((a + c) + z = b + d)

●∃z.(a + z = b)
BEGIN ∃-BOX
  var x
  a + x = b

  ●∃z.(c + z = d)
  BEGIN ∃-BOX
    var y
    c + y = d

    (a + x) + (c + y) = b + d
    (a + c) + (x + y) = b + d
      --[●∃導入 z:← x + y]
    ∃z.((a + c) + z = b + d)
  END
  ∃z.((a + c) + z = b + d)
END
∃z.((a + c) + z = b + d)