WEKO3
アイテム
An Intuitionistic Set-theoretical Model of CCω
https://ipsj.ixsq.nii.ac.jp/records/161476
https://ipsj.ixsq.nii.ac.jp/records/161476983abd7e-e2a1-4e58-9575-e1551eb6c918
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-TPRO0902003.pdf (194.0 kB)
|
Copyright (c) 2016 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | Trans(1) | |||||||||
|---|---|---|---|---|---|---|---|---|---|---|
| 公開日 | 2016-05-24 | |||||||||
| タイトル | ||||||||||
| タイトル | An Intuitionistic Set-theoretical Model of CCω | |||||||||
| タイトル | ||||||||||
| 言語 | en | |||||||||
| タイトル | An Intuitionistic Set-theoretical Model of CCω | |||||||||
| 言語 | ||||||||||
| 言語 | eng | |||||||||
| キーワード | ||||||||||
| 主題Scheme | Other | |||||||||
| 主題 | [通常論文] type theory, model, intuitionistic logic | |||||||||
| 資源タイプ | ||||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||||||
| 資源タイプ | journal article | |||||||||
| 著者所属 | ||||||||||
| Graduate School of Mathematics, Nagoya University | ||||||||||
| 著者所属 | ||||||||||
| Graduate School of Mathematics, Nagoya University | ||||||||||
| 著者所属(英) | ||||||||||
| en | ||||||||||
| Graduate School of Mathematics, Nagoya University | ||||||||||
| 著者所属(英) | ||||||||||
| en | ||||||||||
| Graduate School of Mathematics, Nagoya University | ||||||||||
| 著者名 |
Masahiro, Sato
× Masahiro, Sato
× Jacques, Garrigue
|
|||||||||
| 著者名(英) |
Masahiro, Sato
× Masahiro, Sato
× Jacques, Garrigue
|
|||||||||
| 論文抄録 | ||||||||||
| 内容記述タイプ | Other | |||||||||
| 内容記述 | Werner's set-theoretical model is one of the simplest models of CCω. It combines a functional view of predicative universes with a collapsed view of the impredicative sort Prop. However this model of Prop is so coarse that the principle of excluded middle P ∨ ¬ P holds. In this paper, we interpret Prop into a topological space (a special case of Heyting algebra) to make it more intuitionistic without sacrificing simplicity. We prove soundness and show some applications of our model. ------------------------------ This is a preprint of an article intended for publication Journal of Information Processing(JIP). This preprint should not be cited. This article should be cited as: Journal of Information Processing Vol.24(2016) No.4(online) ------------------------------ |
|||||||||
| 論文抄録(英) | ||||||||||
| 内容記述タイプ | Other | |||||||||
| 内容記述 | Werner's set-theoretical model is one of the simplest models of CCω. It combines a functional view of predicative universes with a collapsed view of the impredicative sort Prop. However this model of Prop is so coarse that the principle of excluded middle P ∨ ¬ P holds. In this paper, we interpret Prop into a topological space (a special case of Heyting algebra) to make it more intuitionistic without sacrificing simplicity. We prove soundness and show some applications of our model. ------------------------------ This is a preprint of an article intended for publication Journal of Information Processing(JIP). This preprint should not be cited. This article should be cited as: Journal of Information Processing Vol.24(2016) No.4(online) ------------------------------ |
|||||||||
| 書誌レコードID | ||||||||||
| 収録物識別子タイプ | NCID | |||||||||
| 収録物識別子 | AA11464814 | |||||||||
| 書誌情報 |
情報処理学会論文誌プログラミング（PRO） 巻 9, 号 2, 発行日 2016-05-24 |
|||||||||
| ISSN | ||||||||||
| 収録物識別子タイプ | ISSN | |||||||||
| 収録物識別子 | 1882-7802 | |||||||||
| 出版者 | ||||||||||
| 言語 | ja | |||||||||
| 出版者 | 情報処理学会 | |||||||||
