A Construction of the Reals from an Intuitive and Formal Perspective

Abstract

Based on intuitive facts about a straight line, we define what a straight line is with the help of R. Dedekind. And we introduce a proof assistant program Coq. After that, adding two operations - addition and multiplication to the reals, we show that the reals is a Dedekind-complete ordered field by complementing natural language and Coq.

이 논문에서는 리하르트 데데킨트의 업적을 바탕으로 직선에 대한 직관적인 사실에 근거하여 직선이 무엇인지 정의한다. 그리고 증명보조기의 한 예인 Coq를 소개한다. 더불어 직선과 대응하는 대수적 구조인 실수에 두 연산, 덧셈과 곰셈을 정의한다. 마지막으로 이렇게 정의한 실수 구조가 완비순서체임을 Coq를 이용해서 보인다.