선언적 삼단 논법

1. 개요

선언적 삼단 논법은 두 가지 추론 규칙으로, 명제 논리에서 유효한 추론 규칙이다. 이는 두 명제 중 적어도 하나가 참이고, 전자가 참이 아니라면 후자가 참이라고 추론하는 방식으로, 형식 증명에서 논리적 선택지를 제거할 수 있게 해준다. 선언적 삼단 논법은 시퀀트 표기법과 진리 함수적 항진명제로 표현될 수 있으며, 다양한 예시를 통해 이해를 돕는다. 논리합의 종류에 따라 배타적 논리합을 사용한 강화된 형식이 존재하며, 직관 논리에서 성립하고 고전 논리에서도 성립하지만, 초일관 논리에서는 성립하지 않는다. 선언적 삼단 논법은 귀류법과 선언지 제거의 조합으로 증명될 수 있으며, 가언 삼단 논법, 정언 삼단 논법 등 다른 삼단 논법과 관련이 있다.

2. 정의

선언적 삼단 논법은 다음과 같은 두 가지 추론 규칙이다.

또는

:$P\backslash lor\; Q,\backslash lnot\; P\backslash vdash\; Q\backslash qquad\; P\backslash lor\; Q,\backslash lnot\; Q\backslash vdash\; P$

여기서

* $P$, $Q$는 논리식을 나타내는 메타 변수이다.
* $\backslash lor$는 논리합이다.
* $\backslash lnot$는 부정이다.
* 수평선은 증명 과정의 이웃한 두 단계를 구분하는 메타 논리 기호이다.
* $\backslash vdash$는 왼쪽에 놓인 논리식들로부터 오른쪽에 놓인 논리식을 증명할 수 있음을 나타내는 메타 논리 기호이다.

3. 형식 표기

선언적 삼단 논법은 시퀀트 표기법으로 다음과 같이 작성될 수 있다.

:$P\; \backslash lor\; Q,\; \backslash lnot\; P\; \backslash vdash\; Q$

여기서 $\backslash vdash$는 $Q$가 $P\; \backslash lor\; Q$와 $\backslash lnot\; P$의 구문적 결과임을 의미하는 메타논리 기호이다.

이는 명제 논리의 대상 언어에서 진리 함수적 항진명제 또는 정리로 표현될 수 있다.

:$((P\; \backslash lor\; Q)\; \backslash land\; \backslash neg\; P)\; \backslash to\; Q$

여기서 $P$와 $Q$는 어떤 형식 체계로 표현된 명제이다.

4. 예시

명제 논리에서 사용되는 선언적 삼단 논법의 예시는 다음과 같다.

* 그것은 빨갛거나 파랗다.
* 그것은 파랗지 않다.
* 그러므로 그것은 빨갛다.

다음은 또 다른 예시이다.

* 위반은 안전 위반이거나, 벌금 부과 대상이 아니다.
* 위반은 안전 위반이 아니다.
* 그러므로, 벌금 부과 대상이 아니다.

* 나는 수프를 선택하거나 샐러드를 선택한다.
* 나는 수프를 선택하지 않는다.
* 따라서, 나는 샐러드를 선택한다.

다른 예시는 다음과 같다.

* 브라운스가 이기거나 벵골스가 이긴다.
* 브라운스는 이기지 않는다.
* 따라서, 벵골스가 이긴다.

5. 포괄적 논리합과 배타적 논리합

논리합에는 포괄적 논리합과 배타적 논리합 두 가지 종류가 있다. 선언적 삼단 논법은 이 두 가지 모두에 적용 가능하다.

5.1. 배타적 논리합을 사용한 강화된 형식

모두스 톨렌도 포넨스는 전제 조건으로 포괄적 논리합 대신 배타적 논리합을 사용함으로써 더 강력하게 만들 수 있다.

:$\backslash frac\{P\; \backslash underline\backslash lor\; Q,\; \backslash neg\; P\}\{\backslash therefore\; Q\}$

논리합에는 다음의 2가지 종류가 있다.

* 포괄적 논리합''은 영어로 "and/or"로 표기되는 경우와 등가이며, 한쪽만 참일 수도 있고, 양쪽 모두 참일 수도 있다.
* 배타적 논리합 ("xor")은 한쪽이 참이면, 다른 한쪽은 반드시 거짓이다. 양쪽 모두 동시에 참이거나, 양쪽 모두 동시에 거짓이라는 것은 있을 수 없다.

일반적으로 자연어에서는 논리합적인 문장이 이들 2가지 중 어느 의미인지 모호한 경우가 많지만, 그 차이는 중요하다.

P이거나, 또는 Q이다.
P가 아니다.
따라서, Q이다.

이 경우, 포괄적으로도 배타적으로도 해석할 수 있다. 그러나, 다음의 경우에는 배타적 논리합에서만 성립한다.

P이거나, 또는 Q이다.
P이다.
따라서, Q가 아니다.

포괄적 논리합으로 해석하면, 위의 귀결은 이끌어낼 수 없다. 이것을 선언 긍정의 오류라고 한다.

6. 성질

직관 논리에서 성립하며, 따라서 고전 논리를 비롯한 모든 초직관 논리에서 성립한다. 초일관 논리의 일종인 1차 필연(一次必然, first-degree entailment^영어, 약자 FDE)에서는 선언적 삼단 논법이 성립하지 않는다.

7. 다른 논법과의 관계

전건 긍정이나 후건 부정과는 달리, 선언적 삼단 논법은 논리 체계의 명시적인 규칙이나 공리로 만들어지지 않는 경우가 많다. 이는 귀류법과 선언지 제거의 조합으로 증명될 수 있기 때문이다.

다른 형태의 삼단 논법으로는 가언 삼단 논법, 정언 삼단 논법 등이 있다.