근거가 붙은 주장에 반례가 있는지, 어디까지 확인하면 될까요?

보통의 양상논리는 □A로 “A가 알려져 있다”거나 “A가 증명 가능하다”는 뜻을 나타냅니다. 정당화 논리는 t:A처럼 써서 A를 뒷받침하는 근거나 증명을 t라는 항으로 함께 적습니다.

논문은 이 명시적인 근거가 직접 관찰일 수도 있고, 친구가 A를 들었다는 보고처럼 전달된 증거일 수도 있다고 설명합니다. 그래서 핵심 질문은 A의 참만이 아니라 어떤 근거가 어떤 방식으로 결합되는지까지 포함합니다.

항은 상수 c와 변수 x에서 시작합니다. 두 근거를 적용하는 t·s, 어느 한 근거를 더하는 t+s, 근거 자체를 다시 확인하는 !t를 사용해 더 복잡한 항을 만듭니다.

기호는 장식이 아닙니다. 뒤에 나오는 공리와 증거 관계의 닫힘 조건이 각 연산의 역할을 정합니다. 생활 속 “근거를 합친다”는 말과 논리식의 정확한 조건을 구별해야 합니다.

t가 A→B의 근거이고 s가 A의 근거라면 t·s는 B의 근거가 됩니다. 또 t나 s 가운데 하나가 A의 근거이면 t+s도 A의 근거가 됩니다.

첫 규칙은 modus ponens에 근거의 이동 경로를 붙입니다. 둘째 규칙은 어느 쪽 근거를 갖고 있든 합친 항으로 A를 지지하게 합니다. 두 연산의 뜻을 같은 “증거 합치기”로 뭉개면 조건의 차이를 놓칩니다.

이것을 허용하는지가 논리 체계를 나누는 조건입니다. jt라는 공리는 “t가 A의 근거이면 A다”를 뜻합니다. 이 공리를 채택한 체계에서는 근거에서 주장의 참으로 나아갈 수 있습니다.

jd는 모순을 정당화하는 근거를 허용하지 않는 조건이고, j4는 “t가 A의 근거다”에서 “!t는 t가 A의 근거라는 주장의 근거다”로 나아가는 조건입니다. !t는 근거를 다시 확인하는 형식적 연산입니다.

J는 기본 체계의 이름입니다. JT, JD, J4는 각각 해당 조건을 더한 체계이고, JD4는 jd와 j4를, LP는 jt와 j4를 더합니다. 여기의 LP는 증명 논리라는 이름이며, 호주편의 역설의 논리 LP와 구별합니다.

상수 명세 CS는 어떤 상수 c가 어떤 공리 A의 근거인지를 기록한 목록입니다. 모든 공리에 적절한 상수가 있는지, 한 상수가 일정한 공리 꼴을 체계적으로 담당하는지가 뒤의 결과에 영향을 줍니다.

논문은 axiomatically appropriate, schematic, decidable이라는 조건을 구분합니다. JD 계열의 강한 유한 모형 성질에는 적절성이 필요하고, 결정가능성에는 명세가 판정 가능한 도식이어야 합니다.

증거 관계 E는 (t,A,w)라는 세 항목을 묶어 세계 w에서 t가 A의 허용된 근거임을 기록합니다. 적용·합·상수 명세와, j4가 있을 때의 ! 연산 및 세계 이동에 대해 닫혀야 합니다.

여기서 “닫혀 있다”는 입력 관계가 있으면 규칙이 요구하는 출력 관계도 반드시 포함된다는 뜻입니다. 실제 사실 여부는 뒤의 만족 관계에서 접근 가능한 세계와 함께 다시 검사합니다.

증거 기반 B는 출발점으로 적어 둔 유한한 관계들의 집합입니다. 전체 증거 관계 E는 B를 포함하고 닫힘 규칙을 모두 적용한 최소 고정점입니다.

기반이 유한해도 닫힘을 반복해 얻는 E 자체가 겉보기에는 커질 수 있습니다. 논문의 유한 모형 정의가 E의 모든 원소를 직접 나열하라고 하지 않고, E를 생성하는 유한 기반 B를 요구하는 이유입니다.

세계 w에서 t:A가 참이려면 두 조건이 모두 필요합니다. w에서 접근 가능한 모든 세계 v에서 A가 참이어야 하고, (t,A,w)가 증거 관계 E에 들어 있어야 합니다.

근거 꼬리표만 붙었다고 문장이 자동으로 참이 되지 않습니다. 반대로 A가 모든 관련 세계에서 참이어도 t가 허용된 근거로 등록되지 않았다면 t:A는 성립하지 않습니다.

건전성은 공리와 규칙으로 유도한 식이 모든 해당 모형에서 타당하다는 뜻입니다. 완전성은 유도되지 않는 식에 대해 그 식이 실패하는 모형을 찾을 수 있다는 방향을 제공합니다.

이 논문은 선행 연구의 건전성과 완전성 결과를 정리한 뒤, 특히 유한 모형에 대한 완전성 보조정리를 사용합니다. 따라서 핵심 따름정리는 논문 안에서 처음부터 긴 여과 증명을 다시 전개한 결과가 아닙니다.

유한 모형은 세계 집합 W가 유한하고, 증거 관계가 유한 기반 B에서 생성되며, 어떤 세계에서 어떤 원자 명제가 참인지 적은 평가 기록도 유한해야 합니다.

세계 수만 세고 “작은 모형”이라고 부르면 부족합니다. 명시적 근거를 다루기 때문에 근거 기반과 참값 기록의 크기도 함께 관리해야 합니다.

단순한 유한 모형 성질은 필요한 반모형이 유한하다고 말합니다. 강한 성질은 입력 식 A의 길이 |A|에 따라 세계 수, 증거 기반 크기, 평가 기록 크기의 상한을 계산 가능한 함수 f·g·h로 잡을 수 있다고 말합니다.

따라서 반모형이 어딘가 유한하게 존재한다는 정보에서 한 걸음 더 나아가, 어디까지 찾아보면 되는지 계산 가능한 경계를 얻습니다. 이 경계가 결정 절차를 만드는 핵심입니다.

J·JT·J4·LP는 상수 명세에 대해 강한 유한 모형 성질을 얻습니다. JD·JD4는 상수 명세가 공리적으로 적절하다는 조건이 추가됩니다.

논문의 따름정리 11은 이 목록과 조건을 정확히 나눕니다. 다른 정당화 논리나 더 풍부한 언어까지 자동으로 포함한다고 읽을 근거는 없습니다.

논문은 상수 명세가 판정 가능한 도식이고 모형이 유한하게 제시되면, 세계 w에서 식 A가 참인지 결정할 수 있다는 선행 보조정리를 사용합니다.

유한하다는 사실만으로 모든 검사가 저절로 쉬워지는 것은 아닙니다. 증거 관계가 유한 기반에서 닫힘으로 생성되므로, 명세와 관계의 소속을 효과적으로 확인할 조건이 함께 필요합니다.

판정 가능하다는 말은 정해진 입력마다 절차가 끝나고 예 또는 아니요를 답한다는 뜻입니다. 빠르게 끝난다는 뜻까지 포함하지는 않습니다.

먼저 A가 항상 성립하는지 묻는다고 합시다. 검사 범위에 포함되는 모형에서 A가 거짓인 세계를 하나 찾으면 반례를 얻습니다. 건전성에 의해 A는 그 논리에서 증명되는 문장이 될 수 없습니다.

반례가 존재하면 계산 가능한 크기 상한 안에도 반례가 있다는 성질과 필요한 판정 조건을 확보한 경우, 그 상한 안의 후보를 빠짐없이 검사할 수 있습니다. 모든 검사를 끝내고도 반례가 없다면 완전성에 의해 A의 타당성과 증명가능성을 결론 내립니다. 몇 개의 작은 모형만 확인한 상태에서는 이 결론을 내릴 수 없습니다.

“A가 참인 경우가 하나라도 있는가?”라는 만족가능성 질문은 별도로 봅니다. 이 글에서 다루는 고전적 부정이 있는 체계에서는 ¬A의 타당성을 검사해 답할 수 있습니다. A를 거짓으로 만드는 모형 하나가 발견됐다는 사실만으로 A가 어느 모형에서도 참일 수 없다고 결론 내리면 안 됩니다.

논문이 열거한 정당화 논리에서는 가능합니다. 식 길이에 따라 반모형의 세계·증거 기반·평가 크기를 계산 가능한 범위로 제한하고, 필요한 조건 아래 그 범위의 후보들을 검사해 타당성과 증명가능성을 판정합니다. 고전적 부정을 이용하면 만족가능성도 판정할 수 있습니다.

결론에는 조건이 붙습니다. 사용한 논리 체계, 상수 명세의 도식성·판정가능성·필요한 적절성, 선행 유한 모형 완전성 결과가 모두 필요합니다. 작은 모형 성질은 효율적인 실행 시간을 자동으로 보장하는 주장도 아닙니다.