圏論による論理学P22

 λ-h.o.lのA.4がややこしかった。　厳密ではないかもしれないが以下のように考えてみた。

A.4　（Att　Tt　∧　Att　Ft）＝　∀　ｘt　Att　ｘt

　　　　　①　　　　　②

前提として　∀の定義が

　∀ｘ At＝（λｘ　At　＝　λｘ　T）　なので

　　∀ｘ　Ａｔは、ＴかＦ

　　Ｔの場合は　定義より　λｘ　Ａｔが　どんなｘでも→Ｔ
　　Ｆの場合は　λｘ　At　と　λｘ　T　が違うことがあるということなので

　　　　　　　　λｘ　Atが　どんなｘでも→Ｆ　の場合と　

　　　　　　　　　　　　　　ｘにより→Ｆだったり→Ｔだったり　の場合がある

これを　もとに　Ａ．４を考えると

　　∀　ｘt　Att　ｘt　は　ＴかＦ

　　　　Ｔの場合は　　xt→Att　xt　が　T→T＝AttTt　①　F→T＝AttF　②

　　　　Fの場合は　　T→F　①　F→F　②　のときと

　　　　　　　　　　T→T　①　F→F　②　のときと

　　　　　　　　　　T→F　①　F→T　②　の３とおり考えられる

　　　いずれの場合も　A.４を満たす

　　　※　　A.４は　　両辺とも　Attの関数とみてもいいのでないかと、、、

　　　　　　　　ｆ：Ａtt→TまたはF　　つまりｆ（Att）＝T　か　Fになるという

　　　　　　イメージか。