1) 국제학회 발표 a) "Subsystems of arithmetic as type theories with inductive definitions", Workshop on Computability Theory and Foundations of Mathematics, February 2013, Japan b) "Constructive formulations of the big 5 subsystems of second-prder arithmetic", Workshop on Proof Theory and Rewriting,
1) 국제학회 발표 a) "Subsystems of arithmetic as type theories with inductive definitions", Workshop on Computability Theory and Foundations of Mathematics, February 2013, Japan b) "Constructive formulations of the big 5 subsystems of second-prder arithmetic", Workshop on Proof Theory and Rewriting, March 2013, Japan c) "The big five subsystems of reverse mathematics and their computational interpretation", CORCON 2014, March 2014, Italy 2) 논문 a) "Friedman-Weiermann style independence results beyond Peano Arithmetic", Journal of Korean Mathematical Society, 51(2014), No2, pp. 383-402 b) "Uniform Characterization of the Big Five Systems in Reverse Mathematics", in preparation.
Abstract▼
I. Title: Reverse Mathematics in Coq II. Goals of the project Since its introduction by H. Friedman in 1975, the research program of reverse mathematics has been extremely productive. However, the framework remained that of the pure force axiomatic mathematical theorems. In particular, no diff
I. Title: Reverse Mathematics in Coq II. Goals of the project Since its introduction by H. Friedman in 1975, the research program of reverse mathematics has been extremely productive. However, the framework remained that of the pure force axiomatic mathematical theorems. In particular, no difference is made between logical reasoning and without contradiction, which does not see clearly the meaning of the axioms key computational highlighted by this research. This is the first objective of our collaboration as to reformulate the foundations of mathematics down in a sufficiently fine, that of a polarized type theory, to observe phenomena and computational properties that the classical thin does not foresee. Mathematics are also largely down to the language remained ad hoc pure natural numbers when it is obvious that any mathematical application a little bit of concrete required to incorporate ideas of suites, dies, tuples , trees, all kinds of objects that mathematics traditionally bring down the entire coding via (called Gödel) that although the standard can not be used in practice. This is our second goal to reformulate the key languages of mathematics down in a usable in practice, based on the concepts of the theory of types (inductive types, dependent products) so that Coq can serve actual reference to the formalization of all types of mathematics within the scope of mathematics down. We will then be able to provide a concrete framework and effective at any logician or mathematician interested in formalizing the results of machine-specific systems of mathematics in reverse, starting with ourselves. III. Contents and Plan Our goal is to analyze the first three languages of mathematics to achieve three objectives: A. Reformulation of X as type theory and characterization of X as a subsystem of logic as a basis for Coq B. Changing the implementation of Coq that the logical force of Coq can be accurately restricted to the level of language X C. Formalization in Coq of the key findings of mathematics down on the language X IV. Results a) Theoretic aspect: RCA0, WKL0, ACA0 are reformulated as a type theory. b) Implementation: A proof assistants are being implemented. Ⅴ. Future Plan After finishing the implementation of a proof assistant, we will start to formalize important mathematical results based on Stephen Simpson' book “Subsystems of Second Order Arithmetic".
목차 Contents
표지 ... 2
제출문 ... 3
보고서 요약서 ... 4
요약문 ... 6
SUMMARY ... 8
CONTENTS ... 10
목차 ... 11
제1장 연구개발과제의 개요(연구개발의 목적, 필요성 및 범위 등을 기술) ... 12
제2장 국내외 기술개발 현황(국내·외 관련분야에 대한 기술개발현황과 연구결과가 국내·외 기술개발현황에서 차지하는 위치 등을 기술) ... 12
제3장 연구개발수행 내용 및 결과(이론적, 실험적 접근방법, 연구내용, 연구결과를 기술) ... 13
제4장 목표달성도 및 관련분야에의 기여도(연도별 연구목표 및 평가착안점에 입각한 연구개발목표의 달성도 및 관련분야의 기술발전에의 기여도 등을 기술) ... 15
※ AI-Helper는 부적절한 답변을 할 수 있습니다.