여러 공리 식을 하나로 묶는 방법

John Baez 선생님 트위터에 올라온 이야기. 수학에서 lattice는 보통 집합과 두 연산 \vee, \wedge가 있어 위의 공리들을 만족시키는 대수적 오브젝트로 정의한다. 즉 두 연산은 교환법칙과 결합법칙을 성립시키며, p=p \wedge (p \vee q), p = p \vee (p \wedge q)를 만족시킨다는 것. (흡수법칙) 집합의 합집합과 교집합 어낼로지나 논리학의 or/and 등을 생각하면 이해하기 쉽다.

즉 lattice를 정의하기 위해선 6개의 식이 필요한데, 이를 단 한 개의 식으로 표현할 수 있는지에 대한 이야기이다. 1970년 Ralph McKenzie가 그런 식을 발견했지만 변수 34개를 써서 약 30만개의 심볼이 동원된 거대한 식이 되었다고. McKenzie는 6개의 axiom이 성립하는 것과 다음 4개의 식이 성립하는 것이 동치임을 밝히기도 했다.

\begin{aligned} x \vee (y \wedge (x \wedge z)) =& x \\ x \wedge (y \vee (x \vee z)) =& x \\ ((y \wedge x) \vee (x \wedge z)) \vee x =& x \\ ((y \vee x) \wedge (x \vee z)) \wedge x =& x \end{aligned}

그 후 1977년 Ranganathan Padmanabhan이 7개의 변수와 243개의 심볼을 쓴 식을 찾아냈고, 그 이후 Padmanbhan이 계속 이 주제에 매달려와 2003년 McCune, Veroff와 함께 다음 식을 발견했다고 한다.[1]

(((y \vee x) \wedge x) \vee (((z \wedge (x \vee x)) \vee (u \wedge x)) \wedge v))  \wedge (w \vee ((s \vee x) \wedge (x \vee t))) = x

8개의 변수와 29개의 심볼을 이용해 만든 이 식이 성립하는 것과 lattice의 여섯 공리가 성립하는 것이 동치가 된다. (길이가 같은 또 다른 식도 같이 발견함)

이 식을 발견하기 위해 약 5000억개의 가능한 식들을 컴퓨터로 생성한 다음 lattice가 아닌 것들도 만족하는 식들을 필터링해 약 10만개의 식들을 남긴 후, OTTER 프로그램으로 이들이 원래 정의와 동치인지를 증명을 찾아냈다고 한다. OTTER는 위 식으로부터 McKenzie의 4-basis를 찾아내는데 170스텝의 증명을 찾아냈고, 후에 Larry Wos가 50스텝짜리 증명으로 간략화했다. 이 증명은 [1]에서 확인할 수 있다.

참고로 OTTER의 증명 탐색이 너무 오래 걸리는 식들도 있어서, 위 식이 최단해는 아닐 수도 있다고 한다.

밑의 멘션을 보니 Wolfram Axiom이라고 불 대수에서 비슷한 역할을 하는게 있다고 한다. 아래 6개의 NAND를 쓴 식이 불 대수의 공리들과 동치라고. (역시 같은 길이의 또 다른 식도 발견됨)

((p \bar{\wedge} q) \bar{\wedge} r) \bar{\wedge} (p \bar{\wedge} ((p \bar{\wedge} r) \bar{\wedge} p)) = r

NAND 6개와 변수 2개로 나올 수 있는 16896개의 공리식들 중에서는 만족하는게 없었고, NAND 6개와 변수 3개로 만들 수 있는 288684개의 공리식들 중에서 추려낸 25개의 식들을 확인하는 식으로 2000년 스티븐 울프람이 찾았다고 한다. 더 짧은 식으로는 안 된다는 것도 울프람이 증명했다고. 거의 비슷한 시기에 lattice 논문에서 등장한 McCune, Robert, Wos 등도 위 식을 발견했다고 한다.[2]

References

[1] W. McCune, R. Padmanabhan and R. Veroff, “Yet another single law for lattices” Algebra univers. (2003) 50: 165. DOI: 10.1007/s00012-003-1832-2

[2] W. McCune, R. Veroff, B. Fitelson, K. Harris, A. Feist and L. Wos, “Short single axioms for Boolean algebra”, Journal of Automated Reasoning, 29 (1):1-16. DOI: 10.1023%2FA%3A1020542009983

답글 남기기

아래 항목을 채우거나 오른쪽 아이콘 중 하나를 클릭하여 로그 인 하세요:

WordPress.com 로고

WordPress.com의 계정을 사용하여 댓글을 남깁니다. 로그아웃 /  변경 )

Google photo

Google의 계정을 사용하여 댓글을 남깁니다. 로그아웃 /  변경 )

Twitter 사진

Twitter의 계정을 사용하여 댓글을 남깁니다. 로그아웃 /  변경 )

Facebook 사진

Facebook의 계정을 사용하여 댓글을 남깁니다. 로그아웃 /  변경 )

%s에 연결하는 중