초시퀀트

수학적 논리학에서, 초시퀀트 프레임워크는 구조적인 증명 이론에 사용되는 연속적인 캘커리의 증명 이론적 프레임워크의 확장으로서, 연속적인 프레임워크에서 포착되지 않는 로직들에 대한 분석적인 캘컬리를 제공한다.초시퀀트는 보통 일반 시퀀스의 유한한 다중 집합으로 기록된다.

${\displaystyle \Gamma _{1}\Rightarrow \Delta _{1}\mid \cdots \mid \Gamma _{n}\Rightarrow \Delta _{n}}}}}}$

초시퀀트를 구성하는 시퀀스를 성분이라고 한다.하이퍼시퀀스 프레임워크의 추가 표현성은 중간 논리 LC에 대한 통신 규칙(왼쪽 아래) 또는 모달 논리 S5에 대한 모달 분할 규칙(오른쪽 아래)과 같이 다른 요소들을 조작하는 규칙에 의해 제공된다.^[1]

${\displaystyle {\frac {\Gamma _{1}\Rightarrow \Delta _{1}\mid \dots \mid \Gamma _{n}\Rightarrow \Delta _{n}\mid \Sigma \Rightarrow A\qquad \Omega _{1}\Rightarrow \Theta _{1}\mid \dots \mid \Omega _{m}\Rightarrow \Theta _{m}\mid \Pi \Rightarrow B}{\Gamma _{1}\Rightarrow \Delta _{1}\mid \dots \mid \Gamma _{n}\Rightarrow \Delta _{n}\mid \Omega _{1}\Righarrow \theta _{1}\mid \dots \mid \Oomega _{m}\Rightarrow \mid \Sigma \Rightarrow B\mid \Pi \Rightarrow A}}}}}$ ${\displaystyle {\frac {\Gamma _{1}\Rightarrow \Delta _{1}\mid \dots \mid \Gamma _{n}\Rightarrow \Delta _{n}\mid \Box \Sigma ,\Theta \Rightarrow \Box \Pi ,\Omega }{\Gamma _{1}\Rightarrow \Delta _{1}\mid \dots \mid \Gamma _{n}\Rightarrow \Delta _{n}\mid \Box \Sigma \Rightarrow \Box \Pi \mid \Theta \Rightarrow \Omega }}}$

초시퀀트 캘컬리는 모달 로직, 중간 로직, 하위 구조 로직 치료에 사용되어 왔다.하이퍼시퀀트는 대개 공식 해석을 가지고 있다. 즉, 거의 항상 일종의 분리로서 객체 언어의 공식에 의해 해석된다.정확한 공식 해석은 고려된 논리에 따라 다르다.

공식 정의 및 제안 규칙

형식적으로, 초순은 보통 쓰여진, 보통 순서의 유한한 다중 집합으로 받아들여진다.

${\displaystyle \Gamma _{1}\Rightarrow \Delta _{1}\mid \dots \Mid \Gamma _{n}\Rightarrow \Delta _{n}}}}}}$

초순을 이루는 순서는 다순의 다순의 튜플로 이루어져 있으며, 초순의 성분이라고 불린다.다중 집합 대신 집합이나 리스트의 관점에서 하이퍼시퀀스와 시퀀스를 정의하는 변형도 고려되며, 고려된 논리에 따라 시퀀스는 고전적이거나 직관적일 수 있다.제안적 연결에 대한 규칙은 일반적으로 추가적인 측면 하이퍼시퀀스(hypersequent context)를 가진 해당 표준 시퀀스 규칙의 변형이며, 이를 하이퍼시퀀스 컨텍스트라고도 한다.예: 고전적인 명제 논리를 위한$$ 기능적으로 완전한 연결 장치 집합 {${\displaystyle \mathrm{\perp }}$,${\displaystyle }$→ ${\displaystyle \}}$ ${\displaystyle \{\bot ,\to \}$에 대한 일반적인 규칙 집합은 다음 네 가지 규칙에 의해 주어진다.

${\displaystyle {\frac {}{{\mathcal {G}\mid \Gamma ,p\Rightarrow p,\Delta }}}$

${\displaystyle {\frac {}{{\mathcal {G}\mid \Gamma ,\bot \Rightarrow \Delta}}}$

${\displaystyle {\frac {{\mathcal{G}\mid \Gamma ,B\Rightarrow \Delta \delta \qquad {\mathcal {G}\Delta \{\mathcal {G}}\Mid \Gmad \Mama ,A\to B\Rightarroweightarrowercelta}}}$

${\displaystyle {\frac {{\mathcal {{G}\mid \Gamma ,A\Rightarrow B,\Delta }{{\mathcal {G}\mid \Mad \Rightarrow A\to B,\Delta }}}}}$

초시퀀스 설정의 추가 구조로 인해 구조 규칙은 내부 및 외부 변형에서 고려된다.내부 약화와 내부 수축 규칙은 하이퍼시퀀스 컨텍스트를 추가한 해당 시퀀스 규칙의 적응이다.

${\displaystyle {\frac {{\mathcal{G}\mid \Gamma \Rightarrow \Delta }{{\mathcal {G}\mid \G}\Gigma \Rightarrow \Delta ,\Pi}}}}$

${\displaystyle {\frac {{\mathcal{G}\mid \Gamma ,A,A,\Rightarrow \Delta }{{\mathcal{G}\mid \Mathcal,A\Rightarrow \Delta }}}}}}$

${\displaystyle {\frac {{\mathcal{G}\mid \Gamma \Rightarrow A,A,\Delta }{{\mathcal {G}\mid \Gamma \Rightarrow A,\Delta }}}}$

외부 약화 및 외부 수축 규칙은 공식 대신 초순차 구성 요소 수준에 대한 해당 규칙이다.

${\displaystyle {\frac {\mathcal {G}{\mathcal {G}\mid \감마 \Rightarrow \Delta}}}}$

${\displaystyle {\frac {{\mathcal {G}\Mid \Gamma \Rightarrow \Delta \Mid \G}{\mathcal {G}\Mid \Gama \Rightarrow \Delta }}}}}$

이러한 규칙의 건전성은 거의 항상 어떤 형태의 분리로서 초순구조의 공식 해석과 밀접하게 연관되어 있다.정확한 공식 해석은 고려된 논리에 따라 달라진다. 몇 가지 예는 아래를 참조하라.

주요 예

모달 로직

초시퀀트는 모달 로직의 분석적 석회화를 얻기 위해 사용되어 왔으며, 분석적 연속 석회화는 이해하기 어려운 것으로 판명되었다.모달 로직의 맥락에서 초시퀀트의 표준 공식 해석

${\displaystyle \Gamma _{1}\Rightarrow \Delta _{1}\mid \dots \Mid \Gamma _{n}\Rightarrow \Delta _{n}}}}}}$

공식은

${\displaystyle \Box(\bigwedge \Gamma _{1}\bigvee \Delta _{1}\lor \dots \lor \Box(\bigwedge \Gamma _{n}\bigvee \Delta _{n})}$

Here if ${\displaystyle \Gamma }$ is the multiset ${\displaystyle A_{1},\dots ,A_{n}}$ we write ${\displaystyle \Box \Gamma }$ for the result of prefixing every formula in ${\displaystyle \Gamma }$ with ${\displaystyle \Box }$, i.e., the multiset ${\display$$style \Box$ A_${1$},\$dots$,\$Box$ A_${n$ 단일 구성요소는 시퀀스에 대한 표준 공식 해석을 사용하여 해석되며, 하이퍼시퀀트 막대$∣{\displaystyle \mid}$은(는) 박스를 분리하는 것으로 해석된다는 점에 유의하십시오.초시퀀트가 분석적 미적분을 제공하는 모달 논리의 대표적인 예는 논리 S5이다.이 논리에^[1] 대한 표준 초순 미적분학에서 공식 해석은 위와 같으며, 명제적 규칙과 구조적 규칙은 이전 절의 규칙이다.또한 미적분학에는 모달 규칙이 포함되어 있다.

${\displaystyle {\frac {{\mathcal{G}\mid \Box \Gamma \Rightarrow A}{{\mathcal {G}\mid \Box \Gmd \Box \Gammad \Gamma \Rightarrow \Box A}}}}}}}}$

${\displaystyle {\frac {{\mathcal{G}\mid \Gamma ,A\Rightarrow \Delta}{{\mathcal {G}\mid \G}\Mid \Mathcal,\Box A\Rightarrow \Delta}}}}}}$

${\displaystyle {\frac {{\mathcal {G}\Box \Gamma ,\Sigma \Rightarrow \Box \Delta ,\Pi}{\\\Mathcal {G}}{\Mathcal \Mid \Box \Delta \Sigmad \Rightarrowepi}}}}}}}}}}$

절단 규칙의 적합하게 공식화된 버전의 성능은 유도 구조에 대한 통사적 논거 또는 S5의 의미론을 사용하여 직접 절단 규칙 없이 미적분의 완전성을 보여줌으로써 보여줄 수 있다.모달 논리 S5의 중요성에 따라, 많은 대안적 계산법이 공식화되었다.^{[2][3][1][4][5][6][7]}초시퀀트 캘컬리는 또한 많은 다른 모달 로직에도 제안되었다.^[6][7][8][9]

중간 로직

직감적 또는 단일 분석적 속성에 기초한 초시퀀트 캘컬리는 많은 종류의 중간 로직, 즉 직감적 명제적 논리의 확장을 포착하기 위해 성공적으로 사용되어 왔다.이 설정의 하이퍼시퀀스는 단일 추출된 시퀀스에 기초하므로 다음과 같은 형식을 갖는다.

${\displaystyle \Gamma _{1}\오른쪽 화살표 A_{1}\mid \dots \Mid \Gamma _{n}\오른쪽 화살표 A_{n}}}}$

그러한 초시퀀트에 대한 표준 공식 해석은 다음과 같다.

${\displaystyle(\bigwedge \Gamma _{1}\{1}\lor \dots \lor(\bigwedge \Gamma _{n}\n})}$

중간 로직의 대부분의 초시퀀스 캘커리에는 위에 주어진 제안 규칙의 단일 분석 버전, 즉 구조 규칙의 선택이 포함된다.특정한 중간 논리의 특성은 대부분 다수의 추가 구조 규칙을 사용하여 포착된다.예: 중간 논리 LC에 대한 표준 미적분학(Gödel-Dummett 논리라고도 함)은 다음과 같은 통신 규칙을 추가로 포함한다.^[1]

${\displaystyle {\frac {\Gamma _{1}\Rightarrow \Delta _{1}\mid \dots \mid \Gamma _{n}\Rightarrow \Delta _{n}\mid \Sigma \Rightarrow A\qquad \Omega _{1}\Rightarrow \Theta _{1}\mid \dots \mid \Omega _{m}\Rightarrow \Theta _{m}\mid \Pi \Rightarrow B}{\Gamma _{1}\Rightarrow \Delta _{1}\mid \dots \mid \Gamma _{n}\Rightarrow \Delta _{n}\mid \Omega _{1}\Righarrow \theta _{1}\mid \dots \mid \Oomega _{m}\Rightarrow \mid \Sigma \Rightarrow B\mid \Pi \Rightarrow A}}}}}$

많은 다른 중간 로직들을 위한 초시퀀트 캘컬리가 도입되었고,^{[1][10][11][12]} 그러한 캘컬리의 컷 탈락에 대한 매우 일반적인 결과가 있다.^[13]

하부 구조 로직

중간 로직의 경우, 많은 하위 구조 로직과 퍼지 로직의 분석적 계산법을 얻기 위해 초시퀀트를 사용해 왔다.^[1][13][14]

역사

초순구조는 모달 논리 S5에 대한 미적분을 얻기 위해 코테지라는 이름으로 먼저 등장한^[2] 것으로 보인다.모달 로직을 ^[3]치료하기 위해서도, 모달 로직, 중간 및 하부구조 로직의 캘컬리를 고려하고,^[1] 초시퀀트라는 용어를 도입하는 영향력 있는 곳에서도 독자적으로 개발된 것으로 보인다.

참조