[논리학] 6. Formal Proofs and Boolean Logic

Introduction Rules & Elimination Rules

Introduction Rules

- 기호를 포함하여 어떤 명제를 증명

ex) a=a (identity introduction)

 

Elimination Rules

- 특정 기호로부터 어떤 명제를 증명

ex) 1. a=b

      2. b=b

      3. b=a (identity elimination 2,1)

 

※ Fitch에서도 적용 가능

 

Conjunction Rules

- Conjunction ∧ 기호에 관한 증명 규칙

 

Conjunction Introduction

 

ex) A∧B∧C 가 주어졌을때, C∧B 를 증명

먼저 Fitch format으로 작성

마지막 문장을 이끌어 내기 위해 B와 C를 각각 써줌

B와 C가 참이 되는 이유를 써줌

B와 C로부터 최종 문장을 이끌어 낼 수 있음

 

Conjunction Elimation

 

 

Disjunction Rules

Disjunction Introduction

 

Disjunction Elimation

-proof by cases로 부를 수 있음

※ Fitch style에서는 subproof라는 것을 이용

 

Subproof

- Large proof 안에 끼워서 사용

- Subproof는 보통 가정(assumption)으로 시작

- Fitch bar를 이용하여 subproof를 구분

- Subproof 상의 가정은 오로지 subproof 내에서만 임시로 참이라고 가정하는 것임

- Subproof 이후에 그 안에서 가정 했던 것은 효력이 떨어짐

 

ex) ( B∧A) ∨(A∧C) 로부터 A를 증명

Disjunction 쪼개기 전 문장과 subproof 들 모두 citation

Subproof 를 cite할 때는 n-m 형태로 줄 번호를 표기

 

 

Reiteration 을 이용하는 예시

둘째subproof 에서 가정한 A가 증명하고자 하는목표그 자체라서Reit 을 사용

 

Negation Rules

Negation Introduction

- proof by contradiction (또는 indirect proof)

- v Elim과 유사하게 subproof가 쓰임

- 어떤 가정 P로부터 모순 ⊥을 이끌어 낼 수 있다면, 본래 전제로부터 ¬P라고 말 할 수 있음

 

Negation Elimination

- ¬¬P 문장으로부터 P라고 할 수 있음

 

Contradiction Introduction

- 어떤 문장 P와 ¬P가 성립할 때, 모순⊥이라고함

- (즉, ⊥ Intro)

- 보통 subproof 의 가정이 틀린 것을 보이기위해서, subproof 안에서 사용 (앞장의 subproof 내부에서 일어나는일)

 

Contradiction Elimination

- Subproof 내에서 가정에 모순 된다는 점을밝혀냈다면, 그 다음 문장은 어떤 문장 P 든지 주장할 수 있음

- 보통 ∨Elim과 함께 사용

 

왜 ⊥ Elimination이 필요할까?

-> ⊥ Elim 은 증명을 짧게 만들어 주기 때문에 사용

 

증명 전략

- Argument 자체가 valid 한 지 먼저 생각

- 증명해야 할 결론을 informal하게 먼저 생각해보기

- 결론에서부터 (뒤에서부터) 반대로 거슬러 올라가보기 (결론 바로 앞에 무엇이 있어야 결론이 나올 수 있을지 생각)