1/0 = 0

면책조항 2024-12-02

이 푸념이 다시 (다시 (또)) 바이럴이 되는 김에, 몇 가지 면책조항을 붙인다:

1. 이 글은 못생긴 트위터 싸움에서 “”“이기기”“” 위해 6년 전에 썼다. 촉발한 트윗을 익명화해 둬서 다행이고, 이 일로 아직도 곤욕을 치르는 사람이 나 혼자였으면 좋겠다.
2. 핵심 흥미거리— 1/0=0을 정의하는 것이 왜 수학적으로 타당하며 많은 정리 증명기가 그 정의를 쓰는지—는 Xena 프로젝트 FAQ가 더 잘 다룬다.
3. “정리 증명기에 좋다”가 “프로그래밍 언어에 좋다”와 같지는 않다.
4. 수학자 99%+는 “역곱셈”으로서의 일상적 나눗셈 정의를 써서 전체 수학의 99%+를 수행한다. “어디서나 정의된” 나눗셈은 주로 논리학자들과 일부 대수학자에게 흥미롭다.
5. 무엇보다 흥미로운 것은, 0으로 나누기를 정의하면 모든 것이 망가질 것처럼 보이지만 실제로는 일관적이며 다른 수학에 대한 통찰을 준다는 점이다. 수학은 주입식 암기가 아니다: 유동적이고, 놀이 같으며, 즐겁다.

---

트윗 하나 보시라:

Pony가 여기서 올바른 선택을 하는지 전혀 모르겠다. 나는 Pony를 모른다. 배우고 싶은 마음도 없다.1 하지만 이 트윗은 두 가지 이유로 나를 불편하게 했다:

1. 꽤 잘난 체한다. 나는 프로그래밍에 대해 강한 의견을 가지고 있지만, 내가 지키려 애쓰는 규칙 하나는 _다른 프로그래머를 비웃지 말 것_이다.2 프로그래밍은 너무 거대하고 나는 모든 것을 이해하기엔 너무 작다. 반대하는 건 괜찮고, 왜 틀렸는지 설명하는 것도 괜찮지만, 비웃는 것은 괜찮지 않다.
2. Pony가 수학적으로 틀렸다고 말한다. 이것은 객관적으로 거짓이다.

나는 1/0 = 0이 수학적으로 건전함을 설명하는 글을 트윗했다. 어떤 사람들은 동의했고, 어떤 사람들은 단서와 함께 동의했으며, 어떤 사람들은 헛소리라고 했다. 몇몇은 내가 진짜 수학을 모르는 게 분명하다고, 진짜 수학자라면 그런 실수를 하지 않는다고 말했다.

그래서 이 글에서 1/0 = 0이라고 말하는 것이 왜 일관적인지, 흔한 반론들이 왜 통하지 않는지, 그리고 진짜 수학자들이 뭐라고 하는지 명확하고 형식적으로 정리하고자 한다. 미리 경고하자면, 이 글은 내 평소 글보다 수학적으로 조금 더 밀도 높을 것이다. 최대한 명료하게 쓰려 했지만, 뭐, 수학이니까.

일관성

먼저 “일관성(consistency)”이 무엇을 뜻하는지 설명해야 한다. 형식 체계가 건전하다는 것은 오직 참인 명제만을 증명할 수 있다는 뜻이다. 1/0 = 0이 비건전하다고 말하는 것은, 1/0 ≠ 0을 증명할 수 있거나, 1/0 = 0을 가정하면 거짓을 증명할 수 있다는 뜻이다. 사실 이 둘은 동치지만, 설명을 위해 구분해서 다루는 편이 유용하다.

다음으로 “나눗셈”이 무엇인지 설명해야 한다. 그런데 그러려면 **체(field)**를 소개해야 한다.

체

체는 원소들의 집합 S와 그 위의 덧셈 연산(+)과 곱셈 연산(*)이 다음 성질들을 만족하는 구조다:

1. 두 연산에 대해 집합이 닫혀 있다. 만약 x와 y가 S의 원소라면, x + y와 x * y도 S의 원소다.
2. 두 연산은 교환법칙을 만족한다. a + b = b + a, a * b = b * a.
3. 두 연산은 결합법칙을 만족한다. a + (b + c) = (a + b) + c, a * (b * c) = (a * b) * c.
4. 곱셈은 분배적이다. a * (b + c) = a * b + a * c.
5. 덧셈 항등원 0이 존재하여 a + 0 = a.
6. 곱셈 항등원 1이 존재하여 a * 1 = a.
7. 두 항등원은 서로 다른 원소다. 1 ≠ 0.
8. 모든 원소는 덧셈에 대한 역원 -a를 가져서 a + (-a) = 0.
9. 0을 제외한 모든 원소는 곱셈에 대한 역원 a⁻를 가져서 a * a⁻ = 1.

이것이 체의 모든 규칙이다. S, +, *를 어떻게 정의하든 상관없지만, 위 규칙들을 모두 따라야 한다. 실수 집합과 우리가 익숙한 덧셈·곱셈은 체를 이룬다. 이것이 시스템의 성질을 밝혀낼 토대를 준다. 정리를 증명하려면 S/+/*의 정의, 체의 정의, 그리고 우리가 가진 공리만으로 도출해야 한다.3 예를 들어 모든 a에 대해 a * 0 = 0임을 증명할 수 있다:

1. 덧셈 항등원에 의해 0 + 0 = 0, 따라서 a * 0 = a * (0 + 0)
2. 분배법칙에 의해 a * (0 + 0) = a * 0 + a * 0
3. 덧셈 역원 성질에 의해 - (a * 0) + (a * 0) = 0이 되도록 하는 어떤 - (a * 0)가 존재한다.
4. (1)과 (2)를 합치면 a * 0 = a * 0 + a * 0.
5. (3)과 (4)를 합치면 - (a * 0) + (a * 0) = - (a * 0) + a * 0 + a * 0.
6. (5)를 계산하면 0 = a * 0. 증명 끝.

이 정리를 얻었으니, 이를 이용해 다른 정리들도 증명할 수 있다. 이를 바탕으로 0의 곱셈 역원이 없음을 곧바로 보일 수 있다:

1. 0이 곱셈 역원 0⁻을 가진다고 하면 0 * 0⁻ = 1.
2. 모든 실수 a에 대해 a * 0 = 0.
3. 1 ≠ 0이므로 0에는 곱셈 역원이 없다.

좋다, 이제 실수에서의 나눗셈을 이야기하자.

나눗셈

체의 정의에는 나눗셈이 포함되어 있지 않고, 우리의 덧셈·곱셈 정의에도 없다. 이는 우리가 나눗셈을 원하는 대로 정의할 수 있다는 뜻이다. 우리는 직관을 대체로 따르면서 건전한 방식으로 정의하고 싶다. _대체로_라고 한 이유는 우리의 직관이 일반화되지 않기 때문이다. 예를 들어, 우리는 직관적으로 a * b를 “a를 b번 더한 것”으로 생각한다. 그렇다면 -1 * π는 뭔가? π번 더한다는 게 무슨 뜻인가? 나눗셈에 “이상함”이 하나도 없으면 좋겠지만, 그렇게 보장하면 수학을 심각하게 제약하게 된다.

나눗셈의 직관적 정의는 역원에 의한 곱셈이다. a/2 = a * 2⁻. 이 정의 아래에서, 우리가 익숙한 나눗셈의 성질들을 증명으로 얻을 수 있다. 예를 들어,

• 정리: a/a = 1. 증명: a/a = a * a⁻ = 1.
• 정리: a * (b/c) = b * (a/c). 증명: a * (b/c) = a * (b * c⁻). 곱셈이 교환적이고 결합적이므로, 이를 재배열하여 b * (a * c⁻) = b * (a/c)를 얻는다.

모두 훌륭하지만, 한 가지 문제가 있다: 0에는 곱셈 역원이 없다. 두 증명 모두 0에서는 무효다. 0/0을 쓰면 0 * 0⁻가 되어, 잘못된 식이 된다. 따라서 a/a = 1을 증명할 수 없다. 다만 더 약한 것을 증명할 수 있다:

• 정리: IF a ≠ 0, THEN a/a = 1. 증명: 동일.
• 정리: IF c ≠ 0, THEN a * (b/c) = b * (a/c). 증명: 동일.

이는 역도 성립하지 않는다: 0/0 ≠ 1이 따라오지 않는다. 우리가 아는 것은 이 정리로는 0/0 = 1을 증명할 수 없다는 것뿐이다. 그러니 0/0 ≠ 1이라고 할 수 없다. 우리가 나눗셈을 역원 곱셈으로 정의했고 0에는 역원이 없으므로, 우리의 나눗셈 정의는 0으로 나누는 경우를 다루지 않는다. 아무것도 말해주지 않으며, 말하자면 “정의되지 않음”으로 남는다.

이런 형태의 나눗셈은 0에서 정의되지 않으므로, 실수 위에서 부분 함수가 된다: 정의역의 어떤 값에 대해 값을 지정하지 않았다. 실용적으로는 괜찮다: 우리는 1/0을 불가능한 연산으로 여기는 데 익숙하다. 하지만 이상한 결과도 따른다: 모든 것은 자기 자신과 같다라는 공리가 있다. 그렇다면 1/0 = 1/0인가? 이게 우스꽝스럽다고 말한다면 a = a를 더 이상 갖지 못한다! 설령 그게 괜찮다 해도, TRUE \/ (1/0 = 1/0) 같은 명제는 어떤가? 두 번째 절이 무엇이든 상관없이 이 명제는 참이어야 한다. 그런데 배중률에 따르면, 우리는 두 번째 절이 참이거나 거짓이라고 말해야만 한다. 수학과 논리를 형식화할 때는 1/0을 썼을 때 무슨 일이 벌어지는지 어떤 방식으로든 다뤄야 한다. 그래서 수학자들이 보통 할 수 있는 일은 세 가지다:4

• “안 됨, 미안, 1/0을 쓰는 것조차 허용 안 함, 값도 못 줌”이라고 한다. 우리가 일상에서 하는 방식이고, Agda와 Idris가 나눗셈을 다루는 방식이다.
• 실수가 아닌 값을 하나 고른다. 예컨대 “정의되지 않음”이나 무한대 같은 것, 그리고 x/0 = <뭐든지>라고 한다. 리만 구를 쓰는 일부 수학자들이 이렇게 한다.
• 19 같은 실수를 하나 골라서 x/0 = 19라고 할 수도 있다. Isabelle, Lean, Coq가 이렇게 한다.

모두 장단점이 있다. 1/0 같은 식을 금지하면 앞서 본 두통거리들이 있다. “정의되지 않음” 값을 쓰면, 나눗셈이 더 이상 실수 위에서 닫혀 있지 않다. 마지막 경우에는 모두의 나눗셈 직관을 폭파한다. 하지만 모두 건전하다. 우리의 원래 나눗셈 개념은 0으로 나누기에 대해 아무 말도 하지 않으므로, 아무 것도 배제하지 않는다. 이런 확장들로 모순이 생기지 않는다.

논란은 마지막 경우에 집중되므로 그것에 초점을 맞추자. 다음과 같이 나눗셈을 정의하겠다: IF b = 0 THEN a/b = 1 ELSE a/b = a * b⁻.

여기서 강조해야 할 점: 이것이 0의 역원을 주는 것은 아니다. 1/0은 0⁻이 아니다. 그래서 0/0 = 1이지만 0 * 1/0 = 0이다. 분모가 0이 아닐 때만 나눗셈이 “역원 곱셈”이다. 우리가 한 것은 0으로 나누기만 특수 처리했을 뿐이고 그 외는 건드리지 않았다. 그리고 그렇게 해도 이 나눗셈 정의 아래에서는 1/0 = 1로부터 거짓을 증명할 수 없으므로 수학적으로 일관적이다.

반론들

여기서 많은 사람이 반박했다. 그들은 1/0 = 1이라는 사실로부터 보통 1 = 0 같은 거짓을 증명하려 한다. 하지만 이 증명들은 건전하지 않다. 왜 그런지 보기 위해, 몇 가지 예시 증명을 파고들어 어디서 무너지는지 보자.

흔한 논증 하나:

1. 1/0 = 1
2. 1/0 * 0 = 1 * 0
3. 1 * 0/0 = 0
4. 1 = 0

문제는 (3)단계에 있다: 우리의 나눗셈 정리는 c ≠ 0일 때만 유효하므로, 1/0 * 0에서 1 * 0/0으로 갈 수 없다. “분모는 0이 아니다”라는 조건이 우리의 정의를 모순으로 몰고 가는 것을 막아준다.

사람들이 걸려 넘어지는 지점이 이것이다. 그들은 우리가 나눗셈 정리에 분모≠0 조건을 붙여야 하는 이유가 x/0이 정의되지 않았기 때문이라고 가정한다. “x/0이 어떤 값이라면, 정리도 c=0까지 확장되어야지.” 틀렸다. 문제는 1/0이 정의되지 않았다는 게 아니었다. 우리의 증명이 곱셈 역원을 사용한다는 점이 문제였고, 0에는 곱셈 역원이 없다. 수정된 나눗셈 정의 아래에서도 여전히 0⁻은 없고, 따라서 0으로 나눌 때 우리의 증명은 여전히 통하지 않는다. 조건이 여전히 필요하다. 그러니 a * (b / 0) = b * (a / 0)는 _정리_가 아니다.

명확히 하자면, 이것이 둘이 _달라야 한다_는 뜻도 아니다! 우리가 아는 것은 이 정리를 써서 둘이 _같다_고 주장할 수 없다는 것뿐이다. 위 “1 = 0” 증명은 그 정리를 썼으므로, 건전하지 않다.

거의 모든 반론은 정확히 같은 실수를 한다: 1/0이 이제 정의되었으니 어떤 0⁻이 있고 우리의 정리들이 일반화될 거라고 가정한다. 하지만 그렇지 않다.

또 다른 흔한 반론은 1/0 = 1이라면 곱셈 역원이 더 이상 유일하지 않다는 것이다: 2/2 = 1인데 2/0 = 1도 되어 2가 역원을 둘 갖게 된다는 주장이다. 이것도 다시 원인과 결과를 혼동한다. 1/2가 2의 역원인 것은 역원을 그렇게 정의했기 때문이 아니라, 우리가 나눗셈을 그렇게 정의했기 때문이다. 2/2 = 1인 까닭은 2/2 = 2 * 2⁻이기 때문이다. 하지만 다시, 0에는 역원이 없고, 2/0은 2 * 0⁻이 아니다. 0⁻이 존재하지 않으니 2의 역원이 아니고, 0이 아닌 모든 수는 여전히 고유한 역원을 가진다.

1/0 = 1이 모순으로 이어짐을 보이려면, 당신은 당신이 밟는 모든 단계를 명시해야 하며 그 어느 것도 0⁻의 존재를 가정하지 않음을 보여야 한다.

우리는 이제 확립했다 당장은 어떤 상수 C를 골라 x/0 = C가 되도록 나눗셈을 정의해도 모순이 생기지 않는다고 가정하자.5 특정한 C, 특히 0을 선택하면, 몇몇 정리를 _강화_할 수 있다. 방법은 (일부) 나눗셈 정리의 조건을 없애고, 증명 안에 특수 경우를 추가하는 것이다. 예를 들어:

• 정리: a * (b/c) = b * (a/c). 증명: 이미 c ≠ 0일 때 증명했다. 이제 c = 0이라 하자. 그러면 a * (b/0) = a * 0 = 0, 또 b * (a/0) = b * 0 = 0, 따라서 0 = 0.

이 나눗셈 정의 아래에서는 위 반론의 (3)단계가 이제 유효해진다: 1/0 * 0 = 1 * 0/0이라 말할 수 있다. 하지만 (4)단계에서 0/0 = 1이라 했다. 이 정리는 강해지지 않는다:

• “정리”: a/a = 1. 증명: 이미 a ≠ 0일 때 증명했다. 이제 a = 0이라 하자. 그러면 a/a = 0/0 = 0, 따라서 1 = 0이 되고—잠깐, 안 되겠다

Lean과 Isabelle이 이렇게 1/0을 정의하는 이유가 이것이다. Coq도 이렇게 하지만, 내가 알기론 최적화에는 쓰지 않는다.

진짜 수학자들

마지막 반론은 내가 CS 쪽 사람이지 수학자가 아니라서 이 수학을 이해하지 못한다는 것이다. 그렇다면 박사 학위 가진 사람들은 뭐라고 할까?

Lawrence Paulson, 계산 논리 교수이자 Isabelle의 창시자:

약간의 역사: Isabelle에서 처음 지원된 논리는 Martin-Löf의 구성적 유형 이론이었고, 지금도 있다(CTT). 그 형식화 안에서 산술을 개발하면서, 나는 (필연적으로 원시 재귀적이고 실행 가능한) 나눗셈 정의를 고안했다. 그 결과 n/0 = 0이 나왔다. 그 이후로 여러 사람이 x/0 = 0으로 정의하는 것이 편리하다는 것을 알아챘다. 지금은 꽤 많은 정리 증명기에서 이 항등식이 성립한다.

이런 것들은 관례다. x^-n = 1/x^n, x^0 = 0 [원문 그대로 sic]라고 선언하는 것과 정확히 같은.

Leslie Lamport, 수학 박사이자 2013년 튜링상 수상자:

[ZF 집합론에서] 0은 _recip_의 정의역에 없기 때문에, 1 / 0의 값에 대해 우리는 아무것도 모른다. 그것이 √2일 수도, R일 수도, 다른 무엇이든 될 수도 있다.

Matt Noonan, 수학 박사이자 Ghost Proofs를 하스켈에 도입한 사람:

다 좋아 보이는데요!

Arthur Azevedo de Amorim, Coq 입문 교과서의 공저자는 내가 한 것과 같은 논증을 여기에서 재구성한다.

또한 몇몇 수학 대학원생 친구들과 아는 포닥 두 명에게도 연락했다. 지금까지 1/0 = 0을 허용하면 비건전하다고 말한 사람은 없다. 누가 그렇게 답장을 주면 이 글에 반박을 포함하겠다.

결론

이 글은 원래 Pony가 나눗셈을 어떻게 하는지에서 출발했다. 그렇다면 Pony는 여기서 옳은 일을 하고 있는가? 모르겠다. Pony는 프로그래밍 언어이지, 형식 수학 체계가 아니다. 일관성보다 안전, 편의, 맥락이 더 중요하다. 프로그래머로서 나는 마음에 들지 않는다.6

하지만 Pony가 비건전한 일을 하고 있는가? 전혀. 1/0 = 0이라고 정의하는 것은 완전히 괜찮다. 아무것도 망가지지 않고 거짓을 증명할 수 없다. Pony 프로그래머들을 ‘수학 못한다’며 비웃던 사람들은 그 뒤의 수학을 실제로 이해하지 못한 것이다.

다른 사람을 비웃지 말자. 세상은 크고 우리는 작다.

Watson Ladd, Matt Noonan, Ron Pressler, Josh Lieber, Edwin Brady에게 피드백을 감사드린다.

업데이트 2018-08-12

몇몇 분들이 내가 용어를 애매하게 썼다고 지적해 주셨고, 최대한 수정했다. 그리고 더 많은 반론도 여러 사람이 보내줬는데, 대부분 공통된 테마를 따른다.

ab = cb => a = c 하지만 0으로 나누기를 허용하면 1 * 0 = 2 * 0 => 1 = 2가 된다.

이건 많은 사람이 하는 흔한 실수다: 나눗셈의 어떤 성질이 정의의 일부라고 (우리가 그 조작이 유효함을 증명해야 하는 성질이 아니라) 가정하는 것. 하지만 나눗셈에는 “태생적” 성질이 없다: 나눗셈이 포함된 모든 조작은 그 조작이 유효함을 우리가 증명해야 한다. 어떤 모순이라도, 식을 조작할 때마다 그 조작을 유효하게 해주는 정리를 하나하나 나열하고, 그 정리의 증명이 0⁻을 사용하지 않음을 보여야 한다.

1/0 = 0을 허용하면 프로그램에 숨은 오류를 유발할 것이다.

앞서 말했듯, 이 글은 실용적으로 무엇이 좋은 아이디어인지에 관한 글이 아니다. 내가 주장하는 것은 수학적으로 이렇게 나눗셈을 확장해도 모순으로 이어지지 않는다는 것뿐이다. 프로그래밍 언어는 수학적 형식 체계와 다르며, 달라야 한다. 나는 1/0이 오류가 되길 선호한다. 내 프로그램으로 정리를 증명하는 게 아니기 때문이다.

모든 언어는 안전성, 실용성, 예측 가능성을 위해 수학적 건전성을 희생해야 한다. 거의 모든 실무 언어에서 head의 타입이 [a] -> a이지 [a] -> Maybe a가 아닌 이유와 같다.

이제 더 이상, 정의역 전체에서 나눗셈이 곱셈의 역함수라는 사실을 갖지 못한다.

흔한 주장인데, 논의의 초점은 형식화 가능성이라기보다 나눗셈의 “미학”에 가깝다. 함수들을 확장할 때 이런 일은 자주 일어난다. 예컨대 자연수 위에서 a * b는 반복된 덧셈일 뿐이다. 하지만 유리수로 곱셈을 확장하면 그 멋진 정의를 잃는다.

일반적으로, 나는 함수의 정의역에 대한 의존이 명시적으로 포함된 정의와 정리를 미학적으로 “싫어한다”. 확장할 때 “부작용”을 낳기 때문이다.

만약 0/0 = 0이면 lim_(x -> 0) sin(x) / x = sin(0) / 0 = 0인데, 로피탈의 정리에 따르면 lim_(x -> 0) sin(x) / x = lim_(x -> 0) cos(x) / 1 = 1이다. 그러니 0 = 1이다.

이건 꽤 영리했다. 문제는 반론이 “극한이 존재하고 f(0)이 정의되어 있다면 lim_(x -> 0) f(x) = f(0)”을 가정한다는 데 있다. 이건 항상 참이 아니다. 연속 함수에 점 불연속을 하나 추가해 보라. sin(x) / x의 극한은 sin(0) / 0이 아니다. sin(x) / x가 0에서 불연속이기 때문이다. 확장 전 나눗셈에서는 sin(0) / 0이 정의되지 않았기 때문이고, 확장한 나눗셈에서는 그것이 점 불연속이기 때문이다. 재미있게도 만약 x/0 = 1을 골랐다면 sin(x) / x는 모든 곳에서 연속이 된다.

다른 몇몇 분들도 극한을 이용한 반론을 제기했는데, 비슷한 방식으로 모두 해결된다.

찝찝하다.

동의한다.

업데이트 2019-10-23

Pony가 이제 부분 나눗셈을 지원한다고 들었다.

---

1. 이 글을 쓴 지 1년이 지나, Pony는 부분 나눗셈을 추가했다. 나는 여전히 그 언어에 대해 아는 바가 없지만, 이 글로 인해 그들이 곤욕을 치르는 것 같아 분명히 해 두고 싶었다. [return]
2. 분명히 하자면, 나는 이 기준을 완벽히 지키지 못한다. 지키려 노력하지만 자주 비틀거린다. 그 트윗 폭풍 중에 원 게시자를 한 번 놀렸는데 아직도 미안하다. [return]
3. 공리는 증명 없이 참이라고 받아들이는 것이다. 예시로 “0은 수다”와 “모든 것은 같거나 같지 않다”가 있다. 공리를 어떻게 고르느냐에 따라 매우 다른 수학적 틀이 나온다. 가장 유명한 예로 “임의의 한 점을 지나는 평행선은 정확히 하나 존재한다”는 공리를 거부하면 비유클리드 기하가 나온다. [return]
4. 네 번째 방법도 있다는 지적이 있었다: 1/0이 실수라는 것만 말하고 _그게 무엇인지는 모른다_고 하는 것이다. TLA+가 이렇게 형식화되어 있고, 다만 TLC는 1/0을 오류로 본다. [return]
5. 몇몇 분들이 우리가 사실 이것을 확립한 게 아니라, 흔한 반론들이 적용되지 않음을 보였을 뿐이라고 지적했다. 이것이 사실임을 증명할 수는 있지만, 증명은 매우 빨리 기술적으로 복잡해진다. [return]
6. Pony 개발자 중 한 분이 연락을 주셨다. Pony가 왜 1/0 == 0을 선택했는지 더 자세한 설명을 쓸 계획이라고 하며, 가능해지면 링크하겠다. 내 이해로는, Pony는 모든 부분 함수를 처리하도록 강제한다. 1/0을 정의하는 것은 그에 따른 “차악”의 결과다. [return]