구조증거이론

수학적 논리학에서 구조적 증명 이론은 분석적 입증의 개념을 지지하는 증명 캘커리를 연구하는 증명 이론의 하위 학문으로서 의미적 특성이 노출되는 증거의 일종이다.구조적 증명 이론에서 공식화된 논리의 모든 이론이 분석적 증거를 가지고 있을 때, 증명 이론은 일관성 같은 것을 증명하고, 의사결정 절차를 제공하며, 수학적 또는 계산적 증인들이 이론의 상대자로서 추출될 수 있도록 하는데 사용될 수 있는데, 이것은 모델 th에 더 자주 주어지는 종류의 작업이다.어리의

분석증거

분석적 증거의 개념은 게르하르트 겐첸에 의해 증명 이론에 도입되었다. 분석적 증거는 절삭되지 않은 것이다.그의 자연적 추론 미적분학 또한 Dag Prawitz에서 보여지듯이 분석적 증명의 개념을 지지한다. 정의는 약간 더 복잡하다. 분석적 증명은 정상적인 형태로서 용어 재작성에서 정상적인 형태의 개념과 관련이 있다.

구조 및 연결 장치

구조 증명 이론의 용어 구조는 순차 미적분학에서 도입된 기술적 개념에서 유래한다: 연속 미적분학은 구조 연산자라 불리는 특수하고, 초논리적 연산자를 사용하여 추론하는 모든 단계에서 이루어진 판단을 나타낸다: $A_{1},\dots ,A_{m}\vdash B_{1},\dots ,B_{n}$ $A_{1},\dots ,A_{m}\vdash B_{1},\dots ,B_{n}$ , $A_{1},\dots ,A_{m}\vdash B_{1},\dots ,B_{n}$ … , $A_{1},\dots ,A_{m}\vdash B_{1},\dots ,B_{n}$ $A_{1},\dots ,A_{m}\vdash B_{1},\dots ,B_{n}$ $A_{1},\dots ,A_{m}\vdash B_{1},\dots ,B_{n}$ $A_{1},\dots ,A_{m}\vdash B_{1},\dots ,B_{n}$ $A_{1},\dots ,A_{m}\vdash B_{1},\dots ,B_{n}$ , $A_{1},\dots ,A_{m}\vdash B_{1},\dots ,B_{n}$ … $A_{1},\dots ,A_{m}\vdash B_{1},\dots ,B_{n}$ , $A_{1},\dots ,A_{m}\vdash B_{1},\dots ,B_{n}$ n ${\$ $대시 B_{1},\dots ,B_{n}},$ 개찰구 왼쪽에 있는 쉼표는 보통 연산자로, 우측에 있는 쉼표는 분리형으로 해석되는 연산자로, 개찰구 기호 자체는 함축적으로 해석된다.단, 이러한 연산자와 그 연산자가 해석하는 논리 결합체 사이에 근본적인 행동 차이가 있다는 점에 유의해야 한다. 즉, 구조 연산자는 미적분학의 모든 규칙에서 사용되며, 보조공식 속성이 적용되는지 여부를 물을 때는 고려하지 않는다.나아가 논리적인 규칙은 오직 한 가지 방향으로만 진행되는데, 논리적인 구조는 논리적인 규칙에 의해 도입되며, 한 번 창조된 후에는 제거할 수 없는 반면, 구조적인 운영자는 파생 과정에서 도입되고 제거될 수 있다.

시퀀스의 통사적 특징을 특별하고 비논리적 연산자로 보는 발상은 오래되지 않았으며, 증명 이론의 혁신에 의해 강요되었다: 구조 연산자가 겟젠의 원래 시퀀스 미적분학에서처럼 단순할 때는 그들을 분석할 필요가 거의 없지만 표시 논리(Nue가 소개함)와 같은 깊은 추론의 증명(proof calculi)이 있다.1982년 l Belnap)^[1]는 구조 연산자를 논리 결합체처럼 복잡하게 지원하며, 정교한 처리를 요구한다.

시퀀스 미적분에서의 절단 제거

자연공제 및 형식별 대응방식

논리적 이중성과 조화

초시퀀트

하이퍼시퀀트 프레임워크는 일반적인 시퀀스 구조를 다수의 시퀀스까지 확장하며, 다른 시퀀스를 분리하기 위해 추가 구조 결합체(초시퀀트 막대라고 함)를 사용한다.그것은 모달, 중간 및 하부구조 로직^[2]^[3]^[4] 등에 대한 분석적 석회화 제공에 사용되어 왔다. 초시퀀트는 구조물이다.

$\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}}}}}$

여기서 각 $\Gamma _{i}\vdash \Delta _{i}$ $\Gamma _{i}\vdash \Delta _{i}$ i ${\$ 는 초시퀀트의 성분이라 불리는 일반적인 시퀀스다 $\Gamma _{i}\vdash \Delta _{i}$ .시퀀스의 경우, 하이퍼 시퀀스는 세트, 멀티셋 또는 시퀀스에 기초할 수 있으며, 구성요소는 단일 컨버전스 또는 다중 컨버전스 시퀀스일 수 있다.초계열성의 공식 해석은 고려 중인 논리에 따라 다르지만, 거의 항상 어떤 형태로든 분리되어 있다.가장 일반적인 해석은 단순한 구분이다.

${\displaystyle(\bigwedge \Delta _{1}\오른쪽 화살표 \bigvee \Delta _{1}\lor \dots \lor(\bigwedge \Gamma _{n}\오른쪽 화살표 \bigbigvee \Delta _{n}}})}$

중간 로직의 경우 또는 상자의 분리용

${\displaystyle \Bigwedge \Gama _{1}\오른쪽 화살표 \bigvee \Delta _{1}\lor \dots \lor \Box(\bigwedge \Gama _{n}\오른쪽 화살표 \bigvee \Delta _{n})$

모달 로직의 경우

초시퀀트 막대의 이항 해석에 맞추어, 본질적으로 모든 초시퀀트 캘컬리는 외부 구조 규칙, 특히 외부 약화 규칙을 포함한다.

${\frac {\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}}{\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}\mid \Sigma \vdash \Pi }}$

외부 수축 규칙

${\frac {\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}\mid \Gamma _{n}\vdash \Delta _{n}}{\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}}}$

초시퀀스 프레임워크의 추가 표현성은 초시퀀스 구조를 조작하는 규칙에 의해 제공된다.중요한 예는 변조된 분할 규칙에^[3] 의해 제공된다.

${\frac {\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}\mid \Box \Sigma ,\Omega \vdash \Box \Pi ,\Theta }{\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}\mid \Box \Sigma \vdash \Box \Pi \mid \Omega \vdash \Theta }}$

모달 로직 $\Box \Sigma$ 의 경우, 여기서 $\Box \Sigma$ \ $\Box \Sigma$ 은(는) $\Box \Sigma$ ◻ $\Box \Sigma$ 의 모든 공식이 $\Box A$ A ${\displaysty \Box A}$ 형식임을 $\Box \Sigma$ 의미한다 $\Box \Sigma$ $\Box A$

또 다른 예는 중간 논리^[3] LC에 대한 통신 규칙에 의해 제시된다.

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

통신 규칙에서 구성 요소는 단일 결합 시퀀스라는 점에 유의하십시오.

구조물의 미적분학

내포된 시퀀스 미적분학

내포된 연속 미적분은 구조물의 양면 미적분과 닮은 공식화다.

메모들

^ N. D. 벨납."Display Logic." 철학적 논리학 저널, 11(4), 375–417, 1982.
^ Minc, G.E. (1971) [Originally published in Russian in 1968]. "On some calculi of modal logic". The Calculi of Symbolic Logic. Proceedings of the Steklov Institute of Mathematics. AMS. 98: 97–124.
^ ^a ^b ^c Avron, Arnon (1996). "The method of hypersequents in the proof theory of propositional non-classical logics" (PDF). Logic: From Foundations to Applications: European Logic Colloquium. Clarendon Press: 1–32.
^ Pottinger, Garrel (1983). "Uniform, cut-free formulations of T, S4, and S5". Journal of Symbolic Logic. 48 (3): 900. doi:10.2307/2273495. JSTOR 2273495.

참조

Sara Negri; Jan Von Plato (2001). Structural proof theory. Cambridge University Press. ISBN 978-0-521-79307-0.
Anne Sjerp Troelstra; Helmut Schwichtenberg (2000). Basic proof theory (2nd ed.). Cambridge University Press. ISBN 978-0-521-77911-1.

[1] N. D. 벨납."Display Logic." 철학적 논리학 저널, 11(4), 375–417, 1982.

[2] Minc, G.E. (1971) [Originally published in Russian in 1968]. "On some calculi of modal logic". The Calculi of Symbolic Logic. Proceedings of the Steklov Institute of Mathematics. AMS. 98: 97–124.

[:0-3] Avron, Arnon (1996). "The method of hypersequents in the proof theory of propositional non-classical logics" (PDF). Logic: From Foundations to Applications: European Logic Colloquium. Clarendon Press: 1–32.

[4] Pottinger, Garrel (1983). "Uniform, cut-free formulations of T, S4, and S5". Journal of Symbolic Logic. 48 (3): 900. doi:10.2307/2273495. JSTOR 2273495.

[1]

[2]

[3]

[4]

Search