증명과 의미론적 태블로

1. 증명이란 무엇인가

논증이란 어떤 결론이 몇 개의 전제로부터 따라 나온다는 주장입니다. 증명은 그 주장을 매듭짓는 것, 곧 누구나 한 줄씩 읽고 수긍할 수 있는 유한하고 검사 가능한 대상이며, 당신의 말을 믿을 필요가 없습니다. 증명의 요점은 설득하는 데 있지 않습니다. 좋은 연설도 설득합니다. 요점은 그 안의 모든 단계가 달리 될 수 없었다는 데 있습니다.

이는 들리는 것보다 엄격한 요구입니다. 「비가 오니 땅이 젖었다」는 합당한 말이지만, 비와 땅에 대해 당신이 아는 바에 기대고 있습니다. 형식논리는 그것을 걷어내고 더 좁은 물음을 던집니다. 오직 문장의 형태만 놓고 볼 때, 전제가 참이고 결론이 거짓인 길이 하나라도 있는가? 하나도 없다면 논증은 타당하며, 증명은 왜 그런 길이 없는지에 대한 기록입니다.

이 안내서는 그 기록을 만드는 한 가지 방법, 곧 진리나무라고도 불리는 의미론적 태블로의 방법을 다룹니다. 계산기에 논증을 입력할 때마다 이 사이트가 쓰는 방법이 바로 이것이며, 한 번만 따라가 보면 펜 한 자루로 종이 위에서 논증을 검사할 수 있게 됩니다.

2. 타당함, 그리고 그것을 아는 법

논증을 귀결 기호와 함께 씁니다. 전제는 왼쪽, 결론은 오른쪽입니다. p → q, ¬q ⊨ ¬p 라는 주장은 조건문과 그 후건의 부정으로부터 전건의 부정이 따라 나온다는 말입니다. 귀결 기호는 또 하나의 연결사가 아닙니다. 그것은 양옆의 논리식에 관한 주장이며, 옳거나 그르거나 둘 중 하나입니다.

타당성의 정의는 검사 방법을 곧바로 가리킵니다. 변수에 참과 거짓을 배정하는 모든 경우를 훑어보고, 그중에 전제를 모두 참으로 만들고 결론을 거짓으로 만드는 것이 있는지 보면 됩니다. 진리표가 하는 일이 바로 그것이고, 변수가 둘이나 셋이면 아무 문제 없습니다. 문제는 표가 2ⁿ으로 불어난다는 점입니다. 변수 열 개면 천 줄, 스무 개면 백만 줄이 필요하고, 게다가 표는 어느 줄이 중요했는지 아무 말도 해 주지 않습니다.

타블로는 같은 물음을 반대쪽 끝에서 공략합니다. 모든 가능성을 늘어놓고 나쁜 것을 찾는 대신, 나쁜 것이 있다고 가정하고 그것을 지어 보려 합니다. 그 시도가 갈 수 있는 모든 경로에서 모순으로 무너진다면 그런 배정은 존재하지 않으며 논증은 타당합니다. 시도가 성공한다면 지어진 것이 곧 그대로 읽어 낼 수 있는 반례입니다.

3. 타블로 방법

타블로는 부호가 붙은 논리식의 나무입니다. 각 줄은 앞에 T나 F가 붙은 논리식이고, 부호는 그 가지가 해당 논리식에 대해 무엇을 가정하는지를 말해 줍니다. 진리값이 무엇인지가 아니라, 논증이 무너지려면 무엇이어야 하는지입니다. 방법 전체는 네 단계입니다.

1. 각 전제를 T와 함께 씁니다. 논증의 전제가 모두 성립한다고 가정하는 것입니다.
2. 결론을 F와 함께 씁니다. 그럼에도 결론이 무너진다고 가정하는 것이며, 이것이 반박하려는 가정입니다.
3. 아직 원자가 아닌 줄을 하나 골라 그 주 연결사와 부호에 해당하는 규칙을 적용하고, 규칙이 내놓는 것을 그 줄을 지나는 모든 가지의 끝에 덧붙입니다.
4. 같은 논리식 A에 대해 T A와 F A를 함께 가지게 되는 즉시 그 가지를 닫습니다. 모든 가지가 닫혔거나 분해할 줄이 남지 않았을 때 멈춥니다.

이 되풀이에는 재치도 전략의 선택도 필요하지 않습니다. 각 줄에 해당하는 규칙은 정확히 하나이고, 어떤 순서로 적용하든 같은 판정이 나옵니다. 그래서 기계가 할 수 있고, 그래서 기계가 낸 결과를 믿을 수 있습니다.

4. 규칙

연결사마다 부호마다 규칙이 하나씩, 모두 열 개입니다. 규칙은 두 갈래로 나뉘는데, 그 차이야말로 타블로가 목록이 아니라 나무인 이유의 전부입니다. α 규칙은 여러 가지가 함께 성립해야 한다고 말하므로 결과를 가지를 따라 아래로 쌓습니다. β 규칙은 둘 중 하나가 성립해야 한다고 말하므로 가지를 둘로 쪼개고 각 경우를 제 갈 길로 보냅니다.

모든 규칙은 그 연결사의 진리 조건을 거꾸로 읽은 것에 지나지 않습니다. 연언은 양쪽이 모두 참일 때만 참이므로 T (A ∧ B)는 T A와 T B를 쌓습니다. 연언은 적어도 한쪽이 거짓이면 거짓이지만 논리식은 어느 쪽인지 말해 주지 않으므로 F (A ∧ B)는 둘 다 시도해야 합니다. 그래서 갈라집니다. 선언에서는 같은 비대칭이 반대 방향으로 작동하고, 조건문이 거짓이라는 것은 전건이 성립하고 후건이 무너졌다는 뜻, 곧 함축이 깨지는 유일한 경우입니다.

규칙이 결코 하지 않는 일에 주목하십시오. 규칙은 논리식을 지어내지 않습니다. 규칙이 내놓는 것은 모두 그것이 나온 줄의 한 조각입니다. 이 성질, 곧 부분논리식 성질이 이 방법을 유한하게 만들며, 아래에서 다시 다룹니다.

5. 가지를 닫기

가지는 하나의 추론 줄기입니다. 뿌리에서 잎까지 읽으면 온전한 가정 한 벌이 나옵니다. 가지가 닫히는 것은 그 가정들이 정면으로 모순될 때, 곧 같은 논리식에 대해 T A와 F A를 함께 지니고 있을 때입니다. A가 얼마나 복잡한지, 두 줄이 얼마나 떨어져 있는지는 상관없습니다. 어떤 논리식이 참이면서 동시에 거짓이기를 가지가 요구한다면, 그것을 만족시키는 것은 없습니다.

닫힌 가지에는 ×를 붙이고 그것을 닫은 두 줄을 적은 뒤, 그 가지 작업을 그만둡니다. 애초에 불가능했던 가정에서 더 배울 것은 없습니다.

모든 가지가 닫히면 타블로가 닫힌 것이고, 그것이 곧 증명입니다. 출발한 가정, 곧 전제는 모두 참이고 결론은 거짓이라는 가정이 갈 수 있는 모든 경로에서 모순에 이른다는 것을 보여 주기 때문입니다. 남은 경로가 없으므로 그런 배정은 존재하지 않고 논증은 타당합니다. 이것은 어떤 경우도 놓칠 수 없도록 펼쳐 놓은 귀류법입니다.

6. 한 줄씩 따라가는 증명

모두스 톨렌스, p → q, ¬q ⊨ ¬p를 봅시다. 1번과 2번 줄은 참으로 가정한 전제입니다. 3번 줄은 거짓으로 가정한 결론인데, 결론이 ¬p이므로 그것을 거짓으로 가정하는 일은 p를 참으로 가정하는 일이고, 5번 줄이 그것을 적어 둡니다. 4번 줄은 2번 줄에 부정 규칙을 적용한 결과로, ¬q가 참이면 q는 거짓입니다. 연결사가 남은 줄은 1번 줄의 조건문뿐이고 이는 β 규칙이므로 나무가 갈라집니다.

왼쪽 가지는 전건이 무너졌기 때문에 조건문이 성립했다고 가정합니다. 그러나 5번 줄에서 이미 p가 참이므로 가지는 스스로 모순되어 닫힙니다. 오른쪽 가지는 후건이 참이었기 때문에 성립했다고 가정합니다. 그러나 4번 줄에서 이미 q가 거짓이므로 이 가지도 닫힙니다.

두 가지가 모두 닫혔으므로 ¬p가 거짓인 채로 p → q와 ¬q를 참으로 만들 방법은 없습니다. 논증은 타당하고, 그 이유가 바로 이 나무입니다. 증명이 비도 땅도, p와 q가 무엇을 가리키는지도 전혀 언급하지 않았음에 주목하십시오. 그럴 필요가 없었습니다.

7. 가지가 열린 채 남을 때

모든 논증이 타당한 것은 아니며, 바로 여기서 이 방법이 값을 합니다. 어떤 가지를 더 분해할 것이 없을 때까지, 곧 원자와 부정된 원자만 남을 때까지 밀고 나갔는데도 닫히지 않았다면, 그 가지는 포화되었고 열려 있습니다. 너무 일찍 멈춰서 닫히지 않은 것이 아닙니다. 더 시도할 것이 없습니다.

열린 가지는 「타당하지 않음」이라는 판정 이상입니다. 그 원자들의 부호를 읽으면 배정이 나옵니다. T가 붙은 원자는 참, F가 붙은 원자는 거짓입니다. 이 배정은 전제를 모두 참으로, 결론을 거짓으로 만들며, 그것이 바로 반례입니다. 논리학자들은 이를 반모형이라 부르며, 이는 「왜 아닌가?」에 대한 구체적인 답이지 거절이 아닙니다.

후건 긍정, p → q, q ⊨ p가 교과서적인 경우입니다. 그 타블로는 p가 거짓이고 q가 참인 가지를 열어 둡니다. 조건문이 성립하고 후건도 성립하는데 전건은 성립하지 않는 상황입니다. 이 하나의 배정만으로 논증은 반박됩니다.

8. 왜 언제나 끝나는가

모든 규칙은 논리식을 그 자신의 부분논리식으로 바꾸고, 부분논리식은 그것이 나온 논리식보다 반드시 짧습니다. 따라서 어떤 가지도 끝없이 자랄 수 없습니다. 각 단계는 원래 논증의 조각들로 이루어진 유한한 사다리를 내려가고, 그 사다리에는 바닥이 있습니다. 마침내 가지의 모든 줄은 원자이거나 원자의 부정이 되고, 더 할 일이 없어집니다.

이는 희망이 아니라 실제 보장입니다. 이 방법이 명제논리의 결정 절차라는 뜻입니다. 어떤 논증에 돌리든 멈추며, 닫힌 나무나 열린 가지 중 하나를 내놓지 어깨를 으쓱하고 끝나지 않습니다. 이 사이트의 증명기는 그 위에 노드 상한을 두지만, 병적인 논리식이 브라우저 탭을 소진하는 것을 막기 위한 것일 뿐이며, 수학 자체에는 그런 한계가 필요 없습니다.

9. 다른 증명 체계들

타블로는 여러 증명 체계 가운데 하나이며, 반박의 모양을 한 체계입니다. 실패를 배제하는 방식으로 작동합니다. 자연연역은 반대로 가서 모두스 포넨스나 조건 증명 같은 규칙으로 전제에서 결론을 앞으로 쌓아 올리며, 수학자가 산문으로 논증하는 방식에 훨씬 가깝게 읽힙니다. 자연연역 증명은 대개 더 짧지만, 그것을 찾아내는 데는 대개 더 많은 착상이 듭니다.

시퀀트 계산은 귀결 기호 자체를 형식화하고 귀결 주장을 대상으로 다루므로, 증명에 관한 것을 증명하려 할 때 즐겨 쓰는 도구가 됩니다. 분해 원리는 모든 것을 절과 단 하나의 규칙으로 환원합니다. 읽기에는 멋이 없지만 실행은 대단히 빠르며, 대부분의 자동 증명기와 SAT 해결기가 그 위에 지어져 있습니다.

어떤 명제 논증이 타당한지에 대해서는 모두 일치합니다. 다른 것은 증명의 생김새와, 무엇을 쉽게 찾을 수 있는가입니다. 배우기에 가장 친절한 것은 타블로입니다. 실패한 증명이 막다른 길이 아니라 반례를 건네주기 때문입니다.

10. 연습

이 방법을 익히는 가장 빠른 길은 직접 돌려 보는 것입니다. ⊨, ⊢ 또는 |=를 써서 계산기에 논증을 입력하면 진리표 옆에 타블로가 그려지므로 나무와 줄들을 맞대어 볼 수 있습니다. 그런 다음 답을 보기 전에 몇 개의 증명을 종이 위에서 풀어 보십시오.