본문 바로가기
Topos Uranos

수리논리학 I: 학습 계획

요약

이 수업은 강좌의 첫 단원을 이루며 강좌의 학습 계획 전체를 제시한다. 강좌의 목적, 대상, 강좌가 이미 안다고 가정하는 얼마 안 되는 지식, 그리고 강좌가 이어지는 강좌들을 밝히고, 강좌가 세우는 일곱 가지 전체 학습 목표를 진술하고, 강좌가 연구하는 체계에 형태를 부여하는 세 가지 결정을 설명하고, 여섯 단원과 그것을 이루는 수업들을 기술하고, 강좌가 요구하는 총 학습량, 단원별 배분, 권장 학습 속도, 호환 학점으로의 환산을 추정하며, 끝으로 수업들이 어떻게 구성되어 있는지 설명하고 강좌를 공부하는 방법에 대해 조언한다.

학습 목표

  1. 강좌의 단원 순서를 기술하고, 각 단원이 뒤따르는 단원들에 무엇을 제공하는지 설명한다.
  2. 강좌의 전체 학습 목표를 진술하고, 각 목표에 어느 단원이 기여하는지 알아본다.
  3. 강좌의 체계를 정하는 결정들, 곧 원과 원판의 언어, 두 번째 기본 규칙, 콤팩트성과 강한 완전성의 순서를 설명한다.
  4. 단원별 추정 시간으로부터 강좌 전체나 그 일부가 요구하는 학습량을 계산하고, 그것으로 개인 학습 속도를 계획한다.

목적

모든 수학 강좌는 증명을 요구하고, 모든 철학 강좌는 논증을 요구한다. 그러나 그 어느 것도 추론 자체를 대상으로 삼지 않으며, 모두 결론이 전제로부터 따라 나온다는 것이 무엇을 뜻하는지를 당연한 것으로 여긴다. 이 강좌는 바로 그 물음을 주제로 삼는다. 그 목적은 논리학의 가장 단순한 언어에 대해, 추론을 대상으로 하는 최초의 완결된 수학 이론을 네 부분이 모두 드러나도록 세우는 것이다. 곧 논리식을 알아보고 모호함 없이 읽을 수 있는 언어, 기호의 의미를 고려하지 않고 연역을 만들어 내는 계산 체계, 각 논리식에 그 변항들의 각 진리값 할당 아래에서의 진리값을 부여하는 의미, 그리고 계산 체계와 의미가 일치한다는 증명이다.

그렇다면 이 강좌는 기호를 다루는 규칙의 모음이 아니라, 앞의 모든 것이 준비하는 완전성 정리라는 중심 결과를 가진 이론이다. 논리식 집합 Γ\Gamma 과 논리식 φ\varphi 에 대해, 연역 가능성 Γ⊢φ\Gamma \vdash \varphi 은 공리와 규칙으로 구성되어 φ\varphi 로 끝나는 논리식의 유한 열이 존재한다는 것을 말하고, 의미론적 귀결 Γ⊨φ\Gamma \models \varphi 는 Γ\Gamma 의 논리식들을 참으로 만드는 모든 진리값 할당이 φ\varphi 도 참으로 만든다는 것을 말한다. 두 관계는 서로 반대되는 생각에서 생겨나는데, 하나는 구문적이고 존재적이며, 다른 하나는 의미론적이고 보편적이다. 그런데도 강좌는 Γ⊢φ⇔Γ⊨φ\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi 임을 증명한다. 이로부터, 어떤 전제들로부터 무엇이 따라 나오는가에 대한 모든 물음은 더 쉬운 쪽에서 답할 수 있다는 것이 따라 나온다. 연역을 제시하거나, 표를 훑거나, 마지막 내용 수업이 가르치듯이 분해로 반박하는 것이다.

대상과 선수 지식

이 강좌는 수학, 컴퓨터 과학, 철학 공부를 시작하는 사람, 그리고 교육의 어느 단계에서든 증명이 무엇이며 왜 그것을 믿을 수 있는지를 정확히 알고 싶은 사람을 대상으로 한다. 대학 수학에 들어서서 증명에 걸려 넘어지는 학생, 회로와 프로그램과 충족 가능성 문제의 논리가 필요한 컴퓨터 과학 학생, 논증의 논리에서 그 이론으로 나아가고 싶은 철학 학생이 그들이다.

이것은 선수 과목이 없고 그 자체로 완결된 1수준 강좌이다. 논리학을 공부했거나, 집합론을 알거나, 정리를 증명해 본 적이 있다고 가정하지 않는다. 집합(원소 관계, 포함, 합집합, 논리식 집합), 함수(진리값 할당은 변항들로부터 {0,1}\{0, 1\} 로의 함수이다), 기호열, 귀납법에 관해 쓰는 것은 필요한 곳에서 가르친다. 집합과 기호열은 1단원의 언어에 관한 수업에서, 귀납법은 그다음 수업에서 쓰기 전에 가르친다. 가정하는 것은 두 가지뿐이다. 주의 깊게 읽는 것(형식 언어에서는 기호 하나를 더하거나 빠뜨리면 기호열이 바뀌기 때문이다)과 자연수의 초등 산술이다. 자연수는 이 강좌에서도 사이트의 다른 곳과 마찬가지로 11 부터 시작한다.

이 강좌가 이어지는 곳

이상에서 사이트 안에서 이 강좌가 차지하는 자리가 따라 나온다. 선수 과목이 없고, 수학, 컴퓨터 과학, 철학 세 학습 과정의 목표 강좌이다. 세 과정 모두에서 추론은 도구이자 대상이기 때문이다. 보완 관계에 있는 강좌가 셋 있으며, 앞이나 병행이나 뒤에, 어떤 순서로든 들을 수 있다. 아리스토텔레스 논리학은 명사 논리와 삼단논법을 공부하는데, 삼단논법의 타당성은 이 강좌가 다루지 않는 “모든”과 “어떤” 같은 낱말에 달려 있다. 또한 그 강좌는 어떤 전통에서 계산 체계에 이르렀는지를 보여 준다. 대수학과 기하학 I은 페아노 공리로부터 연역의 건물을 세우고, 이 강좌가 대상으로 연구하는 공리적 방법과 귀납법을 수에 대해 실제로 적용한다. 그 강좌의 계획은 이 강좌를 먼저 듣거나 병행할 것을 권한다. 끝으로 C++ 프로그래밍 I은 여기서 이론인 것을 실천으로 옮긴다. 기호열이 올바르게 형성되었는지 판정하기, 진리표 훑기, 표준형 계산하기, 반박 찾기는 모두 프로그램으로 쓸 수 있는 절차이다.

그런데 이 강좌는 표현력에 관한 물음을 열어 둔다. 그 언어는 “모든”도 “어떤”도 말할 수 없으며, 한국어로 된 논증의 형식화는 1단원에서부터 양화사를 잃는다. 따라서 예정된 후속 강좌는 술어 논리를 다루는 수리논리학 II이다. 그 강좌는 양화사와 대상들을 범위로 하는 변항으로 같은 길을 걸을 것이다. 건전성, 완전성, 콤팩트성은 이 강좌가 미리 보여 주는 방법으로 유지되지만, 거기서 의미론적 귀결은 더 이상 결정 가능하지 않게 된다.

전체 학습 목표

다음 목표들은 강좌를 마친 사람이 할 수 있어야 하는 것을 기술한다. 각 목표는 관찰 가능한 수행으로 진술되어 구체적인 과제로 확인할 수 있다. 내용 수업도 저마다 자신의 목표를 밝히며, 이 목표들은 하나 또는 여러 전체 목표에 봉사한다. 마무리 수업은 각 목표가 어느 단원과 어느 수업에서 다루어지는지 보여 준다. 일곱 목표에는 인용할 수 있도록 번호를 붙인다.

  1. 목표 1. 대상 언어와 메타언어를 구별하고, 형성 규칙으로 기호열이 논리식인지 판정한다.
  2. 목표 2. 자연 언어의 진술과 논증을 형식화하고, 형식화가 무엇을 보존하고 무엇을 잃는지 지적한다.
  3. 목표 3. 강좌의 체계(우카시에비치의 공리, modus ponens, 이중 부정 대체)에서 공리, 기본 규칙, 파생 규칙을 조합하여 연역을 구성한다.
  4. 목표 4. 자연수, 논리식의 복잡도, 연역의 길이에 관한 귀납법으로 메타정리를 증명한다.
  5. 목표 5. 타당성, 충족 가능성, 의미론적 귀결, 의미론적 동치를 진리표와 동치식으로 판정한다.
  6. 목표 6. 논리식을 표준형으로 변환하고, 그것으로 진리 함수와 회로를 표현한다.
  7. 목표 7. 건전성, 완전성, 콤팩트성을 설명하고 적용하며, 충족 불가능성을 분해로 판정한다.

목표 3과 목표 7은 각각 자기 단원, 곧 연역과 메타이론을 가진다. 목표 5와 목표 6은 의미론 단원을 나누어 가지는데, 앞의 것은 그 전반부에, 뒤의 것은 후반부에 있다. 목표 2는 고유한 수업, 곧 형식화 수업을 가지며, 그 뒤로는 문제가 말로 제시될 때마다 연습된다. 반면에 목표 1과 목표 4는 횡단적이다. 언어 안에서 말해지는 것과 언어에 관해 말해지는 것의 구별은 네 단원을 관통하고, 귀납법은 논리식의 유일 판독성에서 체계의 건전성과 칼마르 보조정리에 이르기까지 강좌의 모든 중요한 증명의 형식이다. 이로부터 그 달성을 한 수업에 돌릴 수 없으며, 강좌 전체에 걸쳐 길러 가는 것이 좋다는 것이 따라 나온다.

강좌의 체계와 그 결정들

명제 논리 강좌는 여러 방식으로 세울 수 있으며, 흔히 쓰이는 교재들은 언어, 기본 연결사, 연역 체계에서 서로 다르다. 이 강좌는 처음부터 알아 두면 좋은 세 가지 결정을 내린다. 그것들이 언뜻 보기에 이상해 보일 수 있는 것을 설명해 주기 때문이다.

원과 원판의 언어

강좌의 언어는 원 ∘\sigO 과 원판 ∙\sigI , 단 두 기호로 된 알파벳을 가진다. nn 번째 변항은 nn 개의 원 뒤에 원판 하나가 오는 기호열 vn=∘n∙v_{n} = \sigO^{n}\sigI 이며, 따라서 v1=∘∙v_{1} = \sigO\sigI 이고 v2=∘∘∙v_{2} = \sigO\sigO\sigI 이다. 형성 규칙은 하나뿐이다. φ\varphi 과 ψ\psi 가 논리식이면 ∙φψ\sigI\varphi\psi 도 논리식이며, 이것은 (φ↓ψ)(\varphi \downarrow \psi) 로 줄여 쓰고 “φ\varphi 도 아니고 ψ\psi 도 아니다”라고 읽는다. 따라서 부정논리합 ↓\downarrow 가 유일한 기본 연결사이고, 다른 연결사는 모두 한 번만 정의되는 약어이다. ¬φ\neg\varphi 는 (φ↓φ)(\varphi \downarrow \varphi) 이고, 선언 (φ∨ψ)(\varphi \vee \psi) 은 ¬(φ↓ψ)\neg(\varphi \downarrow \psi) 이며, 이들로부터 연언, 함의, 쌍조건, 배타적 선언이 정의된다. 이것들을 쓰는 다른 방식은 모두 증명되는 정리이지 정의가 아니다.

이 선택에는 대가가 있는데, 바로 가독성이며, 강좌는 이를 메타언어에서 치른다. 원과 원판의 기호열을 날마다 쓰는 사람은 없으며, 쓰는 것은 그 약칭이고, 그것은 언제든 그것이 가리키는 기호열까지 풀어 쓸 수 있다. 그러나 이 대가는 여러 번 보상된다. 두 기호로 무한히 많은 변항을 충분히 나타낼 수 있으므로, 모든 논리식은 두 원소로 된 알파벳 위의 유한 기호열이다. 연결사는 인수들 앞에 쓰이므로 괄호가 필요 없다. 유일 판독성은 각 변항에 +1+1 을, 각 연결 원판에 −1-1 를 부여하는 무게 논증으로 증명된다. 그리고 모든 복합 논리식은 부정논리합이므로, 복잡도에 관한 귀납법에 의한 증명은 모두 복합의 경우가 하나뿐이며, 이것이 뒤따르는 단원들의 모든 증명을 짧게 만든다. 연결사 하나로 다른 어떤 연결사든 표현할 수 있다는 것은 가정되지 않는다. 의미론 단원이 그것을 증명한다.

두 번째 기본 규칙

연역 체계는 얀 우카시에비치의 체계에서 출발한다. 부정과 함의로 쓰인 세 공리 도식과 유일한 규칙인 modus ponens이다. 이 도식들은 부정과 함의를 기본 연결사로 하는 언어를 위해 만들어졌다. 원과 원판의 언어에서 (v1↓v2)(v_{1} \downarrow v_{2}) 같은 논리식은 부정도 함의도 아니며, 공리들에게는 불투명하다. 연역 단원의 첫 수업은 모든 공리가 가지고 modus ponens가 보존하며 그 논리식은 가지지 않는 표지를 써서, 우카시에비치의 체계가 ((v1↓v2)→¬v1)((v_{1} \downarrow v_{2}) \rightarrow \neg v_{1}) 를 연역하지 못함을 증명한다.

그렇다면 체계를 보완해야 하며, 자연스러운 처방은 둘째 수업이 세 도식으로부터 연역하는 이중 부정 φ⊣⊢¬¬φ\varphi \dashv\vdash \neg\neg\varphi 을 증명하는 것처럼 보인다. 표지는 그것으로 충분하지 않음을 보여 준다. 이중 부정의 정리들은 표지를 보존하며, 그런데도 그것들을 써도 부정논리합 안에서 v1v_{1} 를 ¬¬v1\neg\neg v_{1} 으로 바꿀 수 없다. 따라서 둘째 수업은 이중 부정을 증명한 뒤에 두 번째 기본 규칙인 이중 부정 대체를 덧붙인다. 논리식 χ\chi 로부터, 그 안에서 부분식 θ\theta 의 한 출현을 ¬¬θ\neg\neg\theta 으로, 또는 ¬¬θ\neg\neg\theta 의 한 출현을 θ\theta 로 대체하여 얻는 논리식을 추론한다. 그러므로 강좌의 체계는 우카시에비치의 세 도식, modus ponens, 그리고 이 규칙으로 이루어진다.

부정논리합을 위한 다른 체계들은 거기에 맞추어 만든 공리 도식으로 같은 것을 얻는다. 이 강좌가 규칙을 택하는 이유는 두 가지이다. 그것은 한 행만 취하고 한 출현만 바꾸므로 modus ponens보다도 더 단순하며, 이중 부정이 이미 말하는 것, 곧 θ\theta 과 ¬¬θ\neg\neg\theta 가 서로 바꿔 쓸 수 있다는 것을 논리식의 모든 자리로 확장하여 표현하므로 인위적인 데가 전혀 없다. 게다가 그것은 각 행의 진리값을 보존하므로 건전하며, 증명에 경우 하나가 더해질 뿐 연역 정리를 보존한다. 이 규칙만 있으면 연역되어야 할 모든 것을 연역하기에 충분하다는 것이 마지막 단원의 완전성 정리이다.

강한 완전성보다 먼저 콤팩트성

완전성에는 세 단계가 있다. 약한 완전성은 모든 항진식이 정리라고 말한다. 유한 전제 집합에 대한 완전성은 유한한 전제 집합의 모든 의미론적 귀결이 그 집합으로부터 연역된다고 말한다. 강한 완전성은 같은 것이 임의의 집합, 무한한 집합에 대해서도 성립한다고 말한다. 강좌의 방법인 칼마르 보조정리는 논리식의 유한 개 변항과 유한한 전제들을 다루므로, 처음 두 단계에는 이르지만 세 번째에는 이르지 못한다. 거기에 이르려면, Γ⊨φ\Gamma \models \varphi 일 때 어떤 유한 부분 Γ0\Gamma_{0} , 곧 Γ\Gamma 의 유한 부분이 이미 Γ0⊨φ\Gamma_{0} \models \varphi 를 만족하면 충분하다. 그런데 바로 그것이 콤팩트성 정리가 주장하는 바이다.

많은 교재는 먼저 다른 방법으로 강한 완전성을 증명하고 그로부터 콤팩트성을 이끌어 낸다. 반면에 이 강좌에서는 강한 완전성이 찾는 대상이며, 그로부터 콤팩트성을 얻는 것은 순환이 된다. 그래서 순서가 뒤바뀐다. 콤팩트성 수업은 어떤 연역도 언급하지 않고 의미론 안에서 v1,v2,…v_{1}, v_{2}, \ldots 의 값을 하나씩 고정하여 콤팩트성을 증명하며, 그런 다음에야 세 줄로 강한 완전성, 곧 Γ⊨φ⇒Γ⊢φ\Gamma \models \varphi \Rightarrow \Gamma \vdash \varphi 가 모든 집합 Γ\Gamma 에 대해 성립함을 얻는다.

내용

강좌는 여섯 단원으로 이루어진다. 이 소개, 네 개의 내용 단원, 그리고 마무리이다. 각 내용 단원은 도입 수업으로 시작하며, 도입 수업은 단원의 수업들, 강좌에서 단원이 차지하는 자리, 단원이 이미 안다고 가정하는 것, 단원이 해결하는 문제를 제시하고, 입문 평가로 시작한다. 단원은 종합 수업으로 끝나며, 종합 수업은 단원의 연역 사슬을 재구성하고, 그것을 강좌의 나머지와 연결하며, 마무리 평가에서 입문 평가의 기능들을 되풀이하고, 수업의 문제들보다 어려운 여섯 도전 과제를 제시한다.

0단원. 강좌 소개

이 수업으로 이루어지며, 이 수업은 강좌의 목적, 전체 목표, 결정, 내용, 학습량, 설계를 정한다.

1단원. 언어

그 목표는 강좌가 연구하는 언어를 세우고, 각 논리식이 오직 한 가지 방식으로 읽힌다는 것을 증명하고, 그것을 한국어 논증과 연결하는 것이다.

  1. 언어: 도입.
  2. 수리논리학이란 무엇인가: 진리에 대비한 타당성, 반례, 역설, 대상 언어와 메타언어의 구별.
  3. 명제 논리의 언어: 집합과 기호열, 원과 원판의 언어, 그 형성 규칙과 약어.
  4. 자연수와 논리식에 관한 귀납법: 단순 귀납법, 강한 귀납법, 구조적 귀납법, 무게 보조정리, 유일 판독성, 재귀적 정의.
  5. 자연어의 형식화: 사전, 진술과 논증의 번역, 실질 조건문이 잃는 것.
  6. 언어: 종합과 도전 과제.

2단원. 연역

그 목표는 언어에 계산 체계, 곧 강좌의 체계를 주고, 그 안에서 수학이 이름 붙이지 않고 쓰는 추론 형식들을 각각 한 번씩 도출하는 것이다.

  1. 연역: 도입.
  2. 형식 연역 체계: 우카시에비치의 체계, 전제로부터의 연역, 연역 정리, 그 한계를 보여 주는 표지.
  3. 네 가지 연역 기법: 가언 삼단논법, 전제 교환, 이중 부정, 대우, 이중 부정 대체.
  4. 연결사의 대칭성: 부정논리합의 기본 보조정리, 동치인 것의 대체, 연결사의 다른 형태들과 그 다섯 대칭성.
  5. 고전 논리의 기법: 각 연결사의 규칙, 배중률, 경우에 따른 증명, 귀류법(전제를 가진 경우).
  6. 드모르간 법칙과 분배 법칙: 양방향의 증명과 다른 논리식 안에서의 동치인 것의 대체.
  7. 연역: 종합과 도전 과제.

3단원. 의미론

그 목표는 논리식에 의미를 주고, 그것으로 타당성과 의미론적 귀결을 판정하며, 모든 논리식을 표준형으로 환원하는 것이다.

  1. 의미론: 도입.
  2. 명제 논리의 의미론: 진리값 할당과 재귀에 의한 그 확장, 일치 보조정리, 진리표, 타당성과 충족 가능성.
  3. 의미론적 귀결과 동치: 집합으로부터의 의미론적 귀결, 의미론적 연역 정리, 대체와 균일 대입.
  4. 일반화된 드모르간 법칙과 분배 법칙: nn 개 항의 연언과 선언, 그리고 귀납법에 의한 그 법칙들.
  5. 함수적 완전성: 모든 진리 함수는 논리식을 가지며, 부정논리합 하나로 충분하고, 충분한 연결사 집합들.
  6. 표준형: 리터럴, 절, 선언 표준형과 연언 표준형, 그 쌍대성과 존재.
  7. 표준형 알고리즘과 그 응용: 올바르고 반드시 종료하는 알고리즘, 스위치 회로의 설계와 간소화.
  8. 의미론: 종합과 도전 과제.

4단원. 메타이론

그 목표는 연역과 의미론적 귀결이 일치함을 먼저 유한한 전제에 대해, 다음에 임의의 전제에 대해 증명하고, 그것들을 판정하는 세 번째 방법을 제시하는 것이다.

  1. 메타이론: 도입.
  2. 건전성과 완전성: 행에 관한 귀납법에 의한 건전성, 무모순성, 칼마르 보조정리, 약한 완전성과 유한 전제 집합에 대한 완전성.
  3. 콤팩트성 정리: 그 의미론적 증명, 동치인 형태들, 거기서 따라 나오는 강한 완전성, 조합론적 응용.
  4. 분해 방법: 절 형식, 분해 규칙, 그 건전성과 반박 완전성, 그 비용.
  5. 메타이론: 종합과 도전 과제.

5단원. 강좌 마무리

수리논리학 I: 최종 결산 수업으로 이루어진다. 이 수업은 일곱 전체 목표를 상기시키고, 각 목표가 어느 단원과 어느 수업에서 다루어지는지 그림으로 보여 주며, 마무리 평가의 첫 시도를 목표별로 모으고, 공부가 어디로 이어지는지 가리킨다.

학습량과 학점

강좌의 학습량은 강의 시간으로 재지 않는다. 비동기 강좌에는 강의 시간이 없기 때문이다. 재는 것은 공부하는 사람의 작업 총량, 곧 읽기, 증명과 연역 따라가기, 문제 풀기, 복습이다. 추정은 사이트의 모든 강좌에서 같은 방법을 따른다. 각 수업 본문을 분당 백 단어로 읽는 시간(논리식 하나를 한 단어로 센다), 예제 문제 하나에 이십 분, 연습 문제 하나에 삼십오 분, 도전 과제 하나에 사십오 분, 입문 평가나 마무리 평가 한 번에 십이 분을 세고, 복습을 위해 십분의 일의 여유를 더한다.

결과

강좌의 수업들은 모두 합해 예제 문제 9090 개, 연습 문제 9090 개, 도전 과제 2424 개를 담고 있으며, 그 밖에 단원 평가가 여덟 번 있다. 단원별 추정 학습량은 시간 단위로 반올림하면 다음과 같다.

  • 0단원, 강좌 소개: 11 시간 미만.
  • 1단원, 언어: 3030 시간.
  • 2단원, 연역: 3636 시간.
  • 3단원, 의미론: 4343 시간.
  • 4단원, 메타이론: 2525 시간.
  • 5단원, 강좌 마무리: 11 시간 미만.

합계는 약 137137 시간의 학습이다. 이 수치는 있는 그대로 읽어야 한다. 곧 모든 증명을 공부하고 모든 문제와 도전 과제를 푸는 사람에 대한 추정이다. 이미 논리학을 공부한 사람이나 도전 과제에 손대지 않고 연습 문제에 그치는 사람은 훨씬 적은 시간이 들 것이다. 정리를 한 번도 증명해 본 적이 없는 사람은 더 많은 시간이 필요할 수 있으며, 특히 연역과 의미론 단원에서 그러한데, 이 두 단원은 분량도 가장 많다.

그러나 이 수치는 명목상의 것이다. 강좌의 학점은 이 수치로 정해지며, 일정한 속도로 읽고 도전 과제 하나에 사십오 분을 쓴다고 가정한다. 실제 학생들로 측정되기 전까지는 현실적인 범위를 함께 제시하는 것이 좋다. 각 연역을 종이와 연필로 옮겨 적고 원과 원판의 기호열을 하나하나 손으로 분해할 때처럼 읽는 속도가 가정의 절반이 되고, 도전 과제 하나에 사십오 분이 아니라 칠십오 분이 걸린다면, 같은 방법으로 약 174174 시간이 된다. 따라서 예상 학습량은 약 137137 시간에서 약 174174 시간 사이에 있다. 상한은 신중한 상계이지 측정값이 아니다. 이 범위는 강좌를 공부하는 사람들이 실제로 쓰는 시간이 알려지면 수정되며, 그때까지 학점은 명목상의 수치로 계산한다.

권장 속도

속도를 부르기 위해 이 계획은 사이트의 다른 계획들과 같은 기준을 쓴다. 전일제는 6060 학점의 한 학년, 곧 약 사십 주에 걸친 약 16501650 시간, 다시 말해 주당 약 4040 시간이며, 시간제는 그 절반, 주당 약 2020 시간이다. 여기서 권장 속도가 따라 나온다. 십육 주의 한 학기에 주당 약 88 시간 또는 99 시간을 공부하는 것으로, 전일제의 오분의 일을 조금 넘는다. 현실적인 범위로는 주당 99 시간에서 1111 시간이다. 이 학기는 대수학과 기하학 I과 나누어 쓸 수 있는데, 그 강좌의 증명은 연역이 이미 익숙한 대상일 때 더 잘 읽힌다.

주당 약 2020 시간, 곧 시간제의 집중 속도로는 칠 주에 강좌를 마친다. 주당 약 44 시간 또는 55 시간의 더 여유로운 속도로는 두 학기에 걸치며, 두 학기는 거의 절반씩 나뉜다. 0단원에서 2단원까지, 곧 언어와 연역이 약 6767 시간을, 3단원에서 5단원까지, 곧 의미론, 메타이론, 마무리가 약 6969 시간을 차지한다.

호환 학점으로의 환산

호환 학점 제도는 강좌를 대면 수업 시간이 아니라 강좌가 수강자에게 요구하는 작업의 총량으로 잰다. 한 기관에서 마친 학업을 다른 기관에서 인정받을 수 있게 하려는 것이다. 유럽 학점 상호 인정 및 누적 제도는 볼로냐 선언 이후 유럽 대학들이 채택한 것으로, 전일제 한 학년에 6060 학점을 배정하고 한 학점을 2525 시간에서 3030 시간의 학습으로 정한다. 칠레 호환 학점 제도는 칠레 대학들이 비슷한 설계로 채택한 것으로, 역시 한 학년에 6060 학점을 배정하고 한 학점을 2424 시간에서 3131 시간의 학습으로 정한다.

그런데 추정한 137137 시간을 각 구간의 양 끝으로 나누면, 강좌는 약 55 유럽 학점(4.6에서 5.5), 그리고 44 에서 66 칠레 호환 학점(4.4에서 5.7)에 해당한다. 두 구간의 중앙값인 학점당 27.5시간을 기준으로 삼으면 두 제도 모두에서 같은 수 4.98을 얻으며, 이를 반올림하면 5가 된다. 유럽 학점의 경우 학점 수 CC 는 다음과 같이 범위가 정해진다.

(13730)≤C≤(13725)\left( \frac{137}{30} \right) \leq C \leq \left( \frac{137}{25} \right)

따라서 이 강좌에는 유럽 학점 55 학점과 칠레 호환 학점 55 학점을 부여할 것을 권장한다. 이는 전일제 한 학년의 십이분의 일로, 보통의 6학점 한 학기 과목보다 조금 적다.

강좌의 설계

형태

강좌는 비동기, 온라인, 자기 주도 속도로 진행된다. 일정도 실시간 수업도 마감도 없으며, 각 학생은 자신의 준비와 시간이 허락하는 속도로 나아간다. 강좌는 사이트의 열네 언어로 제공되며, 모든 언어에서 논리는 같다. 논리식, 연역, 증명의 단계는 모든 판에서 동일하며, 번역되는 것은 본문뿐이다. 수업들은 먼저 공부해 두면 좋은 다른 수업들을 밝히므로, 권장 순서가 명시되어 있다.

수업의 구성

모든 내용 수업은 같은 구성을 따른다. 요약과, 관찰 가능한 수행으로 진술된 고유한 학습 목표의 목록으로 시작한다. 이어서 이론이 나오는데, 정의, 정확히 진술된 결과와 그 증명, 그리고 예로 이루어진다. 증명은 단계 재생기로 제시된다. 각 단계는 한 행을 쓰고, 바뀌는 부분을 강조하며, 앞선 결과에 기댈 때는 그 결과로 돌아간다. 체계의 연역은 번호 붙은 행으로 쓰이고, 각 행의 근거가 오른쪽에 적히며(공리, 전제, 쓰인 행들과 함께 적은 modus ponens, 또는 파생 규칙), 진행함에 따라 인용된 행들이 강조된다. 수업의 끝에는 단계별 풀이가 붙은 예제 문제 다섯 개와 연습 문제 다섯 개가 있으며, 연습 문제마다 접힌 힌트와 그 뒤의 최종 답이 있다. 증명을 요구하는 연습 문제에는 답 뒤에 접힌 상세 풀이가 덧붙는데, 이것은 자신의 풀이를 써 본 다음에만 여는 것이 좋다.

또한 각 수업은 사이트의 낭독기로 소리 내어 들을 수 있으며, 낭독기는 원, 원판, 연역과 의미론적 귀결의 기호를 포함하여 논리식의 기호를 말로 읽는다.

평가

강좌는 성적을 매기지 않는다. 그 평가는 형성적이며 자기 평가에 기반한다. 연습 문제로 각 수업의 목표 달성을, 도전 과제로 각 단원의 목표 달성을 확인할 수 있다. 여기에 단원 평가가 더해진다. 입문 평가는 도입의 처음에 있으며, 단원의 문항에 단원이 이미 안다고 가정하는 것에 관한 문항 몇 개를 더하므로, 열한 개에서 열다섯 개의 문항으로 출발점을 잰다. 마무리 평가는 종합 수업에서 도전 과제 앞에 있으며, 열두 문항으로 달성한 것을 재고 입문 평가와 비교된다. 두 평가 모두 브라우저 안에서 채점되며, 답마다 설명과 복습하면 좋은 수업으로의 안내가 붙는다. 그 결과는 응답한 사람의 브라우저에만 저장되며, 최종 결산은 각 마무리 평가의 첫 시도를 전체 목표별 개요로 모은다.

이 강좌를 공부하는 방법

강좌는 순서대로 공부하도록 짜여 있다. 각 단원은 앞의 단원들을 전제로 한다. 연역은 첫 단원의 언어로 쓰이고, 의미론은 그 논리식에 값을 주며, 메타이론은 둘째 단원과 셋째 단원을 비교한다. 수업 하나를 건너뛰면 조만간 그리로 돌아가야 한다.

각 수업에서는 먼저 요약과 목표를 읽는 것이 좋다. 다음에 종이와 연필로 이론을 공부하면서 원과 원판의 기호열을 옮겨 적고, 그 변항들과 원판들을 나누며, 재생기가 쓰기 전에 연역의 각 행을 미리 짐작한다. 예제 문제는 풀이를 보기 전에 시도하고, 연습 문제는 도움 없이 풀며, 힌트는 시도가 바닥났을 때에만 연다. 시도하기 전에 답을 본 문제는 푼 것이 아니라 읽은 것이다.

끝으로 각 주장이 어느 층위에 속하는지 늘 구별하는 것이 좋다. 그것이 논리식처럼 언어 안에서 무언가를 말하는지, 아니면 Γ⊢φ\Gamma \vdash \varphi 이나 Γ⊨φ\Gamma \models \varphi 처럼 언어에 관해 무언가를 말하는지를 구별하는 것이다. 이 구별은 강좌 목표의 첫째이며, 또한 강좌의 중심 결과를 이해할 수 있게 해 주는 것이기도 하다. 그 결과는 메타언어에서만 진술될 수 있다.