이 책이 채택한 해법은 컴퓨터 형식증명 시스템이다. 즉 학생이 작성한 증명에 오류가 있는지를 컴퓨터가 판별해 줌으로써, 학생들이 엄격한 수학적 증명에 대한 훈련을 받도록 하는 것이다. 필자는 2009년 봄부터 컴퓨터 논리 시스템 Proofmood의 개발을 시작하여 중학교 영재 학생들 및 학부 학생들을 대상으로 논리 교육에 활용해 왔다. 초기에는 주로 명제논리를 이용한 논리퍼즐 문제를 다루어 많은 학생들의 흥미를 끌수 있었다.
Contents
머리말 iii
제 1 장 명제와 논리식 1
1 논리식의 구문
2 논리식의 의미
3 논리적 귀결과 모델
4 정규형식
5 변수를 포함한 명제, 벤 다이어그램
제 2 장 논리도해 29
1 추론의 타당성
2 논리도해
3 논리도해 소프트웨어
4 터뜨리기와 추론
제 3 장 Fitch 증명시스템 53
1 피치 시스템 소개
2 피치 증명의 구조
3 피치 추론규칙
4 증명 작성 기법
제 4 장 1계논리 77
1 왜 1계논리인가?
2 1계논리식의 구문과 의미
2.1 구문론
2.2 피치 시스템의 구문
2.3 의미론
2.4 한정사의 영향범위와 치환
3 피치 1계논리 추론규칙
3.1 명제논리적 귀결
3.2 한정사의 도입과 소거
3.3 등호의 도입과 소거
3.4 추론규칙의 확충
제 5 장 1계논리 증명 작성 기법 125
1 군론
1.1 군의 공리계와 기본 정리
1.2 방정식 a · x = b는 유일한 해를 가진다
1.3 a · x = a · y ⇒ x= y(왼쪽 소거)
1.4 1면-공리계
2 페아노 산술
2.1 페아노 산술의 정의와 공리계
2.2 페아노 산술의 정리
2.3 1계논리 형식 증명의 공식과 기법
제 6 장 집합론 151
1 집합과 증명과 역설
1.1 기본 개념과 용어
1.2 형식증명과 비형식증명
1.3 집합의 기본 성질
1.4 기수, 역설, 집합의 존재성 공리
2 관계와 함수
2.1 카티지언곱
2.2 관계
2.3 함수
제 7 장 수학의 기반과 공리적 집합론 205
1 순서집합
2 동등관계와 상구조와 준동형사상
3 부분구조체와 카티지언곱 구조체
4 토픽 몇 가지
4.1 페포연산
4.2 수학적 귀납법과 문자열의 복잡도
4.3 정수론
5 기수와 서수
5.1 기수와 서수의 정의
5.2 귀납적 증명과 재귀적 정의
5.3 조른의 보조정리
5.4 서수와 기수의 연산
5.5 무한과 유한, 미루었던 증명
6 공리적 집합론