Skip to content

Posts Gödel, Escher, Bach Chapter VII: The Propositional Calculus #
Find similar titles

Chapter VII. The Propositional calculus

Words and Symbols #

앞의 대화에서 거북은 'and'와 같은 일상 단어를 일상적이지 않은 의미로 사용

기호를 사용하여 아킬리스가 거북의 수법에 빠져들지 않도록 하는 방법(일상 언어의 해석적 모호함을 제거하기)을 설명하겠음

Alphabet and First Rule of the Propositional Calculus #

새로운 Formal systemPropositional calculus.

기호들:

  • \( \lt \gt \)
  • \( P, Q, R, ' \)
  • \( \land \lor \rightarrow \lnot \)
  • [ ]

규칙1:

  • Rule of Joining: If x and y are theorems of the system, then so is the string \( < x \land y > \)

앞의 대화편을 상기할 것

Well-Formed Strings #

다른 추론을 도입하기에 앞서서 모든 가능한 문자열의 부분집합인 well-formed string을 정의하자:

  • Atoms: P, Q, R은 atom. 기존 atom에 '를 추가하여 새로운 atom을 만들 수 있음. 모든 atom은 well-formed
  • Formation rules: If x and y are well-formed, then the following four strings are also well-formed:
    1. \( \lnot x \)
    2. \( < x \land y > \)
    3. \( < x \lor y > \)
    4. \( < x \rightarrow y > \)

예시 (p182)

Well-formedness 연습 (p182)

More Rules of Inference #

정리를 유도하기 위한 규칙들. 주의할 점: 아래에 나오는 모든 x와 y는 항상 well-formed string이어야 함:

  • Rule of Separation: If \( < x \land y > \) is a theorem, then both x and y are theorems.
  • Double-tilde Rule: The string \( \lnot \lnot \) can be deleted from any theorem. It can also be inserted into any theorem.

The Fantasy Rule #

이 시스템에서 특이한 점은 공리(axioms)가 없고 규칙만 있다는 것. 앞의 Formal system들에서는 항상 공리에서 정리가 유도되었는데, 공리가 없다면 어떻게 정리가 있을 수 있나?

무에서 정리를 만들어내는 하나의 규칙이 존재. 이를 제외한 나머지 모든 규칙에는 입력이 있어야 함. 이를 Fantasy rule이라고 부르자.

Fantasy rule을 사용하기:

  • 일단 임의의 well-formed string x에 대해 "만약 x가 공리 혹은 정리라면?(What if this string x were an axiom, or a theorem?)"이라고 가정
  • x에서 출발하여 추론 규칙을 적용
  • 여러 단계에 의해 y를 유도
  • x에서 y까지의 모든 것(x, y 포함)은 fantasy. 이 때, x를 fantasy의 전제(premise)라고 하고 y를 fantasy의 결과(outcome)라고 한다.
  • 마지막 단계는 fantasy 밖으로 나오는 것: "만약 x가 정리라면 y도 정리이다(If x were a theorem, y would be a theorem."

여기에서 진짜 정리는?

  • \( < x \rightarrow y > \)

Fantasy로의 진입과 진출을 표시하기 위해 []를 사용하자:

$$ [ \\ \quad P \\ \quad \lnot \lnot P \\ ] $$

Recursion and the Fantasy Rule #

Fantasy rule은 중첩하여 사용 가능. 이 때 Carry-over rule이 적용됨.

  • Carry-over rule: Inside a fantasy, any theorem from the "reality" one level higher can be brought in and used.

(Programming language에서의 중첩된 scope와 유사)

중첩된 Fantasy rule을 통해 아래와 같은 정리를 이끌어낼 수 있음:

  • \( < P \rightarrow < Q \rightarrow < P \land Q > > > \)

Python으로 치면 아래와 유사:

#!python
if p:
    if q:
        print p == q # true

The Converse of the Fantasy Rule #

가정문(\( < P \rightarrow Q > \))을 분리하기 위한 규칙:

  • Rule of Detachment: If x and \( < x \rightarrow y > \) are both theorems, then y is a theorem.

이를 Modus ponens라고도 부름. 지금까지 우리가 Fantasy rule이라고 부른 것은 Deduction theorem이라고 부름.

The Intended Interpretation of the Symbols #

기호에 의미를 부여하기:

  • \( \land \): and
  • \( \lor \): or
  • \( \lnot \): not
  • < and >: grouper
  • \( < P \rightarrow Q > \): If P then Q

Atom은 임의의 문장으로 치환 가능. 예를 들어 \( < P \land \lnot P > \):

This mind is Buddha, and this mind is not Buddha.

다른 예시. \( < P \rightarrow < Q \rightarrow < P \land Q > > > \):

If this mind is Buddha, then, if this flax weighs three pounds, then this mind is Buddha and this flax weighs three pounds.

Rounding Out the List of Rules #

지금까지의 모든 규칙들(추가로 세 개 더):

  • Joining Rule: If x and y are theorem, then \( < x \land \ y > \) is a theorem.
  • Separation Rule: If \( < x \land \ y > \) is a theorem, then both x and y are theorems.
  • Double-tilde Rule: The string \( \lnot \lnot \) can be deleted from any theorem. It can also be inserted into any theorem.
  • Fantasy Rule: If y can be derived when x is assumed to be a theorem, then \( x \rightarrow y > \) is a theorem.
  • Carry-over Rule: Inside a fantasy, any theorem from the "reality" one level higher can be brought in and used.
  • Rule of Detachment: If x and \( < x \rightarrow y > \) are both theorems, then y is a theorem.
  • Contrapositive Rule: \( < x \rightarrow y > \) and \( < \lnot y \rightarrow \lnot x > \) are interchangeable.
  • De Morgan's Rule: \( < \lnot x \land \lnot y > \) and \( < x \lor y > \) are interchangeable.
  • Switcheroo Rule: \( < x \lor y > \) and \( \lnot x \rightarrow y > \) are interchangeable.

Justifying the Rules #

생략

Playing Around with the System #

생략

Semi-Interpretations #

명제 논리의 정리를 소리내어 읽을 때 atom을 제외한 나머지만 "해석"하는 것이 자연스럽다. 저자는 이를 semi-interpreting 이라고 표현.

예를 들어 \( < P \lor \lnot P > \) 라는 정리는 "P or not P"와 같이 읽을 수 있음. P에 어떤 문장을 넣어도 참.

Ganto's Ax #

선문답에 응용하는 좀 더 복잡한 예시. 생략.

Is There a Decision Procedure for Theorems? #

이 시스템의 정리에 대한 Decision procedure가 존재하는가? 명제 논리의 정리는 Recursive set.

Do We Know the System is Consistent? #

Propositional calculus에 일관성이 있다는 것을 어떻게 알 수 있나? 두 관점(신중함 vs. 경솔함)이 있을 수 있음:

  • 신중이: 직관에 의존하는 것은 위험. 시스템의 일관성에 대한 증명이 필요하다.
  • 경솔이: 직관적이고 단순하므로 증명이 필요없다. 게다가 Propositional calculus의 일관성을 증명하기 위해 도입되어야 하는 시스템이 Propositional calculus보다 복잡할 것.

The Carrol Dialogue Again #

논리로 논리를 방어하기:

  • 위 대화는 논리논리를 방어하려는 시도의 난점을 보여주는 사례
  • Lewis CarrollWhat the Tortoise Said to Achilles에서 제기한 문제가 바로 이것
  • 논리적 사고에 대해 영원히 방어할 수는 없고 언젠가는 믿음(또는 약속)에 의존할 수 밖에 없음

What the Tortoise Said to Achilles의 대화 일부를 Propositional calculus로 표현하기:

  • Achilles: If you have \( < < A \land B > \rightarrow Z > \), and you also have \( < A \land B > \), then surely you have Z.
  • Tortoise: Oh, You mean: \( < < < < A \land B > \rightarrow Z > \land < A \land B > > \rightarrow Z > \), don't you?

즉, 아킬리스가 "추론 규칙"으로 간주하는 것을 거북은 Formal system의 문자열로 취급. 이 패턴이 무한히 반복되는 것.

Shortcuts and Derived Rules #

\( < Q \lor \lnot Q > \)를 한 번 유도했으면 \( < P \lor \lnot P > \)는 유도 과정 없이도 "마치 전에 유도했던 것처럼" 그냥 사용하곤 한다. 왜냐하면 어떤 atom이 오건 유도 과정이 정확히 동일하기 때문.

하지만 Propositional calculus를 형식적으로 엄밀하게 정의할 때 위와 같은 규칙은 존재하지 않음. 이는 사실 metatheory.

Metatheory는 유용하지만 이를 사용하게 되면 "엄밀한 형식성"이라는 애초의 목적에서 벗어나게 됨(즉, Metatheory는 M-mode가 아니라 I-mode).

Formalizing Higher Levels #

하지만 metatheory 자체를 형식화하면 "엄밀한 형식성"을 유지하면서도 shortcut을 쓸 수 있을 것. metametatheory의 형식화도 가능.

잘 설계하면 theory와 metatheory를 모두 형식화하는 하나의 Formal system을 고안할 수 있을 것. 이렇게 하면 모든 상위 수준(meta, metameta, ...)과 theory를 단일한 층위로 압축할 수 있음.

곧 이러한 시스템을 다루게 될 것이지만 아직까지는 "층위를 섞지 않는다"는 단순한 규칙을 따르도록 하자.

층위를 마구 섞어서 생각하면 치명적 오류에 빠질 수 있음:

  • \( < P \lor \lnot P > \)(해석하면 "P 이거나 P가 아니다")가 정리이므로 P 혹은 \( \lnot P \)가 정리일 것이라는 추측은 오류
  • 형식체계의 문자열을 해석하고 해석에 기반하여 다른 해석을 유도한 후, 이렇게 유도된 해석을 형식체계의 문자열로 만들었기 때문에 발생한 오류

Reflections on the Strengths and Weaknesses of the System #

Propositional logic은 매우 단순한 시스템이고, 그렇기 때문에 수학자들의 관심을 끌 수 있었음:

  • 단순한 모양들을 다루는 기하학과 유사하게, 시스템 자체의 속성에 대한 연구를 할 수 있음. 다른 기호, 추론 규칙, 공리 등을 도입하는 식의 변형을 만들기가 쉬움. 이 책에서 소개한 버전은 Gerhard Gentzen이 고안한 것
  • 추론(reasoning)의 다른 측면을 포함하게끔 확장될 수 있음. 다음 장(Gödel, Escher, Bach/Chapter VIII: Typographical Number Theory)에서 살펴보겠음.

Proofs vs. Derivations #

Propositional logic에서의 유도(derivation)는 인간의 추론 과정(reasoning)에서의 증명(proof)와 매우 유사하지만, 이 둘을 동일한 것으로 간주해서는 안됨:

  • 증명:
    • 덜 형식적, 일반적인 사고 과정의 산물, 인간의 언어로 이루어지며, 인간이 소비하기 위한 것
    • 온갖 복잡한 사고 방식이 활용될 수 있음
    • 맞는 것 같은 느낌이 들지만 정말 논리적으로 옳은지 확신할 수 없는 경우가 있음
  • 유도:
    • "논리적으로 옳은지 확신할 수 있게" 하는 것을 목표로 고안된 인공적 방식
    • 증명과 동일한 결론에 도달하되, 단순하고 명확하게 형식화된 단계들만 거치는 방식

유도는 증명에 비해 단계가 대단히 긴 경우가 많음. 각 단계를 단순하게 만들기 위해 치뤄야하는 비용 같은 것.

증명과 (Propositional logic의) 유도는 각각 한 측면에서는 단순하고, 다른 측면에서는 복잡하다

  • 단순성:
    • 증명: 단계가 짧아서 단순
    • 유도: 각 단계가 너무 당연해서 도저히 오류를 범할 수 없을 것 같아서 단순
  • 복잡성:
    • 증명: 증명에 사용되는 인간의 언어 자체가 복잡
    • 유도: 단계가 너무 길어서 전체를 이해하기가 대단히 어려운 경우가 있음

Propositional logic은 인공적인 유사-증명 구조(artificial proof-like structure)의 일부일 뿐 유연성이나 일반성은 떨어지며, 견고한 수학적 개념과 연결해서만 사용하도록 의도된 것(무슨 뜻인지? Answer me).

이와 관련하여(어떻게 관련? Answer me) 흥미로운 예시를 살펴보자. \( < P \land \lnot P > \)에서 \( < < P \land \lnot P > \rightarrow Q > \)를 유도하기:

$$ [ \\ \quad < P \land \lnot P > \\ \quad P \\ \quad \lnot P \\ \quad [ \\ \quad\quad \lnot Q \\ \quad\quad P \\ \quad\quad \lnot \lnot P \\ \quad ] \\ \quad < \lnot Q \rightarrow \lnot \lnot P > \\ \quad < \lnot P \rightarrow Q > \\ \quad Q \\ ] \\ < < P \land \lnot P > \rightarrow Q > \\ $$

\( < < P \land \lnot P > \rightarrow Q > \)의 해석은 "P and not P together imply Q". 느슨하게 해석해보자면: "모순으로부터는 어떠한 결론도 이끌어낼 수 있음"

따라서 Propositional logic에 기반한 시스템에는 모순이 담겨서는 안됨. 모순이 도입되면 암과 같이 전체 시스템이 망가짐.

The Handling of Contradictions #

하지만 인간은 이와 달리 모순이 있다고 전체 사고 체계가 붕괴되거나 하지 않는다. 대신, 시스템 밖으로 나가서 모순을 해결하기 위한 노력을 함.

예를 들어 앞 절에서의 모순을 막기 위해 Propositional Calculus의 변형(if-then에 대한 제약)을 도입한다거나.

Incoming Links #

Related Books #

Suggested Pages #

Other Posts #

0.0.1_20140628_0