著者
矢田部 俊介
出版者
京都大学文学部科学哲学科学史研究室
雑誌
科学哲学科学史研究 (ISSN:18839177)
巻号頁・発行日
vol.7, pp.1-26, 2013-02-28

Recently some constructivists try to justify impredicative theories with coinduction which play a very significant role in computer science though it had been thought that predicativity is necessary for constructivity. In this paper we introduce these arguments, by Rathjen and by Coquand, and apply these argument to show a naive set theory CONS in FLew∀, which is intuitionistic logic minus the contraction rule, can be regarded as constructive.
著者
矢田部 俊介
出版者
京都大学文学部科学哲学科学史研究室
雑誌
科学哲学科学史研究 (ISSN:18839177)
巻号頁・発行日
vol.9, pp.1-32, 2015-03-31

Truth theories like the Friedman-Sheard's truth theory (FS) have two rules, T-in rule and T-out rule, about introduction and elimination of the truth predicate. They look like the introduction rule and the elimination rule of a logical connective. From the proof theoretic semantics viewpoint, one might think that the truth predicate is a logical connective which is governed by these two rules. From this proof theoretic semantics viewpoint, the nature of truth is like deflationist's nature of truth. Additionally one of the most important things is that the truth predicate does not disturb the traceability of the argument from the premises to a conclusion. However, a crucial problem has been known: any criteria to be a logical connective, known as a "harmony" of the introduction rule and the elimination rule, are not satisfied because of the ω-inconsistency of FS. Such ω-inconsistency is caused by the fact that the truth predicate enables us to define paradoxical formulae of seemingly infinite-length. These formulae can be regarded as coinductive objects in terms of computer science. The reason of the failure of the harmony is that these criteria are defined not for coinductively defined paradoxical formulae but for inductively defined formulae. In this paper, we examine how we can extend the criteria for harmony for coinductive formulae.
著者
矢田部 俊介
出版者
京都大学文学部科学哲学科学史研究室
雑誌
科学哲学科学史研究 (ISSN:18839177)
巻号頁・発行日
vol.6, pp.1-15, 2012-02-28

In his 2003 paper, Peacocke insisted that our implicit conception of natural numbers essentially uses a primitive recursion which consists of three clauses, and claimed that this excludes the non-standard models of natural numbers. In this article, we construct a counter “model” to his argument, which contains a non-standard natural number though the set ω of natural numbers is defined as an analogy to his primitive recursion, in a set theory with the comprehension principle within many-valued logic. This result suggests that we should interpret non-standard natural numbers from a philosophical viewpoint. We discuss this by reviewing Strict Finitism, and we conclude that non-standard natural numbers can be interpreted as “large numbers” in a Strict Finitist sense: It expresses new numbers which are introduced by expanding the notation system of natural numbers.
著者
森 崇 矢田部 俊介
雑誌
情報処理
巻号頁・発行日
vol.57, no.7, pp.638-643, 2016-06-15

近年,無線を用い列車の位置と速度をリアルタイムで把握し,システムで連続的制御を行う方式が採用されるようになった.しかし無線の使用は,セキュリティの問題を生む.従来の安全性の対象を拡大し,人為的攻撃に対する高いセキュリティ性も検討対象として含める必要がある.そのため,JR西日本では,国際規格IEC62278(RAMS)の考え方にもとづき,システムの安全性や安定性をライフサイクル全般にわたって管理すると共に,その枠内でセキュリティ性も専門家の知見を活用しつつ検討する「システム評価委員会」を立ち上げ,検討を続けてきた.小論では,委員会で行われた脅威分析の手法について紹介する.