<テクニカルレポート>
A reduction rule for Peirce's formula makes all the terms with the same type equal

作成者
本文言語
出版者
発行日
雑誌名
出版タイプ
アクセス権
概要 A reduction rule is introduced by $ x^ alpha \to \beta left(P^((alpha \to \beta)\to alpha) \to alpha y ^ (alpha \to \beta) \to alpha \right) stackrel{P}{\to} x(yx) $ as a transformation of proof figur...es in implicational classical logic. The proof figure are represented as typed $ lamda-terms $ with a new constant $ P^ left(( alpha \to \beta) \to alpha) \to alpha $. It is shown that all the terms with the same type are equivalent with respect to the $ \beta-reduction $ and this reduction. Hence all the proof of the same implicational formula are equivalent.続きを見る

本文情報を非表示

rifis-tr-91 pdf 216 KB 52  

詳細

レコードID
査読有無
関連情報
タイプ
登録日 2009.04.22
更新日 2017.01.20