본문 바로가기
Topos Uranos
한국어

논리와 연역

요약

이 수업은 수학, 정보과학, 철학 중 무엇을 공부하는 사람에게나 똑같이 쓸모 있도록 LaTeX로 논리를 쓰는 법을 가르친다. 대상 언어의 연결사와 메타언어의 화살표를 구별하고, 연결사와 그 변형, 다른 전통의 표기(말굽 기호, 물결표, 점, 폴란드 표기법), 그리고 연결사마다 자기 명령을 두는 이점을 소개한다. 양화사의 간격을 정하고, 조건 제시법으로 집합을 조판하며, 키보드의 세로 막대와 \mid의 간격이 왜 다른지 설명한다. 메타논리, 시퀀트, 양상 논리의 기호를 각 기호를 정의하는 패키지와 함께 모은다. 진리표를 array로 조판한다. bussproofs로 자연 연역 나무를 만들고(그 스택의 논리가 오류를 설명해 준다), logicproof로 Fitch 상자를 만든다. 번호가 붙은 전제와 결론으로 이루어진 표준 형식으로 논증을 제시한다. 끝으로 피해야 할 것들을 각 오류의 실제 로그와 함께 다룬다.

학습 목표

  1. 식이 무엇을 주장하는지에 따라 대상 언어의 연결사와 메타언어의 화살표 가운데, 그리고 \models, \vdash, \equiv, \Leftrightarrow 가운데 알맞은 것을 고른다.
  2. 양화사, 조건 제시법의 집합, 물결표 부정의 간격을 예측하고, 아무 경고도 나오지 않는 부주의를 바로잡는다.
  3. 연결사마다 명령을 하나씩 정의하고, 그것이 어떤 전통 전환을 가능하게 하고 어떤 전환은 가능하게 하지 않는지 설명한다.
  4. 스택의 상태를 따라가며 bussproofs로 자연 연역 나무를 만들고, 로그를 보고 그 오류를 진단한다.
  5. 진리표와 표준 형식의 논증을 조판하고, 주어진 증명에 나무와 Fitch 상자 중 어느 것이 알맞은지 고른다.

언어의 두 층위

논리학의 글은 언제나 두 층위에서 말한다. 하나는 대상 언어, 곧 연구 대상인 논리식의 언어로, 고유한 연결사와 양화사를 가진다. 다른 하나는 메타언어, 곧 저자의 언어로, 그 논리식들에 대해 무언가를 주장한다. 어떤 식이 다른 식들로부터 도출된다거나, 두 식이 동치라거나, 어떤 식이 모든 모형에서 참이라는 주장이 그렇다. 표기는 두 층위를 분리해 두어야 한다. 엉뚱한 곳에 놓인 화살표는 조판상의 실수가 아니라 다른 주장이기 때문이다. 이 수업은 기호와 표기 수업의 기호와 연산자, 정리와 증명 수업의 환경을 전제로 하며, 여기서는 논리에 고유한 것을 다룬다. 이 표기들이 표현하는 이론은 수리논리학 I: 명제 논리 과정에서 배울 수 있다.