초일관적 계산 가능성과 함수 문제의 출발점
원문의 문제 설정과 기호를 독자가 직접 따라갈 수 있게 풀어 읽습니다.
모순을 허용하면 계산에서 무엇이 달라지나요?
출석 기록 두 개가 충돌하는 예로 시작해 보겠습니다. 한 기록은 “출석했다”, 다른 기록은 “출석하지 않았다”고 되어 있습니다. 두 기록을 함께 다루면서도 관계없는 모든 결론이 따라오지 않게 하는 논리를 초일관 논리라고 합니다. 이 예는 계산 문제를 설명하려고 만든 상황이며, 기록의 정확성은 별도로 확인해야 합니다.
이제 출석이면 1, 결석이면 0을 내는 계산을 생각해 봅시다. 같은 학생에게 두 값을 모두 내놓으면 입력과 출력의 관계는 기록할 수 있습니다. 그러나 하나의 입력에 출력 하나를 대응시키는 함수의 조건을 충족하는지 문제가 생깁니다. 논문의 비교는 이 문제에서 출발합니다.
연구진은 허용하는 추론 규칙이 많은 체계와 일부 규칙을 제한한 체계를 비교합니다. 각 체계의 이름은 해당 규칙과 예를 설명하는 대목에서 살펴보겠습니다.
첫 두 안내 질문은 무엇을 묻나요?
Q1은 모순되지만 자명하지 않고 모든 계산 가능한 관계를 나타내면서 완전한 산술이 있는지 묻습니다. Q2는 그런 이론이 자기 자신의 절대적 일관성 곧 자명하지 않음을 증명할 수 있는지 묻습니다.
고전 괴델 정리의 가정 가운데 부정 일관성을 바꾸면 새로운 가능성이 생길 수 있습니다. 다만 모순을 허용했다는 사실만으로 완전성과 자기 증명이 자동으로 따라오지는 않습니다.
나머지 안내 질문은 무엇을 더 요구하나요?
Q3은 정지 함수를 나타낼 수 있으면서 이론이 결정 가능한지 묻고 Q4는 수축 규칙을 쓰지 않으면서 자기 건전성을 말할 수 있는지 묻습니다. Q5는 실제 계산과 수학적 추론을 수행할 만큼 풍부한지도 확인합니다.
논문은 이 모든 조건을 갖춘 체계를 아직 찾지 못했다고 분명히 말합니다. 목표 가운데 하나를 얻을 때 다른 조건을 잃는 양상이 비교의 중심입니다.
함수 문제는 어디서 생기나요?
어떤 성질 A가 입력 n에 대해 참이면서 거짓이라면 그 특성 함수는 같은 입력에 1과 0을 모두 내놓게 됩니다. 하나의 입력에 하나의 출력만 대응해야 한다는 함수 조건과 모순 정보가 정면으로 부딪칩니다.
저자들은 함수를 포기하면 계산 자체가 어려워지고 함수를 그대로 두면 0=1 같은 붕괴가 생길 수 있다고 진단합니다. 이 갈등은 논문 전체에서 반복되는 기준입니다.
R♯는 무엇을 얻고 무엇을 놓치나요?
마이어의 관련 산술 R♯는 모든 계산 가능한 관계를 표현하고 결정 불가능하며 자기 안에서 절대적 일관성을 보일 수 있는 체계로 소개됩니다. 그러나 부정 완전하지 않고 페아노 산술의 모든 긍정 정리를 포함하지도 않습니다.
특히 이차잉여 공식이 R♯에서 증명되지 않는다는 결과는 R♯가 고전 페아노 산술만큼 강하다는 기대를 꺾습니다. 저자들은 장점과 결손을 함께 적습니다.
모순 산술의 유한 모형은 어떻게 생기나요?
힙 모형은 일관적인 처음 구간 뒤에서 수들이 서로 같기도 하고 다르기도 한 영역을 둡니다. 순환 모형은 정수의 모듈러 산술처럼 마지막 수 다음이 처음으로 돌아옵니다.
두 유형 모두 유한하게 만들 수 있어 결정 가능성을 다루기 쉬워집니다. 하지만 유한하다는 장점이 우리가 보통 기대하는 무한 자연수 구조를 얼마나 보존하는지는 별도 질문입니다.
RM3 산술은 다섯 질문에 얼마나 답하나요?
RM3의 유한 모듈러 산술은 모순되지만 자명하지 않고 완전하며 결정 가능한 사례를 제공합니다. 원 논문은 Q1과 Q2에 긍정적 사례가 된다고 정리합니다.
정지 함수가 표현 가능한지는 알려지지 않았고 수축 규칙은 여전히 유효합니다. 관련성도 잃어 무관한 명제를 잇는 Safety 같은 함의가 성립합니다. 좋은 성질이 한 묶음으로 따라오지는 않습니다.
PAC로 바꾸면 함수 문제가 사라지나요?
PAC의 조건문은 RM3와 다르게 약화는 허용하고 대우는 허용하지 않지만 두 논리는 정의적으로 서로 번역됩니다. PAC 기반 산술도 비자명하고 모순되며 결정 가능한 유한 모형을 가질 수 있습니다.
그러나 같은 입력이 긍정과 부정을 함께 만족하면 특성 함수가 0과 1을 모두 요구하는 핵심 문제는 남습니다. 조건문을 바꾸는 일만으로 함수성이 회복되지는 않습니다.
RM3와 PAC는 여기서 비교하는 두 논리 체계의 이름입니다. RM3에서는 “A이면 B”에서 “B가 아니면 A가 아니다”로 바꾸는 대우 규칙을 유지합니다. PAC에서는 결론을 얻은 뒤 쓰지 않은 전제를 더해도 되는 약화 규칙을 유지합니다. 어떤 규칙을 보존하는지에 따라 산술 증명과 계산의 성질이 달라집니다.
초일관 튜링 기계는 더 많이 계산하나요?
LFI1으로 공리화한 초일관 튜링 기계는 고전 튜링 기계로 모사할 수 있다는 아구델로와 카르니엘리의 결과가 소개됩니다. 비결정적 기계가 결정적 기계보다 계산 능력이 더 크지 않다는 고전 결과와 나란히 읽힙니다.
저자들은 이를 실패 하나로만 보지 않습니다. 고전 계산 이론에서 너무 멀어지지 않으려는 보수적 목표에는 장점이고 처치–튜링 장벽을 넘으려는 목표에는 한계입니다.
일관성 연산자는 해결책인가요?
일관성 연산자 ◦를 쓰면 A가 모순되지 않는 경우만 골라 특성 함수를 정의할 수 있습니다. 논문은 이 방법이 강한 논리에서 함수 문제를 다룰 근거를 준다고 평가합니다.
하지만 ◦A 자체가 일관적이라는 보장이 필요합니다. 일관성의 일관성을 한 단계 위에서 다시 가정하면 보복형 거짓말쟁이와 괴델식 대각화 문제가 되돌아올 수 있습니다.
왜 수축 없는 논리를 찾나요?
수축은 A를 두 번 쓰는 전제를 한 번으로 줄이는 추론을 허용합니다. 산술의 증명 가능성을 표현할 때 수축과 순열은 뢰프 정리의 한계 논증을 떠받쳐 자기 건전성을 내부에서 증명하려는 목표를 막습니다.
DK 같은 깊은 관련 논리는 수축을 버려 이 경로를 피하려 합니다. 대신 익숙한 추론이 약해져 기본 계산을 전개하기가 매우 어려워집니다.
수축 규칙은 같은 전제를 두 번 요구하는 증명을 그 전제 한 번으로도 쓸 수 있게 하는 규칙입니다. 이 규칙을 제한하면 전제의 사용 횟수가 증명에 영향을 줍니다. 약한 논리라는 말은 이처럼 허용하는 규칙이 제한된다는 뜻으로 읽어야 합니다.
MC♯는 약한 논리의 실용성을 보여주나요?
브래디의 MC♯는 의미 포함 논리에 산술을 세워 모든 원시 재귀 함수와 일반 재귀를 다룰 수 있다고 보고됩니다. 메타평가를 통해 부정 일관성도 확보합니다.
이 성취는 약한 관련 논리에서도 고전 계산 이론을 상당히 수행할 수 있음을 보여줍니다. 동시에 부정 일관성 때문에 고전적 불완전성 한계를 피하려는 급진적 목표에는 답이 되지 않습니다.
DL의 집합론 경로는 무엇이 다른가요?
로건과 보쿠니는 매우 약한 DL의 이차 논리와 프레게의 기본법칙 V를 이용해 집합론에서 페아노 공리의 유사물을 끌어냅니다. 상수 t와 결합 규칙을 세심하게 써서 후속자와 자연수를 구성합니다.
이 경로에서는 덧셈도 함수 기호보다 세 자리 관계 S(x,y,z)로 다룹니다. 함수 문제를 피할 가능성이 있지만 어떤 산술이 실제로 따라오는지는 아직 충분히 알려지지 않았습니다.
약한 Kleene 정리는 무엇을 바꾸나요?
저자들은 계산 가능한 관계를 허용해 선결정 가능과 선준결정 가능을 정의합니다. 함수성까지 만족할 때만 각각 결정 가능과 준결정 가능이라고 부릅니다.
약한 Kleene 정리는 집합과 여집합이 준결정 가능하면 그 집합은 선결정 가능하다고 말합니다. 모순된 집합은 0과 1을 함께 요구하므로 선결정 가능할 수 있어도 결정 가능한 함수는 가질 수 없습니다.
처음 질문에는 어떤 답을 줄 수 있나요?
현재 논문이 주는 답은 “아직 피하지 못했다”에 가깝습니다. 강한 논리는 계산하기 쉽지만 고전 한계를 함께 보존하고 약한 논리는 새로운 가능성을 열지만 함수성과 기본 산술 전개가 어렵습니다.
중요한 진전은 0과 1이 함께 나온 순간 가정을 모두 버리지 않고 그 대응이 함수가 아니라 계산 가능한 관계였는지 다시 묻는 데 있습니다. 이것은 장벽을 넘었다는 증명이 아니라 새 이론을 설계할 출발점입니다.
자료와 출처
- 주된 원전 · Zach Weber · Fernando Cano-Jorge, On Strong and Weak Logics for Paraconsistent Computability, Journal of Applied Logics 12(5), 1349–1381쪽. 공개 전문.
원문의 긴 문장을 옮겨 싣지 않고 논증 구조를 한국어로 풀었습니다. 논문 주장과 편집부 모형을 구분했으며 인용 수는 사용하지 않았습니다.
