연결사의 규칙은 서로 모순되지 않을까요?

기호의 모양만으로는 연결사의 뜻이 생기지 않습니다. 증명론에서는 그 연결사를 결론으로 도입할 때 무엇을 보여야 하는지, 전제로 사용할 때 무엇을 꺼낼 수 있는지를 규칙으로 적습니다. 예를 들어 함의 (A ⊃ B)를 오른쪽에 도입하려면 (A)를 가정해 (B)를 얻는 증명이 필요합니다.

규칙 두 묶음이 따로는 그럴듯해도 함께 놓으면 충돌할 수 있습니다. 같은 전제 조건에서 ◇(A,B)를 만들 수 있고 동시에 그것을 반박하는 방식으로 쓸 수 있다면, 잘라내기(cut)를 거쳐 빈 결론이 생길 수 있습니다. 논문은 이 위험을 규칙의 모양에서 미리 찾습니다.

논문이 쓰는 시퀀트 Γ⇒E에서 오른쪽 E에는 공식이 하나 있거나 아예 없습니다. 빈 후건 Γ⇒은 Γ가 모순을 낳는다는 뜻으로 읽습니다. 이렇게 해야 직관주의 부정의 표준 규칙을 canonical rule로 담을 수 있습니다.

후건이 항상 정확히 하나인 strict 단일 결론 체계에서는 A⇒처럼 부정의 전제가 되는 빈 결론을 표현하지 못합니다. 논문은 Gentzen의 non-strict 틀로 옮기고, 그 대가로 consistency와 coherence의 관계를 더 세밀하게 나눕니다.

오른쪽 도입 규칙은 원자 p₁,…,pₙ으로 된 유한한 전제 시퀀트들을 갖고, 결론으로 ⇒◇(p₁,…,pₙ)을 냅니다. 실제 증명에서는 원자를 공식으로 치환하고 공통 왼쪽 문맥을 붙입니다.

왼쪽 도입 규칙은 결론으로 ◇(p₁,…,pₙ)⇒을 내며 전제를 두 부류로 나눕니다. hard premise는 오른쪽 문맥을 더할 수 없고, soft premise는 규칙 도식에서 후건이 비어 있으며, 규칙을 적용할 때 결론과 같은 오른쪽 문맥을 붙일 수 있습니다. 이 차이는 뒤의 Kripke 의미론에서 절대적 진리와 국소적 진리를 나누는 근거가 됩니다.

논문의 함의 왼쪽 도입 규칙에는 두 전제가 있습니다. hard premise ⇒p₁은 p₁이 참이어야 한다는 조건이고, soft premise p₂⇒은 p₂가 거짓이어야 한다는 조건입니다. 오른쪽 도입 규칙에는 p₁⇒p₂라는 전제 하나가 있습니다. 이 절은 p₁이 거짓이거나 p₂가 참이어야 만족됩니다.

세 절을 함께 놓으면 p₁=true, p₂=false가 먼저 정해지지만, 이 대입은 p₁⇒p₂를 만족하지 못합니다. cut 과정도 그대로 따라갈 수 있습니다. 먼저 ⇒p₁과 p₁⇒p₂를 p₁에 대해 잘라 ⇒p₂를 얻고, 이어 ⇒p₂와 p₂⇒을 p₂에 대해 잘라 빈 시퀀트 ⇒를 얻습니다.

입력은 p₁,p₂의 네 대입입니다.

• false, false: ⇒p₁이 실패한다.
• false, true: ⇒p₁과 p₂⇒이 실패한다.
• true, false: ⇒p₁, p₂⇒은 통과하지만 p₁⇒p₂가 실패한다.
• true, true: p₂⇒이 실패한다.

아래 네 버튼은 각 대입에서 미리 계산한 세 전제의 참·거짓을 비교해 보여 줍니다. 네 행 모두 적어도 한 전제를 만족하지 못하므로, 세 전제를 함께 만족하는 대입은 0개입니다. 이것이 이 규칙 쌍이 coherent하다고 판단하는 근거입니다. 버튼은 이 고정된 사례의 설명을 바꾸며, 새로운 규칙을 입력받아 계산하지는 않습니다.

같은 연결사의 왼쪽 규칙 하나와 오른쪽 규칙 하나를 짝지어, 그 쌍의 전제 절을 모두 모읍니다. 가능한 모든 왼쪽·오른쪽 규칙 쌍에서 이 합집합이 고전적으로 모순이어야 그 연결사의 규칙 묶음이 coherent합니다. 왼쪽 규칙이 두 개이고 오른쪽 규칙이 세 개라면 여섯 쌍을 각각 검사합니다. 체계 전체는 모든 연결사의 규칙 묶음이 이 조건을 만족할 때 coherent하다고 부릅니다.

검사의 범위는 분명합니다. 연결사의 실제 모든 복합 공식에 진리값을 붙이는 검사가 아닙니다. 규칙 도식에 등장하는 원자 절들을 유한하게 비교합니다. 그래서 새 연결사 규칙을 설계할 때 쓸 수 있는 구문적 기준이 됩니다.

논문에서 consistency는 서로 다른 두 고정 원자 사이의 시퀀트 q⁺⇒q⁻를 무전제에서 증명할 수 없다는 조건입니다. 여기서 q⁺,q⁻은 독자 혼동을 막기 위해 바꿔 쓴 이름이며, 원문은 p₁,p₂를 사용합니다.

strong consistency는 두 가정 시퀀트 ⇒q⁺와 q⁻⇒에서 빈 시퀀트 ⇒를 유도할 수 없다는 조건입니다. 예 4.7의 체계는 무전제 consistency는 만족하지만 이 두 가정을 허용하면 빈 시퀀트를 유도할 수 있어 strongly consistent하지 않습니다. ⇒q⁺와 q⁻⇒은 여기서 가정이며, 처음부터 무전제로 증명되었다고 전제하지 않습니다.

incoherent하다는 것은 같은 연결사의 왼쪽·오른쪽 규칙 쌍 가운데 적어도 한 쌍에서, 그 전제들을 모두 만족하는 고전 대입 v가 있다는 뜻입니다. 정리 4.10의 치환을 독자용 표기로 다시 쓰면, 규칙 도식의 각 원자 r에 대해 v(r)=true이면 σ(r)=q⁺, v(r)=false이면 σ(r)=q⁻로 둡니다.

대입 v가 전제 절을 만족하므로, 치환된 각 전제는 가정 ⇒q⁺ 또는 q⁻⇒에서 필요한 문맥을 덧붙이는 약화(weakening) 규칙으로 얻을 수 있습니다. 그 전제들에 왼쪽 규칙과 오른쪽 규칙을 각각 적용하면 ◇…⇒과 ⇒◇…을 얻고, 마지막으로 연결사 공식을 cut하여 빈 시퀀트 ⇒를 얻습니다. 따라서 incoherent한 canonical system은 strongly consistent하지 않습니다.

논문이 직접 보이는 결론은 그 체계가 strong consistency를 잃는다는 것입니다. 이미 ⇒φ 하나와 ψ⇒ 하나가 증명된 상황에서는 모든 시퀀트가 증명될 수 있다는 위험도 설명합니다.

하지만 편집부 활동에서 한 행이 살아남았다는 결과만 보고 임의의 실제 체계가 곧바로 모든 문장을 증명한다고 단정하면 안 됩니다. 활동은 원문 정의에 맞춘 규칙 도식의 coherence 검사입니다. 체계의 언어, 허용한 구조 규칙, 실제 유도 관계가 원문의 canonical system 조건을 만족하는지도 확인해야 합니다.

편집부가 만든 이항 연결사 △(A,B)에 다음 규칙을 둡니다. 원문의 새 연결사가 아니라 coherence 정의를 연습하기 위한 사례입니다.

설정 A

• 오른쪽 규칙의 전제: ⇒p₁, ⇒p₂.
• 왼쪽 규칙: hard premise 없음, soft premise p₁,p₂⇒.
• ⇒p₁과 ⇒p₂를 만족하려면 p₁=true, p₂=true여야 하지만 이 대입은 p₁,p₂⇒을 만족하지 못한다.
• 네 대입 가운데 세 절을 모두 만족하는 행은 없으므로 이 규칙 쌍은 coherent하다.

설정 B

• 왼쪽 규칙을 hard premise p₁⇒p₂, soft premise 없음으로 바꾼다.
• 이제 p₁=true, p₂=true가 오른쪽 두 전제와 왼쪽 전제를 모두 만족한다.
• 살아남은 행이 하나 있으므로 이 규칙 쌍은 정의상 incoherent하다.
• 버튼의 고정된 결과 설명은 오른쪽 두 전제가 요구하는 (true,true)에서 세 절이 각각 참인지 거짓인지 보여 줍니다. 다른 세 행은 오른쪽 전제 중 하나를 만족하지 못합니다.

보통 cut-elimination은 무전제에서 증명 가능한 시퀀트에 cut 없는 증명이 존재한다는 성질입니다. strong cut-elimination은 임의의 가정 시퀀트 집합 S에서 결론 s가 증명될 때, 모든 cut formula가 S의 어느 시퀀트엔가 실제로 등장하는 S-proof가 존재한다는 성질입니다.

S=∅이면 허용할 cut formula가 없어 보통의 cut-elimination이 됩니다. S가 비어 있지 않으면 cut을 전부 없애야 한다는 뜻이 아니라, 가정에 나타나지 않은 새 중간 공식을 cut formula로 쓰지 못하게 제한합니다.

비고 6.9는 이 결과를 한 단계 더 강화합니다. 그 정규형에서는 공리, canonical rule, weakening, 그리고 S의 시퀀트를 nucleus로 갖는 hyper-cut만 사용합니다. S-proof의 정의와 이 hyper-cut 정규형은 서로 다른 층으로 읽어야 합니다.

따름정리 6.10은 strong consistency, coherence, strong cut-elimination의 세 조건을 동치로 묶습니다.

strong consistency에서 coherence로 가는 방향은 정리 4.10이 맡습니다. coherence에서 strong cut-elimination으로 가는 방향은 정리 6.8입니다. 이 정리는 건전성·완전성 정리 6.5와, S-proof가 없으면 가정 S를 만족하면서 결론을 반박하는 G-legal frame을 구성한다는 정리 6.3을 사용합니다. strong cut-elimination에서 strong consistency로 돌아가는 방향은 따름정리 6.10의 마지막 논증이 맡습니다. ⇒q⁺, q⁻⇒에서 허용되는 cut formula를 q⁺,q⁻로 제한하면 빈 시퀀트까지 갈 수 없다는 내용입니다.

일반 canonical system에서 다섯 조건이 동치가 아니라는 말은 ordinary consistency와 cut-elimination이 전혀 따라오지 않는다는 뜻이 아닙니다. coherent이면 따름정리 6.10에 따라 strongly consistent하고 strong cut-elimination을 가지므로, ordinary consistency와 cut-elimination도 각각 약한 결과로 따라옵니다. 일반적으로 실패하는 것은 역방향입니다. 예 4.7은 consistency와 cut-elimination을 가지지만 strong consistency, coherence, strong cut-elimination은 갖지 않습니다.

definite clause는 후건이 비어 있지 않고 정확히 하나의 원자를 갖는 원자 시퀀트입니다. definite canonical system은 오른쪽 규칙의 모든 전제와 왼쪽 규칙의 모든 hard premise가 definite clause인 체계입니다. 왼쪽 규칙의 soft premise에는 negative clause가 올 수 있습니다. 이 제한 아래 따름정리 6.14는 다섯 조건을 동치로 묶습니다.

직관주의 Kripke 의미론처럼 세계들은 부분순서로 놓이고, 참은 더 나중 세계로 보존됩니다. 논문은 규칙이 복합식의 값을 하나로 강제하지 않는 경우를 허용합니다.

원문의 weak affirmation ◮을 두 세계에서 살펴봅시다. w₀≤w₁이고 ψ는 w₀에서 거짓, w₁에서 참입니다. 오른쪽 규칙은 현재 세계에서 ψ가 참일 때 ◮ψ를 참으로 강제하지만 w₀에서는 그 조건이 충족되지 않습니다. 왼쪽의 hard premise는 w₀ 이후 모든 세계에서 ψ가 거짓일 때 ◮ψ를 거짓으로 강제하지만 w₁에서 ψ가 참이므로 이 조건도 충족되지 않습니다.

따라서 w₀의 ◮ψ에는 참과 거짓이 모두 허용됩니다. 원자 ψ의 값과 세계 순서는 같은데 복합식 ◮ψ의 값이 다른 두 부분 프레임(semiframe)을 만들 수 있습니다. 여기서 ψ는 하나의 원자식으로 두며, 두 부분 프레임은 ψ와 ◮ψ의 값만 정하고 해당 규칙을 존중합니다. 규칙이 두 값을 모두 강제하는 것이 아니라, 어느 쪽도 강제하지 않는 경우 두 값이 허용되는 비결정성입니다. 두 semiframe은 w₁에서 모두 ◮ψ=true입니다. 차이는 규칙이 어느 값도 강제하지 않는 w₀에서만 생깁니다.

새 연결사를 검사할 때는 먼저 규칙이 canonical 형식을 갖추었는지 확인한 뒤, 같은 연결사의 모든 왼쪽·오른쪽 규칙 쌍에 coherence 검사를 적용합니다. coherent한 체계라면 세 핵심 조건의 동치를 사용할 수 있습니다. 다섯 조건 전체의 동치를 주장하려면 definite 조건도 확인해야 합니다. 아래 네 경우에서 어떤 전제가 주어졌고 어느 정리까지 적용할 수 있는지 구분해 봅시다.

• 조건 A: canonical + coherent, definite 여부 미확인. 결과: 따름정리 6.10에 따라 strong consistency와 strong cut-elimination이 성립한다. ordinary consistency와 cut-elimination도 각각의 약한 결과로 따라가지만, 두 약한 성질에서 coherence로 돌아가는 역방향은 확정할 수 없어 다섯 조건 동치로 표시하지 않는다.
• 조건 B: canonical + coherent + definite. 결과: 따름정리 6.14에 따라 strong consistency, coherence, strong cut-elimination, cut-elimination, consistency의 다섯 조건이 동치다. 이 선택에서는 오른쪽 규칙의 모든 전제와 왼쪽 규칙의 모든 hard 전제가 definite라는 조건을 가정합니다.
• 조건 C: 같은 연결사의 canonical left/right rule 전제를 모두 만족하는 대입이 하나 이상 존재. 결과: 정의 4.3에 따라 incoherent하다. 정리 4.10의 대우에 따라 이 규칙 쌍을 포함한 canonical system은 strongly consistent하지 않다. Q10의 설정 B에서는 (true,true)가 그 대입입니다. Q08처럼 두 원자를 모두 q⁺로 치환하면, 가정에서 양쪽 결론을 얻고 마지막 cut으로 빈 시퀀트에 이릅니다.
• 조건 D: 자연언어 주장을 이 정리에 바로 적용하려는 경우. 결과: 필요한 규칙 형식과 체계 조건이 주어지지 않았으므로 이 정리로 주장의 참·거짓을 판단할 수 없다.