시퀀트 계산

3. 시퀀트 계산

시퀀트 계산은 시퀀트를 이용한 형식적 연역 논증 수법의 일종이다. 이는 이미 제시된 조건적(무조건적에 대비되는) 항진식들로부터, 정해진 추론 규칙을 통해 또다른 조건적 항진식을 도출해나가는 방식이다.^[1] 증명론과 수학적 논리에서, 시퀀트 계산은 특정 추론 방식과 특정 형식적 속성을 공유하는 일련의 형식 시스템이다.

시퀀트 계산은 자연 연역 판단의 형식을 다음과 같이 일반화한다.

:$A\_1,\; \backslash ldots,\; A\_n\; \backslash vdash\; B\_1,\; \backslash ldots,\; B\_k,$

이것을 시퀀트라고 하는 구문 객체이다. 턴스타일의 왼쪽에 있는 공식들은 ''전항(antecedent)''이라고 불리며, 오른쪽에 있는 공식들은 ''후항(succedent)'' 또는 ''결론(consequent)''이라고 불린다. 이들을 통틀어 ''케덴트(cedents)'' 또는 ''시퀀트(sequents)''라고 부른다.^[12]

$A\_i$와 $B\_i$는 공식이고, $n$과 $k$는 음이 아닌 정수이다. 즉, 왼쪽 또는 오른쪽(또는 둘 다 아님)이 비어 있을 수 있다. 자연 연역에서와 마찬가지로, 정리는 $\backslash vdash\; B$가 유효한 증명의 결론인 $B$이다.

시퀀트의 표준 의미론은 ''모든'' $A\_i$가 참일 때, ''적어도 하나''의 $B\_i$도 참이 될 것이라는 단언이다.^[13] 따라서, 두 케덴트가 모두 비어 있는 빈 시퀀트는 거짓이다.^[14]

고전적 맥락에서 시퀀트의 의미론은 다음과 같이 표현될 수 있다.

::$\backslash vdash\; \backslash neg\; A\_1\; \backslash lor\; \backslash neg\; A\_2\; \backslash lor\; \backslash cdots\; \backslash lor\; \backslash neg\; A\_n\; \backslash lor\; B\_1\; \backslash lor\; B\_2\; \backslash lor\backslash cdots\backslash lor\; B\_k$

(A 중 적어도 하나가 거짓이거나, B 중 하나가 참이다)

또는 다음과 같이 표현될 수 있다.

::$\backslash vdash\; \backslash neg(A\_1\; \backslash land\; A\_2\; \backslash land\; \backslash cdots\; \backslash land\; A\_n\; \backslash land\; \backslash neg\; B\_1\; \backslash land\; \backslash neg\; B\_2\; \backslash land\backslash cdots\backslash land\; \backslash neg\; B\_k)$

(모든 A가 참이고 모든 B가 거짓인 경우는 있을 수 없다).

이러한 공식에서, 턴스타일의 어느 쪽에 있는 공식이든 유일한 차이점은 한쪽이 부정된다는 것이다. 따라서 시퀀트에서 왼쪽을 오른쪽으로 바꾸는 것은 구성 공식을 모두 부정하는 것에 해당한다. 이는 드 모르간의 법칙과 같은 대칭성이 의미론적 수준에서 논리적 부정으로 나타나며, 시퀀트의 좌우 대칭으로 직접 변환된다는 것을 의미한다.

시퀀트 계산에서는 시퀀트의 열로 증명이 기술되며, 각 시퀀트는 증명 과정에서 이미 출현한 시퀀트에 후술하는 추론 규칙을 적용하여 도출된다.

3. 1. LK 체계

3. 1. 1. 논리 규칙

• 가로줄 위의 논리식에서 가로줄 아래의 논리식이 도출된다.
• $\backslash vdash$ (턴스타일)은 좌측의 '가정'과 우측의 '진술'을 구분한다.
• $A$와 $B$는 1차 술어 논리의 논리식이다. (명제 논리로 한정될 수 있다.)
• $\backslash Gamma,\; \backslash Delta,\; \backslash Sigma,\; \backslash Pi$는 논리식의 유한한 열(0개 가능)로, '문맥'이라고 한다.
• $\backslash vdash$ 좌측의 논리식들은 논리곱으로 연결된다.
• $\backslash vdash$ 우측의 논리식들은 논리합으로 연결된다.
• $t$는 임의의 항이다.
• $x$와 $y$는 변수이다.
• $\backslash forall$ (전칭 양화사)나 $\backslash exists$ (존재 양화사)에 종속되지 않은 변수를 자유 변수라고 한다.
• $A[t]$는 항 $t$에 주목한 논리식 $A$이다.
• $A[s/t]$는 $A[t]$ 내의 특정 $t$를 항 $s$로 치환한 논리식이다.
• $WL$와 $WR$는 ''Weakening Left/Right''(약화 좌/우), $CL$와 $CR$는 ''Contraction''(축약), $PL$와 $PR$는 ''Permutation''(순열)의 약자이다.

제약: $(\{\backslash forall\}R)$ 및 $(\{\backslash exists\}L)$ 규칙에서 변수 $y$는 $\backslash Gamma$, $A[x/y]$, $\backslash Delta$에서 자유롭지 않다.

위 규칙은 논리 규칙과 구조 규칙으로 나뉜다. 논리 규칙은 $\backslash vdash$의 좌변 또는 우변에 새로운 논리식을 도입하고, 구조 규칙은 시퀀트의 구조를 조작한다. 단, 동일성 공리(I)와 컷 규칙(Cut)은 예외이다.
컷 규칙은 논리식 $A$가 귀결인 동시에 다른 귀결의 전제가 될 때, $A$를 제외하고 논리적 귀결 관계를 결합할 수 있음을 보인다. 자름-제거 정리는 컷 규칙을 사용한 증명이 컷 규칙을 사용하지 않고도 증명될 수 있음을 보장한다.

3. 1. 2. 구조 규칙

• 약화 (Weakening): 시퀀트에 임의의 논리식을 추가한다.
• 좌변 약화 (WL): $\backslash cfrac\{\backslash Gamma\; \backslash vdash\; \backslash Delta\}\{\backslash Gamma,\; A\; \backslash vdash\; \backslash Delta\}$
• 우변 약화 (WR): $\backslash cfrac\{\backslash Gamma\; \backslash vdash\; \backslash Delta\}\{\backslash Gamma\; \backslash vdash\; A,\; \backslash Delta\}$
• 직관적 설명:
• 좌변: 전제에 논리식을 추가해도 결론은 변하지 않는다. (예: 모든 자동차가 바퀴를 가진다면, 모든 검은색 자동차도 바퀴를 가진다.)
• 우변: 결론에 논리식을 추가하면 적어도 하나가 참이 될 가능성이 유지된다. (예: 모든 자동차가 바퀴를 가진다면, 모든 자동차는 바퀴 또는 날개를 가진다.)
• 축약 (Contraction): 시퀀트 내에서 동일한 논리식을 하나로 합친다.
• 좌변 축약 (CL): $\backslash cfrac\{\backslash Gamma,\; A,\; A\; \backslash vdash\; \backslash Delta\}\{\backslash Gamma,\; A\; \backslash vdash\; \backslash Delta\}$
• 우변 축약 (CR): $\backslash cfrac\{\backslash Gamma\; \backslash vdash\; A,\; A,\; \backslash Delta\}\{\backslash Gamma\; \backslash vdash\; A,\; \backslash Delta\}$
• 직관적 설명: 같은 논리식이 여러 번 나타나도 한 번 나타난 것과 같은 의미를 가진다.
• 순열 (Permutation): 시퀀트 내 논리식의 순서를 바꾼다.
• 좌변 순열 (PL): $\backslash cfrac\{\backslash Gamma\_1,\; A,\; B,\; \backslash Gamma\_2\; \backslash vdash\; \backslash Delta\}\{\backslash Gamma\_1,\; B,\; A,\; \backslash Gamma\_2\; \backslash vdash\; \backslash Delta\}$
• 우변 순열 (PR): $\backslash cfrac\{\backslash Gamma\; \backslash vdash\; \backslash Delta\_1,\; A,\; B,\; \backslash Delta\_2\}\{\backslash Gamma\; \backslash vdash\; \backslash Delta\_1,\; B,\; A,\; \backslash Delta\_2\}$
• 직관적 설명: 시퀀트 내 논리식의 순서는 의미에 영향을 주지 않는다.

3. 2. LJ 체계

4. 시퀀트 계산을 이용한 증명

시퀀트 계산은 분석적 타블로 방법과 유사하게 명제 논리의 공식을 증명하는 도구로 사용될 수 있다.^[20] 이는 논리 공식을 증명하는 문제를 더 간단한 공식으로 줄여나가, 최종적으로는 가장 간단한 공식에 도달하게 하는 일련의 단계를 제공한다.^[20]

이 증명 과정은 루트 트리를 통해 시각적으로 표현할 수 있다. 이 트리의 루트는 증명하고자 하는 공식이며, 리프(leaf)는 원자 공식만으로 구성된다. 이러한 트리를 '''환원 트리'''라고 부른다.^[4][22]

증명 과정은 명제 논리의 임의의 공식에서 시작하여, 턴스타일의 오른쪽을 원자 기호만 포함할 때까지 위 규칙에 따라 처리한다. 그 후, 왼쪽도 동일하게 처리한다. 모든 논리 연산자는 위의 규칙 중 하나에 의해 제거되므로, 논리 연산자가 남지 않으면 증명 과정이 종료된다. 즉, 공식이 완전히 ''분해''된 것이다.

결과적으로 트리의 리프에 있는 시퀀스는 원자 기호만으로 구성되며, 이 시퀀스가 공리적으로 증명 가능한지 여부는 오른쪽에 있는 기호 중 하나가 왼쪽에 나타나는지에 따라 결정된다.

트리의 각 단계에서 분기가 발생할 때마다, 서로 다른 분기 사이에는 논리곱이 존재하는 것으로 이해된다. 따라서 각 단계는 해당 단계에 의해 함의되는 공식의 의미론적 진리값을 보존한다. 또한, 공리는 원자 기호에 대한 모든 진리값 할당에 대해 참인 경우에만 증명 가능하다. 결론적으로, 이 시스템은 고전적 명제 논리에 대해 건전성 및 완전성 (논리)을 만족한다.

5. 힐베르트 시스템, 자연 연역과의 비교

힐베르트 스타일의 추론 시스템은 가장 단순한 형식의 판단을 사용하는데, 이 판단은 다음과 같은 형태를 띤다.^[1]

:$B$

여기서 $B$는 공식이다. 이러한 단순성으로 인해, 완전한 형식적 증명은 매우 길어지는 경향이 있다. 따라서, 힐베르트 시스템에서의 증명에 대한 구체적인 논증은 거의 항상 추론 정리에 의존한다.

자연 연역에서는 다음과 같은 형태의 판단을 사용한다.^[8][9][10]

:$A\_1,\; A\_2,\; \backslash ldots,\; A\_n\; \backslash vdash\; B$

여기서 $A\_i$와 $B$는 공식이며, $n\backslash geq\; 0$이다. 즉, 판단은 턴스타일 기호 "$\backslash vdash$" 왼쪽에 있는 공식 목록(비어 있을 수 있음)과 오른쪽에 있는 단일 공식으로 구성된다. 자연 연역에서 판단의 표준 의미는^[11] $A\_1$, $A\_2$ 등이 모두 참일 때 $B$도 참이 된다는 것을 주장하는 것이다.

시퀀트 계산은 자연 연역 판단을 일반화하여 다음과 같은 형태를 사용한다.^[12]

:$A\_1,\; \backslash ldots,\; A\_n\; \backslash vdash\; B\_1,\; \backslash ldots,\; B\_k$

이것을 시퀀트라고 하는 구문 객체이다. 턴스타일의 왼쪽에 있는 공식들은 ''전항(antecedent)''이라고 불리며, 오른쪽에 있는 공식들은 ''후항(succedent)'' 또는 ''결론(consequent)''이라고 불린다. $A\_i$와 $B\_i$는 공식이고, $n$과 $k$는 음이 아닌 정수이다. 즉, 왼쪽 또는 오른쪽(또는 둘 다 아님)이 비어 있을 수 있다.

시퀀트의 표준 의미는 ''모든'' $A\_i$가 참일 때, ''적어도 하나''의 $B\_i$도 참이 될 것이라는 주장이다.^[13] 고전적 맥락에서 시퀀트의 의미는 다음과 같이 표현될 수 있다.

::$\backslash vdash\; \backslash neg\; A\_1\; \backslash lor\; \backslash neg\; A\_2\; \backslash lor\; \backslash cdots\; \backslash lor\; \backslash neg\; A\_n\; \backslash lor\; B\_1\; \backslash lor\; B\_2\; \backslash lor\backslash cdots\backslash lor\; B\_k$

(A 중 적어도 하나가 거짓이거나, B 중 하나가 참이다)

또는 다음과 같이 표현될 수 있다.

::$\backslash vdash\; \backslash neg(A\_1\; \backslash land\; A\_2\; \backslash land\; \backslash cdots\; \backslash land\; A\_n\; \backslash land\; \backslash neg\; B\_1\; \backslash land\; \backslash neg\; B\_2\; \backslash land\backslash cdots\backslash land\; \backslash neg\; B\_k)$

(모든 A가 참이고 모든 B가 거짓인 경우는 있을 수 없다).

이러한 공식에서, 턴스타일 양쪽에 있는 공식의 유일한 차이점은 한쪽이 부정된다는 것이다. 이는 드 모르간의 법칙과 같은 대칭성이 의미론적 수준에서 논리적 부정으로 나타나며, 시퀀트의 좌우 대칭으로 변환됨을 의미한다. 많은 논리학자들은 이러한 대칭적 표현이 논리의 구조에 대한 더 깊은 통찰력을 제공한다고 생각한다.

겐첸(Gentzen)은 단일 출력 자연 연역 시스템(NK와 NJ)과 다중 출력 시퀀트 계산 시스템(LK와 LJ) 사이의 뚜렷한 구분을 주장했다. 그는 직관주의적 자연 연역 시스템 NJ가 다소 보기 좋지 않다고 언급했으며,^[15] 고전 자연 연역 시스템 NK에서 배중률이 갖는 특별한 역할이 고전 시퀀트 계산 시스템 LK에서는 제거된다고 말했다.^[16] 또한 시퀀트 계산 LJ가 직관주의 논리의 경우뿐만 아니라 고전 논리(LK 대 NK)의 경우에도 자연 연역 NJ보다 더 많은 대칭성을 제공한다고 말했다.^[17]

6. 부분 구조 논리

구조 규칙의 일부 사용을 제한하거나 금지하여 다양한 부분구조 논리 시스템을 생성할 수 있다. 이들은 일반적으로 LK보다 약하며(즉, 정리가 더 적음), 따라서 일차 논리의 표준 의미론에 대해 완전하지 않다. 그러나 이론 컴퓨터 과학 및 인공 지능 분야에 적용될 수 있는 다른 흥미로운 속성을 가지고 있다.^[12] 선형 논리가 대표적인 예시이다.

구조 규칙에 대해서는 조금 더 설명이 필요하다. 규칙의 명칭은 ''Weakening''(W), ''Contraction''(C), ''Permutation''(P)이며, 일본어로는 각각 '약화 규칙', '축약 규칙', '전치 규칙'이라고 한다.

• 약화 규칙 (Weakening, W): 시퀀스에 임의의 요소를 추가할 수 있도록 한다. 직관적으로 전제에 무언가를 더하는 것은 증명에서도 자주 있는 일로 자연스럽다. 결론은 요소의 논리합이므로, 둘 중 하나라도 성립하면 되므로, 증명되지 않은 식을 추가해도 성립한다.

• 축약 규칙 (Contraction, C): 시퀀스 요소의 발생 횟수가 중요하지 않음을 나타낸다.

• 순열 규칙 (Permutation, P): 시퀀스 요소의 순서가 중요하지 않음을 보장한다.

7. 시퀀트 계산의 활용 및 의의

증명론과 수학적 논리에서 시퀀트 계산은 특정 추론 방식과 형식적 속성을 공유하는 일련의 형식 시스템이다. 1934/1935년에 게르하르트 겐첸^[1]은 자연 연역을 일차 논리에서 연구하기 위한 도구로 최초의 시퀀트 계산 시스템인 '''LK'''와 '''LJ'''를 도입하였다(각각 고전 논리와 직관 논리 버전). 겐첸의 "주요 정리"(''Hauptsatz'')는 LK와 LJ에 대한 컷 제거 정리^[2][3]였으며, 이는 일관성을 포함하여 광범위한 메타이론적 결과를 가져왔다. 겐첸은 이후 컷 제거 논증을 적용하여 (초한) 페아노 산술의 무모순성 증명을 제공함으로써 이 기술의 힘과 유연성을 입증했으며, 이는 괴델의 불완전성 정리에 대한 놀라운 반응이었다. 이 초기 연구 이후, '''겐첸 시스템'''이라고도 불리는 시퀀트 계산^[4][5][6][7]과 이에 관련된 개념은 증명론, 수학적 논리 및 자동 증명 분야에서 널리 사용되어 왔다.

시퀀트 계산은 자연 연역 판단의 형식 $A\_1,\; \backslash ldots,\; A\_n\; \backslash vdash\; B\_1,\; \backslash ldots,\; B\_k,$를 일반화한 시퀀트라는 구문 객체를 사용한다. 턴스타일 왼쪽에 있는 공식은 ''전항(antecedent)'', 오른쪽에 있는 공식은 ''후항(succedent)'' 또는 ''결론(consequent)''이라고 불린다. 이들을 통틀어 ''케덴트(cedents)'' 또는 ''시퀀트(sequents)''라고 부른다.^[12] $A\_i$와 $B\_i$는 공식이고, $n$과 $k$는 음이 아닌 정수이다. 왼쪽 또는 오른쪽이 비어 있을 수도 있다. 자연 연역에서와 마찬가지로, 정리는 $\backslash vdash\; B$가 유효한 증명의 결론인 $B$이다.

시퀀트의 표준 의미는 ''모든'' $A\_i$가 참일 때, ''적어도 하나''의 $B\_i$도 참이 된다는 것이다.^[13] 따라서, 두 케덴트가 모두 비어 있는 빈 시퀀트는 거짓이다.^[14] 턴스타일 왼쪽에 있는 쉼표는 "그리고"로, 턴스타일 오른쪽에 있는 쉼표는 (포괄적인) "또는"으로 생각할 수 있다. 시퀀트 $A\_1,\; \backslash ldots,\; A\_n\; \backslash vdash\; B\_1,\; \backslash ldots,\; B\_k$과 $\backslash vdash\; (A\_1\; \backslash land\backslash cdots\backslash land\; A\_n)\backslash rightarrow(B\_1\; \backslash lor\backslash cdots\backslash lor\; B\_k)$는 어느 시퀀트의 증명이라도 다른 시퀀트의 증명으로 확장될 수 있다는 점에서 동등하다.

고전적 맥락에서 시퀀트의 의미는 (A 중 적어도 하나가 거짓이거나, B 중 하나가 참이다)를 나타내는 $\backslash vdash\; \backslash neg\; A\_1\; \backslash lor\; \backslash neg\; A\_2\; \backslash lor\; \backslash cdots\; \backslash lor\; \backslash neg\; A\_n\; \backslash lor\; B\_1\; \backslash lor\; B\_2\; \backslash lor\backslash cdots\backslash lor\; B\_k$ 또는 (모든 A가 참이고 모든 B가 거짓인 경우는 있을 수 없다)를 나타내는 $\backslash vdash\; \backslash neg(A\_1\; \backslash land\; A\_2\; \backslash land\; \backslash cdots\; \backslash land\; A\_n\; \backslash land\; \backslash neg\; B\_1\; \backslash land\; \backslash neg\; B\_2\; \backslash land\backslash cdots\backslash land\; \backslash neg\; B\_k)$로 표현될 수 있다.

이 공식에서 턴스타일 양쪽에 있는 공식의 유일한 차이점은 한쪽이 부정된다는 것이다. 시퀀트에서 왼쪽을 오른쪽으로 바꾸는 것은 구성 공식을 모두 부정하는 것에 해당한다. 이는 드 모르간의 법칙과 같은 대칭성이 의미론적 수준에서 논리적 부정으로 나타나며, 시퀀트 좌우 대칭으로 변환된다는 것을 의미한다. 시퀀트 계산에서 결합(∧)을 처리하기 위한 추론 규칙은 분리(∨)를 처리하는 규칙의 거울상이다.

많은 논리학자들은 이러한 대칭적 표현이 규칙에서 고전적 부정의 이중성이 덜 명확한 다른 스타일의 증명 시스템보다 논리의 구조에 대한 더 깊은 통찰력을 제공한다고 생각한다.

7. 1. 전산학 분야에서의 응용

참조

_[1] 간행물
_[2] 간행물
_[3] 간행물
_[4] 간행물
_[5] 간행물
_[6] 간행물
_[7] 간행물
_[8] 간행물
_[9] 간행물
_[10] 간행물
_[11] 문서 Here, "whenever" is used as an informal abbreviation "for every assignment of values to the free variables in the judgment"
_[12] 웹사이트 PVS Prover Guide http://pvs.csl.sri.c[...] SRI International 2015-05-29
_[13] 간행물
_[14] 간행물
_[15] 간행물
_[16] 간행물
_[17] 간행물
_[18] 간행물
_[19] 간행물
_[20] 웹사이트 Applied Logic, Univ. of Cornell: Lecture 9 http://www.cs.cornel[...] 2016-06-25
_[21] Youtube Remember, the way that you prove an implication is by assuming the hypothesis. https://www.youtube.[...] 2015-11-02
_[22] 서적 Gentzen's Centenary: The Quest for Consistency Springer
_[23] 서적 Elements of Logical Reasoning Cambridge University Press
_[24] 웹사이트 An Introduction to the Theory and Applications of Propositional Sequent Calculi https://link.springe[...] 2022-08-03
_[25] 간행물
_[26] 간행물
_[27] 간행물
_[28] 논문 Proving unprovability IEEE