なんとなく面白そうだけど、身近で使ってる人もいないし、何が便利なのかよくわからないコマンドだったgnu screen Webで断片的な情報を齧るだけだと、 Detachが便利？ 何それ？sshが切れても大丈夫？ 画面の分割が楽しい？ という二つの楽しみかたがあるよう…

パースの法則からcoqで排中律を導く。 Theorem Peirce : forall A B : Prop, ((A -> B) -> A) -> A. Admitted. Theorem classic : forall p : Prop, ~~p -> p. Proof. unfold not. intros. apply (Peirce p False). intro. exfalso. apply H. apply H0. Qed.…

ツェルメロの集合論が小さすぎる(弱すぎる)ということの説明で、いきなり、R(ω+ω)に属する元だけを集合として考えるとツェルメロの集合論の公理はすべて満たされてしまう。とか書いてあってよく分からん。ωは自然数全体の集り R(α)は、順序数αを作るときに作…

音楽と数学の類似について。どっちでも劣等生であったけれども。 とくに数学はまったく分からなかった。ピアノは少し難しくなるとさっぱり弾けなかった。仕事でプログラムをやって、数学との類似性に気がついた。というか、実は同じものだった。 証明はプロ…

竹内外史の「集合とは何か」を読んでる。ずーとほったらかしてあった。 よく読むとすごくいい本かもしれん。いつ何で買ったかも思いだせないが。素朴集合論で、やたらめったら大きい集合について考えると矛盾が出てどうしようもなくなったので、なんとか回避…

述語論理における解釈のことを構造(structure)と呼ぶことがある。 論理式Aは任意の構造Iと任意の付値Jの元で、 となるとき、恒真であるという。 ある構造Iとある付値Jのもとで真になるとき、Aは充足可能(satisfiable)という。 ∃I,J.A = T ¬∀I,J.¬A = T 論理…

だんだん面倒くさくなってきた。 述語論理における解釈(interpretation)、すなわち述語記号と定数記号を含む関数記号の解釈のことを構造(structure)と呼ぶことがある。 述語論理における構造は、領域と呼ばれる空でない集合、定数記号を含む関数記号の解釈、…

このへんのことはラムダ式そのまんまだな。 変数捕獲って、OnLispで初めて見たけど、そういうことにすら数学的な背景があるとは。

∃xA ≡ ¬∀x¬A ∀xA ≡ ¬∃x¬Aドモルガンと似てるつーか、同じ。 A∨B ≡ ¬((¬A)∧(¬B)) A∧B ≡ ¬((¬A)∨(¬B))xが属する集合をXとして、その要素をx1,x2...xnとし、 Aを表す関数記号をfとすると、 ∀xAつうのは、 f(x1) ∧ f(x2) ∧ f(x3) ...∧ f(xn)これにドモルガンを適…

述語記号と項から作られる式を原子論理式(atomic formula)という。 Q(f(x,c), g(f(c, d))) は原子論理式である。 述語論理式(predicate formula)は、原子論理式と論理記号から作られる式である。 命題論理の論理記号である¬,∧,∨,→,⇔などはそのまま使える。 ∀…

論理と計算のしくみを読んでる。 述語(predicate)とは、不特定な対象に関する条件のことである。 P(x)のPを述語記号(predicate symbol)という 述語記号の引数の数をアリティ(arity)という。 Q(10,20)のアリティは2 arityの数が0の述語記号は命題論理の命題に…

正直半可通が言及するとすぐ炎上して火だるまになりそうな話題だけど。鯨については、http://www.kkneko.com/aa1.htm という文章を以前Webで見た。江戸期以前大して鯨を取ってなかった日本に対して、鯨油目的で乱獲を繰り返してきた欧米。そんな欧米がいまさ…

変数/関数定義 Definition 名前 (:型) := 定義. (* 最後ピリオド *) Definition three : nat := 3. Definition three' := 3. := で定義。 型は省略出来る。(型推論が効く場合) 引数のない関数か、単なる定数の区別が私には出来ません。どっかで出来るの？ De…