5balje.hwp 논리철학연습 발제
Chapter 5 – Conjunctive Normal Form
과학사 및 과학철학 협동과정 2004-20309 정동욱 | 제출일 : 2004.5.7
Conjunctive Normal Form (CNF)
정의 : 원자들로 구성된 선언을 연언지로 가지는 연언
형식 : ()
분류 : 원자를 어떻게 정의하느냐에 따라 여러가지 CNF를 정의할 수 있음
PC-CNF
정의 : 원자가 오직 명제변항과 그것의 부정으로만 이루어지는 CNF
타당성 검증 : PC-CNF에 속하는 바른식의 모든 연언지 가 부정기호가 없는 변항 와 그 변항에 부정기호가 붙은 변항 를 동시에 가질 경우에만 타당하다. (예)
MCNF
정의 : 모든 PC바른식과 가 PC바른식인 또는 형식의 모든 바른식을 원자로 다룬 CNF
(예)
(잘못된 예)
※ 모든 바른식이 MCNF의 바른식과 동치일 수는 없다.
※ S5의 모든 바른식은 MCNF의 어떤 바른식과 반드시 동치이다. 아래는 이의 증명이다.
양상함수들과 양상등급
양상함수에 대한 양상등급의 정의는 다음과 같다. (예) : 2등급, : 2등급
1. 명제변항은 등급이 0이다.
2. 의 등급이 이라면 의 등급도 이다.
3. 의 등급이 , 의 등급이 일 때, 이라면 의 등급은 이고, 이라면 의 등급은 이다.
4. 가 등급이 이라면 의 등급은 이다.
※ 환원 : 주어진 체계에서 등급의 식이 보다 낮은 등급의 식과 동치이면, (그 체계 내에서) 전자의 식이 후자의 식으로 환원가능하다고 말한다.
S5 환원정리
정리 : S5 체계 안에서, 1등급보다 높은 등급의 모든 식은 1등급의 식으로 환원될 수 있다.
증명은 2등급의 식을 1등급의 식으로 환원할 수 있는지 살피는 것만으로 충분 (이절차를 반복적용하면 되기 때문)
증명에 필요한 동치들 : PC 동치들, 동치들, 과 분배법칙, R1∼R4 환원법칙, S5(4)∼S5(7)의 정리들
분배법칙(K3)
분배법칙(K6)
S5(4)
S5(5)
S5(6)
S5(7)
※ 다음 절차를 통해, 2등급의 식은 1등급의 식으로 환원가능하다.
1. 우선 적당한 정의를 이용해서 를 제외한 모든 연산자를 제거한다.
2. 드모르강의 법칙과 를 이용해서 괄호와 양상연산자 바로 앞에 나타난 모든 을 제거한다.
3. R1∼R4의 환원법칙을 이용해서 모든 반복되는 양상자를 하나의 양상자로 줄인다.
4. 1∼3단계의 결과로 생기는 식이 여전히 2등급의 식이라면, 이는 오직 그 식 또는 그 식의 어떤 부분이 가 1등급의 연언이거나 선언인 나 형식이기 때문이다. (이 경우, PC분배법칙과 위의 K3, K6, S5(4)∼S5(7)의 동치식을 이용하면 된다.)
※ 유한한 변항들로 구성된 동치가 아닌 1등급의 양상함수는 유한하다. (증명은 간단)
(S5 뿐만 아니라 모든 정상체계에서 적용되는 원리이며, 1등급뿐만 아니라 (유한한 변항들로 구성된) 임의의 유한한 등급의 동치가 아닌 양상함수는 유한함)
MCNF 정리
정리 : S5 체계 안에서 어떠한 바른식도 MCNF로 환원될 수 있다.
<증명>
(i)가 PC바른식이면, 이 바른식은 이미 MCNF의 식이다.
(ii)가 1등급의 식이면, 는 PC바른식 또는 가 PC바른식인 또는 형식의 바른식들의 진리함수이다. 각각의 바른식을 원자로 간주함으로써 PC-CNF를 만드는 방법을 통해 전체 식을 CNF로 환원할 수 있다. 그리고 나서 모든 과 을 각각 와 으로 대치시킬 수 있고, 그 결과인 은 MCNF의 식이다.
(iii)가 1등급보다 높은 등급의 식이라면, 우리는 위에서 설명된 방법(S5환원정리)를 통해 이 식을 1등급의 식으로 환원한 후, (ii)의 과정을 통해 을 얻는다.
(예 1)
단계 1 :
단계 2 :
단계 3 :
단계 4 :
최종결과 :
타당성 검사를 위한 정렬된 MCNF
1. MCNF의 모든 연언지 내의 선언지들을 다음과 같이 배열한다. ① PC바른식 ② 로 시작하는 선언지 ③으로 시작하는 선언지. 결과적인 형식 :
2. 배분법칙을 이용해 를 으로 대치한 후, 을 로 지칭한다.
결과적인 형식 :
MCNF의 논리식 검증
모든 MCNF의 바른식의 형식 : ()
1. 각각의 에 대해서 의 개의 선언(PC바른식)을 만든다.
2. 위의 개의 선언 중에서 적어도 하나가 PC-타당할 경우 오직 그 경우에만 는 검증을 통과한다.
3. 각각의 연언지(∼ 모두)가 검증을 통과하는 경우에만 전체 MCNF인 는 검증을 통과한다.
S5의 완전성
1. 임의의 바른식 는 그와 동치인 MCNF에 속하는 바른식 이 있으며,
2. 의 형식은 ( )
[]에 의해서, 의 각 연언지 가 S5-타당할 경우에만 가 S5-타당하고,
연언화 법칙에 의해, 의 각 연언지 가 정리이면 가 정리이다.
※ 따라서, S5의 완전성을 증명하기 위해서는 (1) 형식인 모든 S5-타당한 바른식이 S5의 정리임을 보이는 것만으로 충분하다. 그리고 이는 다음의 두가지 사실을 증명하는 것만으로 충분하다.
A : (1)의 형식을 가지는 모든 S5-타당한 바른식은 검증을 통과한다.
B : (1)의 형식의 검증을 통과한 모든 바른식은 S5의 정리이다.
A의 증명
A 명제의 대우를 통해 증명. 즉, (1)이 검증을 통과하지 못하면 S5-타당하지 않다는 것을 증명하는 것.
(i) 검증을 통과하지 못한다고, 즉 중 어떤 것도 PC-타당하지 않다고 가정하면,
(ii) 이 경우 S5 반증모형을 구성할 수 있음.
① 개의 세계로 구성된 프레임
② 중 어떤 것도 PC-타당하지 않기 때문에, , , , 인 값할당이 가능하다.
③ 결국, 이 되므로, 반증모형을 성공적으로 구성했다고 할 수있다.
B의 증명
중 적어도 하나가 PC-타당하면, (1)이 S5의 정리라는 것을 증명하는 것.
(i) ()가 PC-타당하다고 가정하면, 이므로 T1과 PC규칙에 의해 가 되며, 결국 이 된다.
(ii) 어떤 가 PC-타당하다고 가정하면, 이고, N에 의해 이 되며, 다시 K9에 의해 가 되므로, 결국 이 된다.
S5-타당성에 대한 결정 절차
어떠한 바른식 가 S5-타당하다는 것을 검증하고자 한다면, 그 식을 MCNF의 바른식 으로 환원한 후 그 식이 위의 검증을 통과하는지만 살펴보면된다. 이는 유한하고 기계적인 절차이다.
또다시 Triv와 Ver
보조정리 3.2 : Ver에 포함되지 않는 K의 모든 일관적인 확장은 D를 포함한다.
<증명>
(i) S를 Ver의 정리가 아닌 를 정리로 가지는 K의 임의의 일관적인 확장이라고 하자.
(ii) S가 형식의 정리를 가진다는 것을 보이는 것만으로 충분.
(ii)의 증명
1. 명제양상논리의 모든 바른식은 PC바른식, 또는 형식의 바른식(는 어떠한 복잡한 정도의 양상바른식도 될 수 있음)을 원자로 간주하는 CNF의 식으로 환원할 수 있음.
2. 바른식 (S의 정리이지만, Ver의 정리는 아닌)를 위의 형식의 으로 환원했다고 가정하자.
3. 그러면 은 의 형식을 가진다.
4. 각 는
(1) PC 바른식이거나
(2) 의 형식인 선언지를 포함하는 선언이거나
(3) 형식의 바른식이거나
(4) 가 PC바른식인 의 형식인 바른식이다.
5. 는 Ver의 정리가 아니기 때문에, (1), (2)는 불가능하고 (3), (4)만 가능하다. 이 경우, (3)에서는 직접적으로 를 정리로 가지게 되며, (4)에서도 가 PC-타당하면 또한 Ver의 정리가 되어 안되고 가 PC-타당하지 않다면 를 정리로 가지게 된다.
6. 결국 S가 형식의 정리를 가지지 않는다면 S는 Ver의 정리가 아닌 어떠한 정리도 가지지 못한다. 따라서 S는 형식의 정리를 가지게 된다.