논리의 기본 개념부터 고전 논리와 직관주의 논리, 그리고 논리를 범주와 순서로 해석하는 방법까지 그림과 함께 설명합니다.
이제 우리가 이것이 범주론임을 깨달을 때 스스로를 “놀라게” 하기 위해, 겉보기에 또 하나의 관련 없어 보이는 주제에 대해 이야기해 보자. 그런데 말하자면, 이 장에는 그것 말고도 또 하나의 놀라움이 있으니 졸지 마시길.
또한 나는 여러분을 단지 수학의 다른 한 분야로 데려가는 데 그치지 않고, 완전히 다른 학문 분야인 논리학 으로 데려가려 한다.
논리학은 가능한 것 의 과학이다. 그런 의미에서 논리학은 다른 모든 과학의 뿌리에 있으며, 다른 모든 과학은 현실적인 것, 즉 실제로 존재하는 것의 과학이다. 예를 들어, 과학이 우리 우주가 어떻게 작동하는지를 설명한다면, 논리학은 그 설명 가운데 존재할 가능성이 있는 다른 어떤 우주에도 적용될 수 있는 부분이다. 과학 이론은 자기 자신과 관측 모두와 일관적이어야 하지만, 논리 이론은 자기 자신과만 일관적이면 되고, 관측과 무관하게 참이면 된다.
따라서 우리는 이렇게 말할 수 있다.
논리학은 어떤 한 가지를 아는 것으로부터 다른 어떤 것도 참이라고 결론짓게(또는 증명하게) 하는 규칙들 을 연구한다. 이때 그 대상들이 속한 분야(예: 과학의 세부 분야)와 무관하며, 오직 그것들의 형식만을 참조한다(“형식적으로”). 더 나아가 논리학은 그런 규칙들을 논리 체계 (또는 형식 체계 라고도 한다)로 조직하려고 한다.
이 설명을 보면, 논리학의 주제가 첫 장에서 설명한 집합론과 범주론의 주제와 꽤 비슷하다고 생각할 수 있다. “formal”이라는 단어 대신 우리는 비슷한 다른 단어인 “abstract”를 썼고, “logical system” 대신 “theory”라고 말했다. 이 관찰은 상당히 정확하다. 오늘날 대부분의 사람들은 모든 수학 이론이 사실상 논리학에 몇 가지 추가 정의를 덧붙인 것이라고 동의한다. 예를 들어 집합론 이 수학의 기초 이론으로 매우 인기 있는 이유 중 하나는, 곧 보게 될 표준 논리 공리에 단 하나의 원시 개념만 추가하여 정의할 수 있기 때문이다. 그 원시 개념은 집합의 원소 관계 를 나타내는 이항 관계다. 범주론도 논리와 가깝지만, 꽤 다른 방식으로 그러하며, 그것은 나중에 이해하게 될 것이다. 자, 이제 시작해 보자.
논리학이 가능한 것의 과학이라는 사실의 한 결과는, 논리학에서 무엇이든 하려면 먼저 참 또는 거짓으로 받아들이는 명제들의 초기 집합이 있어야 한다는 점이다. 이것들은 “전제”, “기본 명제”, 또는 비트겐슈타인이 불렀듯이 “원자 명제”라고도 한다.
논리학 자체의 맥락에서는 이러한 명제들은 추상화되어 있다. 즉, 우리는 그것들 자체를 직접 다루지 않으므로, 익숙한 색깔 공들로 표현할 수 있다.
범주론에서와 마찬가지로 논리학의 핵심에는 합성 이라는 개념이 있다. 서로 어떤 방식으로든 관련된 두 개 이상의 명제가 있다면, 우리는 “그리고”, “또는”, “따른다” 등의 논리 연산자를 사용하여 그것들을 하나로 결합할 수 있다. 그 결과는 새로운 명제가 되며, 이것들이 기본 명제가 아님을 강조하기 위해 합성 명제 라고 부를 수 있다.
이 합성은 두 모노이드 대상이 모노이드 연산을 통해 하나로 결합되는 방식과 닮아 있다. 실제로 몇몇 논리 연산은 모노이드를 이룬다. 예를 들어 그리고 연산은, 항등원 역할을 하는 명제와 함께 모노이드를 이룬다.
하지만 모노이드나 군과 달리, 논리학은 하나의 연산만이 아니라 여러 논리 연산과 그들이 서로 맺는 관계 를 연구한다. 예를 들어 논리학에서는 그리고 와 또는 연산의 분배 법칙, 그리고 그것이 함의하는 바에 관심을 가질 수 있다.
여기서 주의할 점은 가 and 의 기호이고, 가 or 의 기호라는 점이다(물론 위 법칙은 실제로 and 와 or 를 뒤바꾸어도 여전히 성립한다).
방금의 마지막 그림을 볼 때 강조해야 할 중요한 점은, 여러 전제로 이루어진 명제들(다른 공들을 품고 있는 회색 공으로 표시됨)이 “기본” 명제(단색 공)와 어떤 면에서도 다르지 않으며, 똑같은 방식으로 다시 합성된다는 것이다(다만 가장 왼쪽 명제에서는 그림을 더 보기 좋게 하기 위해 초록 공을 회색 공으로 감쌌다).
여러 단계의 중첩을 포함하는 명제의 예이자, 동시에 논리학 자체에 대한 훌륭한 입문으로서, 역사상 가장 오래되고(기원전 3세기 스토아 학파에게도 이미 알려져 있었다) 가장 유명한 명제 중 하나인 modus ponens 를 생각해 보자. 보통 이것은 다음과 같이 제시된다.
모든 인간은 죽는다.
소크라테스는 인간이다.
그러므로 소크라테스는 죽는다.
또는 이렇게 말할 수도 있다.
오늘이 화요일이면, John은 출근할 것이다.
오늘은 화요일이다.
그러므로 John은 출근할 것이다.
패턴이 보일 것이다. modus ponens는 여기서 와 로 표시하는 두 다른 명제로 이루어진 명제이며, 명제 가 참이고 또한 명제 가 참이라면(즉, 가 를 함의한다면), 도 참이라고 말한다. 첫 번째 예에서는 “소크라테스는 인간이다” ()와 “인간은 죽는다” 또는 “인간임은 죽음을 함의한다” ()를 안다면, “소크라테스는 죽는다” ()도 알게 된다.
이것을 그림으로 표현하면 다음과 같다.
modus ponens 명제는 관계로 연결된 두 다른 명제로 이루어져 있으며, 명제 는 기본 명제이지만, 를 함의하는 명제 는 기본 명제가 아니다(이것을 라고 부르자. 그러면 전체 명제는 가 된다).
한 단계 더 내려가 보면, 명제 는 그 자체가 and 관계에 있는 두 명제로 이루어져 있음을 알 수 있다. 다른 하나를 라고 하자(따라서 ). 그리고 는 다시 관계로 결합된 두 명제로 이루어져 있다. 즉, 이다. 하지만 이 모든 것은 그림으로 보는 편이 더 낫다.
주어진 합성 명제가 참인지 거짓인지는, 그것을 이루는 명제들의 값을 알기 전에는 종종 판단할 수 없다. 그러나 modus ponens 같은 명제는 다르다. modus ponens는 그것을 이루는 명제들이 참이든 거짓이든 상관없이 항상 참 이다. 멋지게 말하자면, 그것은 논리 체계의 모든 모델에서 참 이라고도 할 수 있다. 여기서 모델이란, 우리의 명제들이 가리키는 것으로 받아들여지는 현실 세계의 전제들의 집합이다.
예를 들어, 앞의 예에서 “소크라테스”를 다른 어떤 이름으로 치환 하거나, “죽는다”를 인간이 가진 다른 어떤 성질로 치환하더라도 그 명제는 참인 것을 멈추지 않는다.
이런 명제를 항진식이라고 부른다.
항상 참인 명제를 항진식 이라고 부른다. 그리고 더 잘 알려진 짝인, 항상 거짓인 것들은 모순 이라고 부른다.
모든 항진식은 “not”을 하나 붙여 모순으로 바꿀 수 있고, 반대로도 가능하다.
반면 다른 명제들, 즉 어떤 다른 명제들의 값에 따라 참일 수도 거짓일 수도 있는 명제들은 “우연 명제”라고 부른다. 논리학에서는 우연 명제에 관심이 없다. 결국 그것들은 다른 모든 과학이 다루는 것이기 때문이다(그리고 우리는 다른 과학들과 같지 않다).
가장 단순한 항진식은 이른바 동일률로, 각 명제가 자기 자신을 함의한다는 주장이다(예: “모든 총각은 미혼이다”). 이것은 여러분에게 무엇인가를 떠올리게 할지도 모른다.
다음은 조금 더 복잡한(덜 지루한) 항진식들이다(기호 는 “not”/부정을 뜻한다).
어떤 명제가 항진식인지 판별하는 방법은 곧 배우겠지만, 먼저 항진식이 왜 중요한지 보자.
항진식이 유용한 이유는 그것들이 공리 도식 / 추론 규칙 의 기초이기 때문이다. 그리고 공리 도식 과 추론 규칙 은 치환을 통해 다른 참인 논리 명제들을 생성할 수 있는 출발점 역할을 한다.
modus ponens에서 공들의 색깔이 본질적이지 않다는 것을 깨닫고 나면, 우리는 그것의 모든 변형이 공유하는 일반 구조를 표현하고 싶어질 수 있다.
이 구조(우리 예시에서는 색칠 공부 책처럼 보이는 그것)를 공리 도식 이라고 한다. 그리고 그것이 만들어 내는 명제들을 공리 라고 한다.
공리 도식은 변수들을 포함하는 공식이며, 그 변수들을 명제로 바꾸어 넣음으로써 명제들을 도출할 수 있다.
도식에 넣는 명제들은 기본 명제일 필요가 없다는 점에 주의하라. 예를 들어 명제 (아래에서는 주황색 공으로 상징된다)와, 가 를 함의한다는 명제(앞에서 본 항진식들 중 하나)를 가지고 있다면, 이 명제들을 modus ponens 에 대입하여 가 참임을 증명할 수 있다.
그리고 추론 규칙 은 공리 도식과 거의 같은 것이다. 예를 들어 공리 도식은 쉽게 추론 규칙으로 사용할 수 있고, 반대로도 가능하다.
공리 도식/추론 규칙을 사용해 새로운 명제를 생성할 수 있다는 것을 알게 되면, 우리는 이런 물음을 던질 수 있다. 가능한 모든 명제를 생성할 수 있도록 정교하게 고른, 작은 수의 도식/규칙 모음을 만들 수 있을까? 기쁘게도(아마 약간은 짜증도 나겠지만) 그런 모음은 하나가 아니라 여럿 존재한다. 그리고 그렇다. 이런 종류의 모음이 바로 우리가 논리 체계 라고 부르는 것이다.
논리 체계(형식 체계라고도 한다)는 공리 도식/추론 규칙의 모음으로, 그것들을 적용함으로써 가능한 모든 명제를 생산할 수 있는 것이다.
다음은 그런 모음의 한 예로, modus ponens 라는 추론 규칙에 더하여 다음 다섯 개의 공리 도식으로 이루어진다(색을 쓰고 있지만 이것들은 공리 도식이다).
이것과 비슷한 다른 논리 체계들이 완전하다는 것, 즉 실제로 다른 모든 명제를 생성할 수 있다는 것을 증명한 것은 Gödel이며, 이것은 “Gödel의 완전성 정리”로 알려져 있다(Gödel은 너무 중요해서, 나는 그의 이름을 올바르게 쓰기 위해 특별히 “ö” 문자를 찾아봤다).
이제 우리는 몇몇 주요 논리 구성물들(공리, 추론 규칙)이 어떻게 작동하는지에 대해 어느 정도 감을 잡았다. 하지만 그것들이 실제로 작동함을 보이고, 그것들이 무엇인지 이해하려면, 그러한 구성물들에 대한 특정한 해석 을 통해 그렇게 해야 한다.
우리는 두 가지 해석을 볼 것이다. 하나는 매우 오래된 것이고, 다른 하나는 비교적 최근의 것이다. 이것은 우리가 평소 다루는 점과 화살표의 주제에서 약간 벗어나는 길이 되겠지만, 그만한 가치가 있을 것이라고 장담한다. 자, 시작하자.
우리가 매일 살고 지각하는 세계 너머에는 이데아의 세계 가 존재하며, 그곳에는 우리가 지각하는 사물들 속에 드러나는 모든 관념과 개념들이 머무른다. 예를 들어 지금까지 살아온 모든 사람들 너머에는 원형적인 인간이 있으며, 우리는 그 인간을 닮은 만큼만 인간이다. 세상에 존재하는 모든 강한 것들 너머에는 궁극적인 힘의 개념이 있으며, 모든 것은 거기서 힘을 빌린다. 그리고 이것은 모든 범주에 대해 마찬가지다. 예를 들어 컵이 있다면, “컵다움”도 있다. 그리고 비록 우리 같은 필멸자는 현상의 세계에 살며 이데아의 세계를 직접 지각할 수는 없지만, 철학을 통해 그것을 “상기”하고 그 특징 중 일부를 알 수 있다.
위 문단은 그리스 철학자 Plato의 세계관을 요약한 것으로, 때로 Plato의 이데아론 이라고 불린다. 원래 논리학이라는 분야는 이 이데아의 세계에 적용될 수 있는 방식, 즉 “형식적”인 방식으로 사고하고 사유를 구조화하려는 노력이었다. 오늘날 이 원래의 논리 패러다임은 “고전 논리”로 알려져 있다. 비록 모든 것이 Plato에서 시작되었지만, 그 대부분은 20세기 수학자 David Hilbert 덕분이다.
이데아의 세계가 존재한다는 것은, 우리가 인간으로서 모르는 것, 앞으로도 결코 알지 못할 것이 많더라도, 적어도 어딘가에는 모든 질문에 대한 답이 존재한다는 뜻이다. 논리학에서는 이것이 이중값 원리 로 옮겨지며, 이는 각 명제는 참이거나 거짓이다 라고 말한다. 그리고 이 원리 덕분에, 고전 논리의 명제들은 두 값을 포함하는 불 집합으로 집합론에서 적절히 표현될 수 있다.
그렇다면 논리 연산자들은 그저 우리가 너무도 익숙한 함수들일 뿐이다.
고전적 논리 해석에 따르면:
- 기본 명제 는 참이거나 거짓인 어떤 것이다(불 값).
- 논리 연산자 는 하나 또는 여러 개의 불 값을 받아 또 다른 불 값을 돌려주는 함수 이다.
- 합성 명제 는 논리 연산자를 다른 명제들에 적용한 결과로 생기는 것이다.
이제 이 의미론적 맥락에서 모든 논리 연산자를 살펴보자.
먼저 부정 연산부터 시작하자. 부정은 단항 연산이며, 이는 인자를 단 하나만 받는 함수라는 뜻이다. 그리고 다른 모든 논리 연산자와 마찬가지로 하나의 값을 반환하는데, 인자와 반환값 모두 불 값이다.
이 함수는 다음 표로도 조금 덜 화려하게 표현할 수 있다.
| p | ¬p |
|---|---|
| True | False |
| False | True |
이런 표를 진리표 라고 하며, 고전 논리에서는 어디에나 등장한다. 이것들은 연산자를 정의하는 데뿐만 아니라 결과를 증명하는 데에도 사용할 수 있다.
부정 연산자를 정의했으므로, 이제 우리가 본 논리 체계의 첫 번째 공리인 이중 부정 제거 를 증명할 수 있다. 자연어로 말하면, 이 공리는 “나는 X를 할 수 없지 않다 ”라고 말하는 것이 “나는 그것을 할 수 있다 ”라고 말하는 것과 같다는 관찰에 해당한다.
(자명해 보이지만, 이중 부정 공리는 아마도 논리학에서 가장 논쟁적인 결과일 것이다. 왜 그런지는 나중에 보게 된다.)
논리 연산자를 불 값 집합으로부터 불 값 집합으로 가는 함수로 본다면, 공리를 증명하는 일은 그러한 함수 여러 개를 하나의 함수로 합성한 뒤 그 출력을 관찰하는 일이다. 더 구체적으로 말해, 위 공식을 증명하는 일은 단지 부정 함수를 자기 자신과 합성하고 그것이 우리를 출발한 자리로 되돌려 놓는지 확인하는 것이다.
이를 형식적으로 말하면, 부정을 두 번 적용하는 것은 항등 함수 를 적용하는 것과 동치라고 할 수 있다.
그림이 지겹다면, 위의 합성 그림을 표로도 나타낼 수 있다.
| p | ¬p | ¬¬p |
|---|---|---|
| True | False | True |
| False | True | False |
고전 논리의 모든 명제는 이런 그림이나 표로 증명할 수 있다.
좋다. 여러분 도 and 가 무엇인지 알고 나 도 그것이 무엇인지 알지만, 모든 것을 형식적으로 명시하고 싶어 하는 그 성가신 사람들은 어쩌란 말인가(알지, 알지). 그런데 우리는 이미 그들을 만족시키는 방법을 알고 있다. and 를 나타내는 불 함수만 구성하면 된다.
and 는 이항 연산자이므로, 함수는 하나의 값 대신 한 쌍의 불 값을 인자로 받는다.
이에 대응하는 진리표는 다음과 같다(여기서 는 and 의 기호다).
| p | q | p ∧ q |
|---|---|---|
| True | True | True |
| True | False | False |
| False | True | False |
| False | False | False |
에 대해서도 같은 일을 할 수 있다. 다음이 그 표다.
| p | q | p ∨ q |
|---|---|---|
| True | True | True |
| True | False | True |
| False | True | True |
| False | False | False |
과제 1: or 의 그림을 그려 보라.
이 표들을 사용해 나중에 쓸 몇 가지 공리 도식도 증명할 수 있다.
이제 조금 덜 자명한 것을 보자. 바로 implies 연산, (또는 material condition 이라고도 한다)이다. 이 연산은 두 명제를 묶는데, 첫 번째 명제의 참이 두 번째 명제의 참을 함의하는 방식으로 묶는다(또는 첫 번째 명제가 두 번째 명제의 필요조건 이라는 뜻이다). 는 “가 참이면, 도 참이어야 한다”라고 읽을 수 있다.
Implies 역시 이항 함수다. 즉, 정렬된 불 값 쌍에서 불 값으로 가는 함수로 표현된다.
| p | q | p → q |
|---|---|---|
| True | True | True |
| True | False | False |
| False | True | True |
| False | False | True |
여기에는 자명하지 않은 면이 있으므로 모든 경우를 하나씩 살펴보자.
고전 논리에서 는 (가 거짓이거나 가 참일 때) 참이라는 점을 기억해 두면 도움이 될 것이다.
이제 두 명제가 동치임을 나타내는 연산을 살펴보자(또는 한 명제가 다른 명제의 필요충분조건 이라는 것, 이는 그 자체로 역도 참이라는 뜻이다). 이 연산은 두 명제가 같은 값을 가질 때 참을 낸다.
| p | q | p ↔ q |
|---|---|---|
| True | True | True |
| True | False | False |
| False | True | False |
| False | False | True |
하지만 이 연산에서 더 흥미로운 점은, 이것이 implies 연산을 사용해 구성될 수 있다는 것이다. 즉, 이는 각 명제가 서로를 함의하는 것과 동치다(따라서 는 와 같다). 이것은 진리표를 비교함으로써 쉽게 증명할 수 있다.
| p | q | p → q | q → p | p → q ∧ q → p |
|---|---|---|---|---|
| True | True | True | True | True |
| True | False | False | True | False |
| False | True | True | False | False |
| False | False | True | True | True |
이 때문에 동치 연산은 “if and only if”, 줄여서 “iff”라고 불린다.
이제 위의 공식, 즉 가 와 같다는 공식을 살펴보자.
이것은 진리표를 사용하면 쉽게 증명할 수 있다.
| p | q | p → q | ¬p | q | ¬p ∨ q |
|---|---|---|---|---|---|
| True | True | True | False | True | True |
| True | False | False | False | False | False |
| False | True | True | True | True | True |
| False | False | True | True | False | True |
하지만 공리와 추론 규칙을 사용하면 훨씬 더 직관적이다. 그렇게 하려면, 우리가 가진 공식()과 공리 도식들로 시작해서, 증명하고 싶은 공식()에 도달하면 된다.
다음은 그 한 가지 방법이다. 각 단계에서 사용되는 공식은 오른쪽에 적혀 있고, 추론 규칙은 modus ponens이다.
두 공식이 정말로 동치임을 증명하려면, 반대 방향으로도 해야 한다는 점에 주의하라(즉, ()에서 시작해서 ()로 가야 한다).
[…] 논리학은 인간의 뇌 속의 삶이다. 그것은 뇌 바깥의 삶에 동반될 수는 있어도, 그 자체의 힘으로 그것을 이끌 수는 없다. — L.E.J. Brouwer
당신은 어떨지 모르겠지만, 나는 고전 논리의 진리함수적 해석이(그 자체로는 잘 작동하고 옳지만) 여기서 우리가 사용하고 있는 범주론적 틀과 잘 맞지 않는다고 느낀다. 너무 “저수준”이고, 명제의 값들을 조작하는 데 의존한다. 그에 따르면 and 와 or 는 가능한 16개의 이항 논리 연산 중 그저 2개일 뿐이며, 서로 실제로는 연결되어 있지 않다(하지만 우리는 실제로 연결되어 있음을 안다).
이런 이유들과 다른 이유들 때문에, 20세기에 직관주의 논리 라는 완전히 새로운 논리학 학파가 세워졌다. 고전 논리를 집합론 에 기반한 것으로 본다면, 직관주의 논리는 범주론 과 그 관련 이론들에 기반한다고 볼 수 있다. 고전 논리 가 Plato의 이데아론에 기반한다면, 직관주의는 Kant와 Schopenhauer에게서 비롯된 철학적 생각, 즉 우리가 경험하는 세계는 그것에 대한 우리의 지각 방식에 의해 상당 부분 미리 규정된다는 생각에서 출발한다. 따라서 절대적인 진리 기준이 없다면, 명제의 증명은 발견하는 것이 아니라 구성하는 것이 된다.
고전 논리와 직관주의 논리는 출발점부터 서로 갈라진다. 직관주의 논리에 따르면 우리는 어떤 보편적 진리를 발견 하는 것이 아니라 증명을 구성 하고 있으므로, 이중값 원리와는 결별한다. 즉, 직관주의 논리에서는 각 진술이 반드시 참이거나 거짓이다 라고 주장할 근거가 없다. 예를 들어 어떤 진술은 거짓이어서가 아니라, 단지 주어진 논리 체계의 영역 밖에 있기 때문에 증명 불가능할 수도 있다(쌍둥이 소수 추측이 흔히 예로 제시된다).
어쨌든 직관주의 논리는 이중값적이지 않다. 즉, 모든 명제를 참과 거짓으로 환원할 수 없다.
하지만 여전히 있는 것이 하나 있다. 증명이 주어진다는 의미에서 “참”인 명제들, 즉 기본 명제들이다. 그래서 몇 가지 단서와 함께(나중에 보게 될 것이다), 참과 거짓의 이분법은 주어진 명제에 대한 증명의 존재 여부라는 이분법과 비슷하다고 생각할 수 있다. 즉, 그 명제의 증명이 있거나 없거나 둘 중 하나다.
이 이분법은 Brouwer–Heyting–Kolmogorov (BHK) 해석이라고 불리는 것의 핵심이며, 이제 그것을 살펴보자.
다음은 BHK 해석의 정의다(이 해석에서 중심 개념은 명제가 아니라 증명이라는 점에 주의하라).
BHK 논리 해석에 따르면:
- 기본 명제 는 그것에 대한 증명이 주어진 어떤 것이다.
- 논리 연산자 는 여러 증명을 하나의 다른 증명으로 결합하는 구성이다.
- 합성 명제 는 기본 명제들을 논리 연산자로 결합함으로써 그 증명을 구성할 수 있는 어떤 것이다.
원래의 BHK 해석은 특정한 수학 이론에 기반하지 않는다. 여기서는 먼저 그것을 집합론의 언어로 설명하고(조금 뒤에 그것을 버리기 위해서다), 나중에 다른 방식으로 볼 것이다.
명제의 증명이 존재한다는 것은 그 명제가 참이라는 뜻으로 받아들여지므로, and 의 정의는 꽤 간단하다. 다음의 증명은
…그저 의 증명 하나와 의 증명 하나를 담은 쌍 이다. 즉, 두 증명의 집합론적 곱 이다(2장을 보라).
명제가 참인지 거짓인지 결정하는 원리는 기본 명제의 경우와 비슷하다. 와 의 증명 쌍이 존재한다면(즉 두 증명이 모두 존재한다면), 의 증명을 구성할 수 있다(따라서 그것은 “참”이다).
과제 2: 이 경우 or 연산은 무엇이겠는가?
이제 핵심이다. BHK 해석에서 implies 연산은 그저 증명들 사이의 함수 이다. 가 를 함의한다()고 말하는 것은 단지 의 증명을 의 증명으로 바꾸는 화살표가 존재한다는 뜻이다.
하지만 이 증명에 대해 말하려면, 함의 집합, 즉 homomorphism set (집합론에서는 그렇게 부른다)도 필요하다. 이것은 주어진 두 대상 사이의 모든 화살표를 담은 집합으로, 각 화살표마다 하나의 원소를 가진다.
이 집합이 있으면, modus ponens 추론 규칙은 그저 함수 적용 의 과정일 뿐이다. 즉, 의 증명과 함수 하나를 담은 쌍이 있으면, 그 함수를 호출해 의 증명을 얻을 수 있다.
고전 논리 부분에서 우리는 두 명제 와 가 동치라는 것이 가 를 함의하고, 가 를 함의하는 것과 같다는 사실을 증명했다. 그런데 implies 연산이 그저 함수라면, 두 명제가 동치라는 것은 정확히 서로를 다른 쪽으로 보내는 두 함수가 존재하는 경우, 즉 그 명제들을 담은 집합들이 동형 이라는 뜻이다.
(아마도 모든 집합론적 함수가 증명은 아니라는 점을 덧붙여야 할 것이다. 오직 특별히 지정된 일부, 즉 정준 함수들만이 그렇다. 다시 말해 집합론에서는 임의의 두 단원소 집합 사이에 함수와 동형을 만들 수 있지만, 그렇다고 해서 모든 증명이 서로 동등하다는 뜻은 아니다.)
그러므로 BHK 해석에 따르면 가 참이라고 말하는 것은 우리가 의 증명을 가지고 있다는 뜻이다. 충분히 간단하다. 하지만 가 거짓이라는 사실을 표현하는 것은 조금 더 어렵다. 단지 우리가 의 증명을 가지고 있지 않다 고 말하는 것으로는 충분하지 않다(우리가 갖고 있지 않다고 해서 그것이 존재하지 않는다는 뜻은 아니다). 대신, 가 참이라고 주장하는 것이 모순 으로 이어진다는 것을 보여야 한다.
이를 표현하기 위해 직관주의 논리는 상수 를 정의하며, 이것은 False 의 역할을 한다(“바닥값”이라고도 한다). 는 어떤 공식의 증명인데, 그 공식은 아무 증명도 가지지 않는다. 그리고 거짓 명제에 해당하는 것들은, 바닥값이 증명 가능하다고 함의하는 명제들이다(이는 곧 모순이다). 따라서 다음 대신
우리는 다음과 같이 쓸 수 있다.
집합론에서 상수 는 공집합으로 표현된다.
그리고 바닥값과 연결된 명제가 거짓이라는 관찰은, 어떤 명제가 참이라면, 즉 그것의 증명이 존재한다면, 그 명제로부터 공집합으로 가는 함수는 존재할 수 없다는 사실로 표현된다.
그런 함수가 존재할 수 있는 유일한 경우는, 그 명제의 증명 집합도 역시 비어 있을 때뿐이다.
과제 3: 함수의 정의를 찾아보고, 어떤 집합 에서 공집합으로 가는 함수는 존재할 수 없음을 확인하라.
과제 4: 함수의 정의를 찾아보고, 공집합에서 자기 자신으로 가는 함수는 실제로 존재함을 확인하라(사실 공집합에서 임의의 다른 집합으로 가는 함수도 존재한다).
고전 논리의 대안이라는 점 외에도, BHK 해석이 흥미로운 이유는 그것이 논리학에 대한 더 높은 수준의 관점을 제공하기 때문이다. 그리고 그것이야말로 범주론에 기반한 해석을 구성하는 데 필요한 것이다.
이런 더 높은 수준의 논리 해석은 때때로 대수적 해석이라고 불린다. 여기서 대수적 이라는 말은 군이나 순서처럼 범주론으로 표현될 수 있는 모든 구조를 포괄하는 말이다.
그러니 아마 이미 짐작했을 것이다. 대상은 명제이고 사상은 증명이다. 그리고 논리 체계는 하나의 범주로 볼 수 있다.
하지만 늘 그렇듯이 단서가 있다. 모든 범주를 논리 체계로 바꿀 수 있는 것은 아니고, 오직 일부만 가능하다. 그래서 우리의 정리를 마무리하기 위해, 어떤 범주가 “논리적”이기 위해 만족해야 할 기준들을 열거할 것이다. 이 기준들은 그 범주가 모든 올바른 논리 명제에 대응하는 대상을 가지고 있으며, 올바르지 않은 명제에는 대응하는 대상이 없음을 보장해야 한다.
이 기준을 만족하는 범주를 bicartesian closed categories 라고 한다. 하지만 그것들을 바로 설명하기 전에, 우리가 이미 살펴본 비슷하지만 더 단순한 구조, 즉 순서부터 시작하겠다.
과제 5: 논리 증명을 검증하도록 도와주는 “proof assistants”라고 불리는 특별한 종류의 프로그래밍 언어가 있다. 하나 설치해서 어떻게 작동하는지 살펴보라. Coq/Roql용으로는 Mike Nahas의 Coq Tutorial, Lean용으로는 Natural Numbers Game, Agda용으로는 HoTT Game을 추천한다.
과제 6: 우리는 어떤 범주들이 논리를 이룬다는 것을 보이는 데 집중할 것이다. 하지만 그 사이에, 이전 장에서 사용한 범주의 정의를 이용해 모든 논리가 범주를 이룬다는 것을 증명해 보라.
우리는 이미, 어떤 논리 체계와 기본 명제들의 집합이 함께 범주를 이룬다는 것을 보았다.
명제 에서 명제 로 가는 방법이 하나뿐이라고 가정하면(또는 여러 개이지만 그 차이에 관심이 없다면), 논리는 범주일 뿐 아니라 전순서 가 된다. 이때 “더 크다”라는 관계는 “함의한다”를 뜻하므로, 는 이다.
더 나아가, 서로로부터 따라 나오는 명제들(또는 같은 증명으로 증명되는 명제들의 집합)을 동등하다고 본다면, 논리는 진정한 부분 순서 가 된다.
따라서 이것은 Hasse 그림으로 나타낼 수 있으며, 그림에서 가 아래에 있을 때에만 이다.
이것은 범주론의 꽤 특징적인 면이다. 어떤 개념을 범주의 더 제한된 버전(이 경우 순서)에서 먼저 살펴봄으로써 사태를 단순하게 만드는 것이다.
이제 이전에 던졌던 질문을 살펴보자. 정확히 어떤 범주 순서가 논리를 나타내며, 어떤 법칙을 만족해야 논리 체계와 동형인 순서가 되는가? 이 질문에 답하기 위해 논리의 요소들을 다시, 이번에는 순서의 맥락에서 검토해 보자.
이제쯤 여러분도 and 와 or 연산이 논리의 핵심이라는 것을 알아차렸을 것이다(다만 어느 쪽이 빵이고 어느 쪽이 버터인지는 분명치 않다). 앞서 보았듯, BHK 해석에서는 이것들이 집합의 곱 과 합 으로 표현된다. 순서론의 영역에서 대응하는 구조는 meet 와 join 이다(범주론 용어로는 products 와 coproducts ).
논리에서는 임의의 두 명제를 and 또는 or 관계로 결합할 수 있다. 따라서 어떤 순서가 “논리적”이 되려면(즉, 논리 체계를 올바르게 표현하려면) 모든 원소 쌍에 대해 and와 or 연산이 있어야 한다. 공교롭게도 우리는 이런 순서를 이미 뭐라고 부르는지 안다. 그것은 바로 격자 다.
그리고 and 와 or 연산에는 모든 격자에 항상 있는 것은 아닌 중요한 법칙이 하나 있다. 그것은 두 연산 사이의 연결, 즉 서로에 대해 어떻게 분배되는가에 관한 것이다.
이 법칙을 따르는 격자를 분배 격자 라고 한다.
잠깐, 분배 격자에 대해 어디서 들어본 적이 있지 않은가? 이전 장에서 우리는 그것들이 포함 순서 와 동형이라고 말했다. 즉, 주어진 원소들의 모음을 포함하는 집합들의 순서이자, 주어진 원소 집합의 모든 조합 을 포함하는 순서다. 이것이 다시 등장한 것은 우연이 아니다. “논리적” 순서는 포함 순서와 동형이다. 왜 그런지 이해하려면 BHK 해석을 떠올리면 된다. 포함 관계에 참여하는 원소들은 우리의 기본 명제들이다. 그리고 포함들은 이 원소들의 모든 조합인데, or 관계로 결합되어 있다(단순화를 위해 and 연산은 무시하자).
or 와 and 연산(또는 더 일반적으로 coproduct 와 product )은 물론 범주론적으로 쌍대이며, 이것은 그것들을 나타내는 기호와 가 같은 기호를 세로로 뒤집은 것인 이유를 설명해 준다.
심지어 그 기호 자체도 화살표들이 모여드는 방식을 표현한 것처럼 보인다. 아마 실제로는 그렇지 않을 것이다. 이 기호들은 Hasse 그림이 등장하기 훨씬 전부터 사용되었으니, 아마 or 기호는 “uel”(라틴어로 “or”)의 “u”를 뜻하고, and 기호는 그 “u”를 뒤집은 것일 가능성이 크다. 그래도 나는 이 유사성이 흥미롭다.
분배 격자가 논리 체계를 표현하려면, True 와 False 에 대응하는 대상들도 가져야 한다(각각 와 로 쓴다). 그러나 이 대상들의 존재를 요구하려면, 먼저 그것들이 순서론/범주론적 용어로 무엇인지 지정할 방법을 찾아야 한다.
논리학에서 잘 알려진 결과인 폭발 원리 는, 만약 우리가 False 의 증명, 즉 의 증명을 가지고 있다면, 다시 말해 고전 논리의 용어로 “False 가 참이다”라는 진술을 가지고 있다면, 다른 어떤 진술이든 모두 증명할 수 있다고 말한다. 또한 우리는 어떤 참인 진술도 False 를 함의하지 않는다는 것도 안다(사실 직관주의 논리에서는 이것이 참인 진술의 정의다). 이 기준을 바탕으로 보면 False 대상은 다른 대상들과 비교할 때 다음과 같이 생겼을 것이다.
다시 BHK 해석으로 돌아가 보면, 공집합이 이 두 조건을 모두 만족함을 알 수 있다.
반대로 True 의 증명인 는, “True 가 참이다”라는 진술을 표현하지만, 이것은 자명하고 아무 말도 하지 않으므로 거기서 아무것도 따라 나오지 않는다. 그러나 동시에 모든 다른 진술로부터는 따라 나온다.
따라서 True 와 False 는 그냥 우리 순서의 최대 대상과 최소 대상이다(범주론 용어로는 terminal 대상과 initial 대상).
이것은 범주론의 쌍대성 개념의 또 다른 예다. 와 는 서로 쌍대이며, 생각해 보면 아주 자연스럽고, 또 기호를 기억하는 데도 도움이 된다(물론 나 같은 사람이라면, 그것들을 볼 때마다 어느 쪽이 어느 쪽인지 헷갈리지 않게 되기까지 1년쯤 걸릴 것이다).
사실 격자 전체를 거꾸로 뒤집어도(화살표의 방향과 쌍대 개념인 True/False, and/or를 바꾸면) 그 안의 논리는 여전히 유효하다!
그러므로 이제 우리는 우리의 분배 격자가 논리를 표현하기 위해서는 bounded 해야 한다는 것을 안다. 즉, True 와 False 의 역할을 하는 최대 원소와 최소 원소를 가져야 한다. 말했듯이, 모든 격자에는 명제들이 서로를 함의하는 표현(즉 화살표)이 있다. 하지만 그것이 진정한 논리 체계를 표현하려면 함의 대상 도 가져야 한다. 즉, 각 대상 쌍 와 에 대해, 논리의 모든 공리가 따르도록 하는 어떤 유일한 대상 을 지정하는 규칙이 있어야 한다.
우리는 이 대상을 다른 연산들을 설명했던 것과 같은 방식으로 설명할 것이다. 즉, 가 참여하는 대상과 화살표들의 구조를 정의함으로써 설명할 것이다. 그리고 이 구조는 사실 우리가 가장 좋아하는 추론 규칙인 modus ponens 의 범주론적 환생이다.
Modus ponens는 implies 연산의 본질이다. 그리고 그 안에 들어가는 연산들(and 와 implies)이 우리의 격자에서 어떻게 표현되는지 이미 알고 있으므로, 이를 곧바로 정의로 사용할 수 있다. 즉, 라는 대상은 modus ponens 규칙이 성립하는 대상이라고 말하면 된다.
함의 대상은 대상 와 와 관련되어 있으면서 이 성립하도록 하는 대상이다.
하지만 이 정의는 완전하지 않다. 왜냐하면 늘 그렇듯이 가 이 식을 만족하는 유일한 대상은 아니기 때문이다. 예를 들어 집합 도 그런 대상 중 하나이고, 도 그렇다.
그렇다면 이 모든 “가짜” 공식들 가운데서 진짜 공식을 어떻게 골라낼까? 범주론적 곱 의 정의(또는 순서에서 그에 해당하는 meet 연산의 정의)를 기억한다면, 어디로 가는지 이미 알 것이다. 우리는 가 의 상한 limit 임을 알아본다. 그래서 와 안에서 자리에 들어갈 수 있는 다른 모든 가짜 공식들은 그 아래에 놓인다. 이 관계는 여러 방식으로 설명할 수 있다.
이제 관계를 표현하는 가장 좋은 방식을 고른 뒤(모두 동치다), 최종 정의를 제시할 준비가 되었다.
함의 대상(또는 exponential object 나 internal homomorphism object 라고도 한다)은 대상 와 와 관련되어 이 성립하도록 하는 대상들 가운데 가장 위에 있는 대상이다.
이 함의 대상의 존재가 어떤 순서/격자가 논리를 표현하기 위한 마지막 조건이다.
이 함의 대상의 정의는 특히 직관주의 논리에 대해 유효하다. 고전 논리에서는 의 정의가 더 단순하다. 배중률 때문에, 그것은 를 표현하는 또 다른 방식일 뿐이다.
어떤 와 에 대해 역할을 하는 대상이 여러 개 있을 수도 있지만, 그것들은 서로 동형일 것이다. 즉, meet와 join처럼 함의 대상도 유일한 동형까지 정의된다.
앞서 if and only if 연산은 implies 로 정의될 수 있으며, 즉 는 와 동치라는 것을 보았다.
범주론적 논리에서도 비슷한 것이 있다. 두 명제가 서로 연결되어 있을 때, 특히 순서의 맥락에서 말하면, 그것들은 동형이라고 한다.
지금까지 많은 이야기를 했으니, 이제 정의를 정리할 시간이다. 우리는 직관주의 논리가 True 와 False 값, 그리고 and, or, implies 연산으로 이루어진다는 것을 보았다.
앞서 말했듯, 이런 조건을 모두 만족하는 “논리적” 순서에는 특별한 이름이 있다. 그것들은 Heyting algebras 라고 불린다.
join/meet, 최대/최소 대상, 그리고 함의 대상을 갖는 순서를 Heyting algebra라고 부른다.
그리고 우리는 이렇게 말한다.
직관주의 논리의 논리 체계는 Heyting algebra로 볼 수 있다. “and”와 “or” 연산은 join/meet이고, “True”와 “False” 값은 최대 및 최소 대상이며, 함의 연산은 exponential object이다.
그런데 격자는 고전 논리 의 법칙도 따를 수 있다. 그러려면 bounded 이고 distributive 해야 하며, 거기에 더해 complemented 해야 한다. 즉 각 명제 에 대해 유일한 명제 가 존재해서 이고 가 되어야 한다. 이런 격자를 boolean algebras 라고 부른다.
위 정의는 thin 범주(순서)로 서술했지만, 용어만 조금 조정하면 다른 모든 범주에도 그대로 유효하다.
products/coproducts, initial/terminal objects, 그리고 exponential objects를 가지는 범주는 Bicartesian closed이다.
그리고
직관주의 논리의 논리 체계는 Bicartesian Closed Category로 볼 수 있다. “and”와 “or” 연산은 product/coproducts이고, “True”와 “False” 값은 initial/terminal objects이며, 함의 연산은 exponential object이다.
이전 절에서는 몇 가지 정의를 보았다. 여기서는 범주론적 논리를 사용해 실제로 몇 가지 결과를 증명함으로써, 그것들이 정말로 논리 개념을 올바르게 포착하고 있음을 확인해 보자.
가장 위의 대상(True 값의 역할을 하는 대상)과 여러분이 떠올릴 수 있는 임의의 다른 대상의 join(또는 최소 상계)은… 자기 자신이다(또는 그것과 동형인 어떤 것인데, 앞서 말했듯 그것은 같은 것이다). 이것은 join이 두 대상 모두보다 크거나 같아야 하고, 자기 자신보다 크거나 같은 다른 대상이 자기 자신 말고는 없다는 사실에서 자명하게 따라온다. 이는 단지 (다른 모든 대상과 마찬가지로) 이 자기 자신과 같고, 정의상 그것보다 큰 대상이 없기 때문이다.
이것은 논리 명제 와 대응하며, 즉 그것이 참이라는 뜻이다. 따라서 위 관찰은 그 명제의 증명이 된다(진리표에 대한 대안이다).
과제 7: False의 경우인 쌍대 상황을 생각해 보라. 논리적으로 무엇을 뜻하는가?
위에서 우리는 임의의 대상과 top 대상의 join이 top 대상 자체라는 것을 보았다. 그런데 이런 상황은 두 번째 대상이 일 때만 일어나는가? 첫 번째 대상보다 더 위에 있는 임의의 다른 대상을 넣어도 똑같지 않을까?
대답은 “그렇다”이다. 두 대상의 join을 찾는다는 것은 최소 상계, 즉 둘 다 위에 놓이면서 그중 가장 아래 에 있는 대상을 찾는 것이다. 그러므로 두 대상 중 하나가 다른 하나보다 위에 있을 때마다, 그들의 join은 (그 더 높은 대상과 동형인) 바로 그 더 높은 대상이 된다.
즉, 만약 이면,
함의의 첫 번째 예로, 공식을 잡고 와 가 같은 대상인 경우를 보자. 우리는 (우리 경우에는 )가 그 공식이 요구하는 기준을 만족하는 가장 위의 대상이라고 했다. 그런데 이 경우 그 공식은 임의의 에 대해 성립한다(왜냐하면 이것은 로 계산되고, 그것은 항상 참이기 때문이다). 즉 그 조건을 만족하는 가장 위의 대상은… 존재하는 가장 위의 대상, 곧 (그것과 동형인) 이다.
이것이 말이 되는가? 물론이다. 사실 우리는 방금 논리학의 가장 유명한 법칙 중 하나(Aristotle에 따른 동일률), 즉 가 항상 참이라는 것, 또는 모든 것은 자기 자신을 함의한다는 것을 증명한 것이다.
그리고 어떤 모델에서든 가 를 함의한다면, 즉 이면(의미론적 귀결), 무슨 일이 일어날까? 이 경우 는 우리의 Hasse 그림에서 아래에 있게 된다(예를 들어 는 파란 공, 는 주황 공이다). 그러면 상황은 앞의 경우와 다소 비슷해진다. 는 가 무엇이든 참이 된다(왜냐하면 자체만으로 이미 를 함의하기 때문이다). 따라서 는 다시 대상에 대응한다.
이 역시 논리학에서 잘 알려진 결과다(내가 틀리지 않았다면 일종의 연역 정리일 것이다). 즉, 만약 이면, 진술 는 항상 참이다.
논리 격자가 어떻게 작동하는지 이해하는 가장 좋은 방법은 직접 하나 만들어 보는 것일지도 모른다.
어쨌든 논리 격자를 만든다는 것은 몇몇 기본 명제를 고르고, 그것들 사이의 연결을 그래프로 그리는 것을 뜻한다. 먼저 작업하고 싶은 기본 명제들을 고른다. 이것들은 문제 영역에 의존하는 진술들이다(또는 이 경우에는 그냥 우리의 색 취향에 따른다).
그다음 우리가 선택한 논리의 종류(직관주의, boolean)에 따라 합성 명제들을 그리기 시작한다. 모든 와 에 대해 , 가 있어야 한다.
그다음 모든 와 에 대해 명제 도 만들어야 하며, 그러면 우리의 명제 목록은 무한히 늘어나게 된다(덧붙이자면 이런 그림을 그리는 것은 정말 어렵고, 각 명제가 어느 자리에 있어야 하는지 나는 결코 완전히 확신할 수 없다. 그러니 오류를 발견하면 꼭 알려 달라. Donald Knuth처럼 100$ 수표를 보내 줄 수는 있지만, 나는 가난하니 부디 현금화하지 않겠다고 약속해야 한다).
휴, 길었다. 하지만 그럴 가치가 있다. 이것이 끝나면 우리는 참일 수 있는 모든 가능한 명제들 의 목록을 갖게 되고, 어떤 명제에서 어떤 명제가 따라 나오는지는 그 명제에서 나오는 화살표 경로를 따라가기만 하면 알 수 있게 된다.
예를 들어 명제 가 참이라는 것을 알게 되면, 그것은 와 가 각자 참이라는 것도 뜻하고(그리고 그것은 다시 , 등등이 참이라는 것을 뜻한다).
일반적으로 직관주의 논리를 한다는 것은 이런 것이다. 즉, 이미 알고 있는 것들에서 시작해서, 우리가 증명하고 싶은 것들로 이어지는 경로를 찾는다(또는 관점에 따라, 이미 가지고 있는 증명들을 조작하여 증명을 구성한다). 단 한 가지 할 수 없는 것은(특히 직관주의 논리에서는), 어떤 사실이 우리의 경로에서 도달될 수 없다는 것, 즉 공리들로부터 증명될 수 없다는 것을 증명하는 일이다(“부정은 증명할 수 없다”).
