구조 규칙

이 글에는 출처가 없다 신뢰할 수 있는 출처에 인용문을 추가하여 이 기사를 개선할 수 있도록 도와주십시오. 공급되지 않은 재료는 도전하여 제거할 수 있다. 출처 찾기: "구조적 규칙" – 뉴스 · 신문 · 책 · 학자 · JSTOR (2009년 12월) (이 템플릿 메시지를 제거하는 방법과 시기 학습)

증명 이론에서 구조 법칙은 어떤 논리적 결합을 지칭하지 않고 그 대신 판단이나 속편에 직접 작용하는 추론 규칙이다. 구조 규칙은 종종 논리의 의도된 메타-이론적 특성을 모방한다. 구조 규칙 중 하나 이상을 거부하는 로직은 하부구조 로직으로 분류된다.

공통구조규칙

세 가지 일반적인 구조 규칙은 다음과 같다.

• 약화, 추가 구성원과 함께 가설이나 연속체의 결론이 확장될 수 있는 경우. In symbolic form weakening rules can be written as ${\displaystyle {\frac {\Gamma \vdash \Sigma }{\Gamma ,A\vdash \Sigma }}}$ on the left of the turnstile, and ${\displaystyle {\frac {\Gamma \vdash \Sigma }{\Gamma \vdash \Sigma ,A}}}$ on the right.
• 연속체의 같은 쪽에 있는 두 개의 동일(또는 불가능) 멤버가 단일 멤버(또는 공통 인스턴스)로 대체될 수 있는 수축. Symbolically: ${\displaystyle {\frac {\Gamma ,A,A\vdash \Sigma }{\Gamma ,A\vdash \Sigma }}}$ and ${\displaystyle {\frac {\Gamma \vdash A,A,\Sigma }{\Gamma \vdash A,\Sigma }}}$. Also known as factoring in automated theorem proving systems using resolution. 고전적 논리학에서 관여의 전위성으로 알려져 있다.
• 교환, 시퀀스의 같은 쪽에 있는 두 멤버를 교환할 수 있다. Symbolically: ${\displaystyle {\frac {\Gamma _{1},A,\Gamma _{2},B,\Gamma _{3}\vdash \Sigma }{\Gamma _{1},B,\Gamma _{2},A,\Gamma _{3}\vdash \Sigma }}}$ and ${\disp$$laystyle {\frac {\Gamma \vdash \Sigma _{1},A,\Sigma _{2},B,\Sigma _{3}}{\Gamma \vdash \Sigma _{1},B,\Sigma _{2},A,\Sigma _{3}}}}$. (This is also known as the permutation rule.)

위의 구조 규칙 중 어느 것도 없는 논리는 시퀀스의 측면을 순수한 시퀀스로 해석할 수 있고, 교환과 함께 그것들은 다중 집합이며, 수축과 교환 모두 집합이다.

이것들만이 가능한 구조 규칙이 아니다. 유명한 구조 규칙은 절단이라고 알려져 있다. 다양한 논리학에서 삭감된 규칙이 불필요하다는 것을 증명 이론가들에 의해 상당한 노력을 기울인다. 좀 더 정확히 말하면, 보이는 것은 컷은 증거를 완화하는 도구일 뿐, 증명될 수 있는 이론에는 추가되지 않는다는 것이다. 절단 제거라고 알려진 절단 규칙의 성공적인 '제거'는 정상화로 계산하는 철학과 직접 관련이 있다(Curry-Howard 통신 참조). 이는 종종 주어진 논리를 결정하는 복잡성을 잘 보여준다.

참고 항목

• 아핀 논리학
• 선형 논리학
• 순서 논리학
• 엄격한 논리
• 분리논리