日々の流転

λ. 近代思想

今日は、「人間主義」について。行動の究極的目的を(神・善・正義でも、快楽・金銭・権力でもなく)人間に置くってのがやっぱりポイントだろう。

「天動説 → 地動説」と「神中心主義または宇宙中心主義 → 人間中心主義」を対置して「ルネッサンスの逆説」と呼ぶのは筋違いに感じられる。

λ. LK

「(A → B) → ((A → ¬B) → ¬A)」の証明なんかに苦戦。かなりダメげ。でも、シーケント計算とか推論規則とかって面白いなぁ。

[2005-05-30 追記] 一応書いておこう(exchangeは省略)。ちなみにLJで十分。それにしても、「→左」規則は直観的でないと思う。

                     B |- B
                   ------------ (¬左)
          A |- A     B, ¬B |-
         ---------------------- (→左)
A |- A      B, A→¬B, A |-
------------------------------------ (→左)
A→B, A→¬B, A, A |-
----------------------- (contraction左)
A→B, A→¬B, A |-
----------------------- (¬右)
A→B, A→¬B |- ¬A
------------------------ (→右)
A→B |- (A→¬B)→¬A
-------------------------- (→右)
|- (A→B)→(A→¬B)→¬A

ちなみに、Agdaだと簡単だし直観的。

--#include "Hedberg/SET.alfa"
open SET use Imply, Not
 
z (|A,B::Set) :: (A `Imply` B) `Imply` ((A `Imply` Not B) `Imply` Not A)
z = \(x::A `Imply` B)-> 
     \(y::A `Imply` Not B)-> 
      \(a::A)-> 
       case y a (x a) of { }

λ. 読んだ本

• 「BASTARD 第22巻」　萩原一至
• 「遊戯王 第24巻」　高橋和希
• 「ノルマンディーひみつクラブ　第4巻」　たかはしみきお