2026년 8월, Ulrich의 u4라는 논리식 하나로 목표한 논리의 모든 정리를 끌어낼 수 있는지 살폈다. 내가 구성해 형식화한 반모형은 그 식만으로는 기본적인 명제인 P → P조차 끌어낼 수 없음을 보였다. 검증 패키지를 공개한 뒤에는 같은 핵심 결론과 Lean 형식화가 몇 달 먼저 공개되어 있었다는 사실을 확인했다. 저널 경로는 9월 2일 종료했다.
P → P는 ‘P라면 P이다’라는 뜻이다. 여기서 다룬 양의 함의 논리는 ‘그리고’나 ‘아니다’ 같은 다른 연결사 대신 함의를 중심으로 정리를 다룬다. 단일 공리 문제는 필요한 정리들을 하나의 출발식과 허용된 추론 규칙으로 모두 만들 수 있는지 묻는다. 그 체계의 정리 하나라도 만들 수 없음을 보이면, 후보식은 단일 공리 역할을 할 수 없다.
계산이 끝나지 않는 것과 불가능함을 보이는 것
증명을 한동안 찾지 못했다는 사실만으로 불가능하다고 결론 낼 수는 없다. 이 작업에서는 유한한 수식들을 대상으로 무한한 반모형을 구성했다. ‘참으로 취급하는 수식’의 집합을 정하고, u4의 모든 대입 사례가 그 안에 들어가도록 했다. 또 P와 P → Q를 얻으면 Q를 얻는 추론 규칙을 적용해도 그 집합 밖으로 나가지 않는다는 것을 보였다.
반면 P → P 꼴의 수식은 그 집합에 들어가지 않는다. 시작식에서 허용된 규칙으로 아무리 나아가도 목표한 수식에 도달할 수 없다는 경계가 생긴다. 같은 문자를 같은 수식으로 일관되게 바꾸는 균일 대입도 명시적으로 포함했다. 강화판에서는 표준 K·S 공리 체계가 P → P를 유도한다는 것까지 같은 Lean 환경에서 확인해, 무엇과 무엇을 구분하는지 드러냈다.
검증 패키지를 고정하며 고친 부분
초기 기록은 Lean 4.30.0 빌드였다. 8월 21일 공개한 수정·강화 v2에서는 Lean 4.33.0으로 옮기고, 균일 대입과 유도 규칙·건전성 정리를 명시했다. 건전성은 그 규칙으로 얻은 수식이 모두 반모형에서 참으로 취급되는 집합에 남는다는 성질이다. 공개 PDF에서 빠졌던 재귀 정의 부분도 복구했다.
Lean 직접 컴파일과 환경 검사, 별도 Rust 검사기 nanoda, 공리 의존성 감사, Python 심볼릭 검사를 함께 남겼다. 직접 컴파일은 종료 코드 0이었고 nanoda 로그에는 타입 검사 오류가 없었다. 공리 감사에는 사용한 표준 공리가 표시된다. 증명할 자리를 비워 두는 sorry·admit나 사용자 정의 공리로 결론을 통과시킨 것은 아니다.
Python 쪽에서는 재귀식 100단계와 잎이 12개인 이진 적용 트리 58,786가지까지 검사했다. 여기서 잎은 출발식 한 사본, 내부 갈림길은 두 식을 적용하는 한 단계다. 이 유한 검사는 재귀식과 구현을 대조하는 보조 수단이고, 모든 단계에 대한 결론은 귀납 증명과 형식화가 맡는다. 서로 다른 검사기를 프로젝트 안에서 실행해 맞대 본 결과다.
선행 결과를 확인한 뒤
처음의 공개 검색에서는 같은 증명을 찾지 못했다. 8월 29일 후속 확인에서 3월 12일 공개된 고정 버전을 받았고, 동일한 핵심 결과와 Lean 검증이 먼저 존재한다는 것을 확인했다. 그날 구조적 중복과 우선권 문제를 저널에 알렸다. 9월 2일에는 핵심 결과의 신규성이 부족하다는 이유로 거절되었고, 같은 결과로 이어가던 투고 경로를 닫았다.
공개 검증 패키지는 남아 있다. DOI는 파일을 공개 보존한 기록이고, 출판 심사에서 결과의 새로움을 인정받았다는 표시는 아니다. 9월 5일에는 선행 고정 버전과 내 강화판을 정리별로 대조할 묶음을 준비했다. 비교를 준비한 단계에서, 이어 갈 수 있는지는 선행 결과와 겹치지 않는 명제를 실제로 확보하는 데 달려 있다. 다시 이 주제를 붙잡는다면 그 질문부터 확인해야 한다.