Σ₁ 문장에 한정하면, ‘증명 가능함’의 논리를 판정할 수 있을까요?

먼저 “어떤 자연수 n에 대해 n+2=5이다”를 E라고 부르겠습니다. n=3을 넣으면 3+2=5이므로 E를 확인할 수 있습니다. 이때 3은 존재 주장을 뒷받침하는 증인입니다. 여기서 자연수에는 0을 포함합니다.

“E를 증명할 수 있다”는 한 걸음 더 나아간 말입니다. 계산과 추론 규칙을 적은 유한한 증명문이 있다는 뜻이지요. 이 글에서는 헤이팅 산술이라는 체계를 쓰며 줄여서 HA라고 적습니다. HA는 자연수의 계산과 귀납법을 직관주의 논리로 다룹니다.

논문은 E 하나의 증명을 찾는 데서 멈추지 않습니다. E처럼 증인의 존재를 표현하는 문장을 여러 자리에 넣어도 항상 보존되는 증명 가능성의 규칙을 묻습니다. 개별 계산과 모든 허용 치환에 관한 질문을 먼저 나누어 봅시다.

□E는 “HA에서 E의 증명이 존재한다”로 읽습니다. 증명의 각 기호와 줄을 자연수로 부호화하면, d가 E의 올바른 증명 코드인지 기계적으로 검사할 수 있습니다. 이를 Proof_HA(d,⌜E⌝)라고 적겠습니다. ⌜E⌝는 문장 E 자체의 코드입니다.

따라서 □E의 산술 번역은 ∃d Proof_HA(d,⌜E⌝)입니다. 앞의 n=3은 등식의 증인이고, 여기서 d는 증명 전체의 코드입니다. 부호화 방식을 정하지 않았으므로 d에 임의의 숫자를 붙이지 않겠습니다.

이 구분은 □가 두 번 붙을 때도 필요합니다. □□E는 “E의 증명이 있다는 문장의 증명이 있다”입니다. 바깥 □가 생기면 검사할 증명문의 결론도 달라집니다.

3+2=5 같은 계산은 고전적인 페아노 산술 PA와 HA에서 모두 다룰 수 있습니다. 차이는 일반적인 논리 규칙에 있습니다. PA는 임의의 A에 대해 A∨¬A를 사용할 수 있지만, HA에서는 이 배중률을 모든 문장에 일괄 적용하지 않습니다.

예를 들어 “어느 프로그램이 언젠가 멈춘다”는 주장을 P라고 해 봅시다. 제한된 횟수까지 실행해 멈추지 않았다는 사실만으로 ¬P를 얻을 수는 없습니다. 더 오래 뒤에 멈출 수도 있기 때문입니다. 반면 실제로 멈춘 유한 실행 기록은 P의 증인이 됩니다.

이 차이는 “증명할 수 있다”는 말의 규칙에도 영향을 줍니다. 뒤에서 나오는 여러 양상논리의 이름은 이러한 규칙 묶음의 이름입니다. 우선 계산의 증인, 산술의 증명, 그 증명에 관한 주장을 구분하면 됩니다.

앞의 E=∃n(n+2=5)는 존재 양화사 뒤에서 유한한 계산으로 조건을 확인하는 문장입니다. Σ₁ 문장은 엄밀하게는 앞의 존재 양화사들 뒤에 유계 양화사만 있는 산술 공식을 두는 형태로 설명합니다. 계산 기록을 함께 부호화하면 유한 계산의 성공도 이 형태로 표현할 수 있습니다.

치환 σ는 원자 명제 p,q에 산술 문장을 배정합니다. 예를 들어 σ(p)=∃n(n+2=5), σ(q)=∃m(m+m=8)로 정하면 p∧q는 두 존재 문장의 연언으로 바뀝니다. 첫 문장의 증인은 3, 둘째의 증인은 4입니다. □는 앞 문답의 HA 증명 술어로 번역합니다.

제한되는 곳은 원자 p,q의 해석입니다. p→q처럼 조합한 공식 전체까지 언제나 Σ₁ 문장이라고 가정하지 않습니다. 또 이 치환 한 번의 성공만으로 규칙의 타당성이 증명되지는 않습니다. 논문의 질문은 모든 Σ₁ 치환에서 성립하는가입니다.

Σ₁ 문장은 유한한 계산이나 증인 탐색의 성공을 표현하는 데 자연스럽습니다. ‘어떤 수가 이 조건을 만족한다’, ‘어떤 코드가 증명이다’ 같은 문장이 여기에 속합니다.

논문은 이 조각이 단순한 장난감이 아님을 보입니다. HA의 증명 가능성에서 알려진 어려운 현상과 반례가 이미 나타나며, 동시에 정확한 공리화와 판정 절차를 만들 만큼 구조가 드러납니다.

HA에는 명제 수준의 분리 성질이 있지만, □(p∨q)→(□p∨□q)는 모든 산술 치환에서 성립하지 않습니다. 논문은 크립키 반모형과 Σ₁ 치환을 연결해 이 공식을 반박할 수 있음을 보입니다.

핵심은 메타수준의 분리 성질과 체계 내부에 형식화된 증명 가능성 명제를 섞지 않는 데 있습니다. □ 안의 증명 존재를 다시 □p 또는 □q 중 하나로 고르는 일은 별도 원리입니다.

iHσ는 이 논문이 제시한 규칙 체계의 이름입니다. 예를 들어 원자 p에 Σ₁ 문장을 넣는 조건에서는 p→□p라는 원리를 사용할 수 있습니다. 앞의 간단한 예에서는 등식의 증인을 확인하는 계산을 산술 증명으로 옮기는 모습을 볼 수 있습니다.

여기서 원자에 한정한 원리는 CP_a입니다. 임의의 복합 공식 B에 대해 B→□B를 허용하는 CP와 구별해야 합니다. 논문의 비교 체계 LC에는 전체 CP가 들어갑니다. 두 체계를 같은 공리 목록으로 취급하면 적용 범위가 넓어집니다.

iHσ의 정확한 정의에는 직관주의 뢰프 논리 계열의 규칙, 확장 Leivant 원리, 원문의 보존 관계에서 얻는 □A→□B도 들어갑니다. 뒤의 판정에서는 그 목록을 외우기보다 어떤 공식을 보존하며 다른 체계로 옮기는지를 보겠습니다.

함의 A→B에서 A가 왼쪽입니다. (p→q)→r를 보면 바깥 함의의 왼쪽에 또 함의 p→q가 있습니다. 반면 p→(q→r)는 안쪽 함의가 오른쪽에 있습니다. 이 위치 차이를 따지는 것이 NNIL의 출발점입니다.

TNNIL은 □ 안쪽에도 같은 제한을 적용하되 □ 경계를 구분합니다. 그래서 □(p→q)→r는 허용되지만 (p→q)→r는 그대로 허용되지 않습니다. □를 지워 두 식을 같게 읽으면 이 구분을 놓칩니다.

예를 들어 ¬¬p는 (p→⊥)→⊥이고, 그 근사 공식은 p입니다. 이 예에서 p는 이미 허용된 모양입니다. 이 변환의 근거는 다음 문답에서 확인하겠습니다.

상자가 없는 예 A=¬¬p를 보겠습니다. A의 NNIL 근사 A*=p에서 원래 식으로 가는 p→¬¬p는 직관주의 논리로 증명됩니다. p를 가정한 뒤 ¬p를 더 가정하면 모순 ⊥을 얻으므로, ¬p라는 가정을 닫아 ¬¬p를 얻습니다. 역방향 ¬¬p→p는 일반적으로 허용되지 않습니다.

NNIL 근사의 아래쪽 근사 성질은 A*→A라는 방향입니다. 그러나 □ 안까지 바꾸는 TNNIL 근사 A⁺에는 이 함의 관계를 그대로 일반화할 수 없습니다. 원문은 정의 4.6 뒤에서 이 차이를 명시합니다.

판정에 필요한 보존은 모든 Σ₁ 치환 σ에 대한 HA ⊢ □σ(A)↔□σ(A⁺)입니다. 이 식에서 바깥 □를 임의로 지워 σ(A)↔σ(A⁺)로 쓰면 안 됩니다. 무엇을 보존하는 근사인지가 핵심입니다.

작은 모형으로 □(p∨q)→(□p∨□q)를 검사해 봅시다. 시작점 α에서 β와 γ로 갈라집니다. β에서는 p만, γ에서는 q만 강제합니다. 강제는 그 노드에서 공식이 성립한다고 판정하는 관계입니다. “강제하지 않는다”를 곧바로 “부정을 강제한다”로 읽지는 않습니다.

여기서는 정보가 늘어나는 순서 ≤에 α≤β, α≤γ를 두고 각 노드의 자기 관계도 포함합니다. □를 검사하는 R에는 αRβ, αRγ만 둡니다. β와 γ는 끝 노드입니다. 이 유한 나무는 LC에 허용되는 모형 조건을 만족합니다.

α의 모든 R-후속 노드에서 p∨q가 성립하므로 □(p∨q)는 성립합니다. 하지만 γ 때문에 □p가 실패하고, β 때문에 □q도 실패합니다. 따라서 α에서 전건은 성립하고 후건은 성립하지 않습니다. 이 반모형이 해당 공식의 LC 비증명을 보여 줍니다.

건전성 정리 6.3은 iHσ에서 증명되는 모든 공식이 HA의 모든 Σ₁ 산술 해석에서 성립한다고 말합니다. 공리 하나하나가 산술 해석 아래 보존되는지 확인하는 방향입니다.

대부분의 공리는 알려진 결과를 이용하고, 논문이 새로 보강하는 핵심은 확장된 Leivant 원리입니다. 건전성만으로는 iHσ가 빠뜨린 타당식이 없는지 알 수 없으므로 완전성이 따로 필요합니다.

방금 본 기호 p,q를 실제 산술 문장으로 옮겨야 HA에 관한 결론이 됩니다. 이를 위해 저자들은 자연수 단계에 따라 모형의 노드를 값으로 갖는 특수한 계산 가능 함수 F를 구성합니다. 단순히 왼쪽·오른쪽을 번갈아 고르는 함수로 대체할 수는 없습니다.

B=∃x(F(x)=β), C=∃x(F(x)=γ)라고 두면, 각각 F가 그 노드에 도달하는 단계의 존재를 표현합니다. 함수 계산 기록을 부호화해 Σ₁ 문장으로 나타냅니다. 여기서 β,γ는 산술 안에서는 노드에 붙인 수 코드로 읽습니다.

5절의 어려운 부분은 F의 정의와 산술 모형들을 함께 구성해, 필요한 원자식과 □ 공식의 강제 관계를 보존하는 것입니다. 이 조건이 갖춰지면 위 반모형의 □(p∨q) 성립과 □p∨□q 실패가 산술 번역에도 이어집니다. 따라서 HA가 그 번역된 함의를 증명하지 못합니다. 아래는 대응할 문장을 펼친 것이며, 모형 존재의 긴 증명을 대신하지 않습니다.

판정의 입력은 양상 공식 A입니다. 먼저 TNNIL 근사 A⁺를 계산하고, LC에서 A⁺가 증명되는지 판정합니다. 그 답이 iHσ에서 A가 증명되는지의 답이 됩니다.

앞의 A=□(p∨q)→(□p∨□q)는 이미 TNNIL 형태여서 근사해도 같은 형태로 둘 수 있습니다. 문답 10에서 LC 반모형을 얻었으므로 이 입력의 답은 “아니오”입니다. 비교하면 A=p→p는 가정 p를 그대로 반환하는 증명이 있으므로 “예”입니다.

아래 버튼은 확인한 두 예의 근거를 읽는 활동입니다. 임의 공식을 받아 TNNIL 변환이나 모형 탐색을 수행하는 프로그램은 아닙니다. 일반 결정 절차의 정당화는 원문의 정리 6.6에 있습니다.

논문은 HA에 □⊥을 더한 이론이 de Jongh 성질을 가진다는 결과도 얻습니다. 양상 기호가 없는 명제 공식 A에 대해, IPC에서 증명되는 것과 모든 산술 치환이 이 확장 이론에서 증명되는 것이 일치합니다.

이 결과는 ‘HA 자체의 모든 경우’를 말하지 않습니다. □⊥을 추가한 특정 이론과 비양상 명제 공식에 대한 진술입니다. 논문의 중심인 Σ₁ 증명 가능성 논리와 연결되지만 적용 범위를 따로 적어야 합니다.

예, 원자식을 Σ₁ 문장으로 해석하는 범위에서는 가능합니다. TNNIL 근사와 LC의 유한 모형 판정을 거쳐 iHσ에서 공식이 증명되는지 끝나는 절차로 결정할 수 있습니다.

이 답을 HA의 전체 증명 가능성이나 산술의 모든 참·거짓 판정으로 넓히면 논문의 경계를 벗어납니다. 정확한 결론은 제한된 해석의 건전하고 완전한 공리화와 그 정리 집합의 결정가능성입니다.