最小元 ∃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の約数である（bはaの倍数である）ことを表す（広く合意された）記号がない。 縦棒 | を使うことがあるが、使い勝手が悪い！ Unicode一覧を見ると、⊑（U+2291） と ⊒（U+2292） がある。 これを使おう。 定義： aはbの約数である ⇔ a⊑b…

参考： 引き算と無限個の足し算は両立しない - 檜山正幸のキマイラ飼育記 モノイドや半環は、群や環とはかけ離れている - 檜山正幸のキマイラ飼育記 定義 集合Lの定義 L := {(x, y)∈N2 | x≦y } (x, y)∈L ⇔ ∃z.(x + z = y) 関数subtの定義 function subt := λ…

x ≦ x 準備 Γ |-? ∀x∈N.(x ≦ x) ---------------------------------- Γ |-? ∀x∈N.∃z∈N.( x + z = x) ---------------------------------- Γ, x∈N |-? ∃z∈N.( x + z = x)証明 証明要求： Γ, x∈N |-? ∃z∈N.(x + z = x) x + 0 = x ---(1) -----------------[●∃…