Daddy's Journey to Platinum

5 Predicate Logic / 술어 논리
진술과 추론 규칙을 추가해서 확장한 명제 논리를 술어 논리라고 한다. 

5.1 Quantifiers
정의. 
기호 ∀은 "모두를 위해", "모두를 위해" 또는 "각자를 위해"라고 불립니다. 
기호 ∃은 "어떤 것을 위해" 또는 "존재합니다"라고 불립니다. 

5.2 Statements / 명제
정의. x가 임의의 변수이고 W가 x와 같은 유형의 식에 적용될 때 문에 평가되는 람다 식인 경우, (∀x, W(x))와 (∃x, W(x))는 모두 명제입니다. 

5.3 Declarations / 선언
1. 변수(변수 선언) 로 선언 
2. 상수(상수 선언) 로 선언 
3. 임시적인 새로운 표기법으로 정의 
4. 증명 시작 전에 주어진 전제 또는 전역적으로 선언된 전제에서 정리의 진술 

5.4 Rules of Inference / 추론규칙
The rules of inference for these two quantifiers are as follows.

∀+ (Let s be arbitrary ⊢ W(s)) ⊢ (∀x, W(x))
∀− (∀x, W(x)) ⊢ W(t) 
∃+ W(t) ⊢ (∃x, W(x)) 
∃− (∃x, W(x)) ⊢ For some constant c, W(c)

5.5 Equality / 동일성
등식/동일성 
- 반사성 
- A = B <-> B = A
- 대체성
- A = B -> A+B = A + A = 2A

증명에서 전체에 대한 증명에서 많이 사용하는 For all (∀) 과 임의의 존재하는(∃) 에 대한 내용들이 나온다. 어떤 증명에서 해당하는 대상전체에 대한 증명어서는 "모든 x에 대해서" 라고 하고, 반례를 이용하여 증명하는 경우에 임의로 존재한다고 가정하는 "임의의 x"에 대해서라고 전개하는 경우에 사용된다. 소수의 무한성에 대한 유클리드의 증명에서 이것들을 생각할 수 있다.

소수(prime number)가 유한하다면, ∀ P_i 를 생각할 수 있고, 그 모든 수들을 곱하고 +1 을 하면 특정한 P를 만들수 있다. ∃P는 소수가 아니기 때문에, 1 과 자기 자신을 제외한 약수를 가져아 하지만, 모든 ∀ P_i 에 대해서 나누면 항상 1이 남기때문에 약수로 가질 수 없다. 그러므로, 처음 가정했던 유한성에 오류가 있고, 무한성이 증명되었다.

대략 이런 형태로 생각할 수 있겠다.

3 수학에서의 추론 규칙 (Rules of Inference in Mathematics)
3.1 추론 규칙을 위한 템플릿 표기법 (Template Notation for Rules of Inference)

Rule Name Here 
- P1 (show) 
- . . .
- Pk (show) 
- . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 
- Q1 (conclude)
- . . . 
- Qn (conclude)

전제(P1, . . . . Pk) 및 결론(Q1, . . . Qn)을 갖는 추론 규칙은 다음과 같이 표현될 수 있습니다
(P1, . . . , Pk ⊢ Q)

Proof by Cases
- W or V (show) 
- Assume W 
- U (show) 
- ←
- Assume V 
- U (show) 
- ← 
- . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 
- U (conclude)

4 명제 논리  
4.1 명제 논리의 진술
정의. φ, ψ를 참/거짓을 알 수 있는 명제라고 하면'¬φ', 'φ and ψ', 'φ or ψ', 'φ⇒ψ', 'ψ⇔φ'의 다섯 가지 논리연산 값도 결정됩니다. 

- Atomic Statements 는 논리연산을 포함하지 않습니다. 
- Compound Statements 는 명제들의 논리연산의 형태로 표현할 수 있습니다. 

4.2 명제 논리의  규칙 
연역법은 정의에 대한 '더하기'와 '빼기' 규칙을 정의합니다. 
- '더하기' 규칙 : and+, or+, ⇒+, ⇔+, not+ (proof by contradiction)
- '빼기'  규칙 : and-, or-, ⇒-, ⇔-, not− (proof by contradiction)

4.3 Formal Proof Style
Example 7. Let P and Q be statements. Prove the following case of DeMorgan’s Law, namely that 

¬P or ¬Q⇒ ¬(P and Q)

Proof.

• Assume ¬P or ¬Q -
  • Assume ¬P -
    • Assume P and Q -
    • P by and−
    • →← by →←+
    • ←
  • ¬(P and Q) by not+ 
  • ← -
• ¬P⇒ ¬(P and Q) by ⇒+;
  • Assume ¬Q -
    • Assume P and Q -
      • Q by and −
      • →← by →←+
      • ← -
    • ¬(P and Q) by not+;
    • ← -
• ¬Q⇒ ¬(P and Q) by ⇒+
  • ¬(P and Q) by or−
  • ← -
• ¬P or ¬Q ⇒ ¬(P and Q) by ⇒ +

기본문장(atomic expression)과 복합문장(compound expression) 사이의 관계를 증명에서 이용할 때 확인할 내용들에 대한 안내이다.

챕터 요약 (0. Introduction ~ 2. The Language of Mathematics)

0 Introduction
수학적 증명은 수학적인 사실을 결정하고 전달하기 위해서 필요한 객관성을 보여줄 수 있고 누구나 직접 확인해볼 수 있도록 한다. 이점이 공감대 형성에 도움을 줄 수 있다. 또한 공동작업을 위해서 필요한 가정, 용어, 사실에 대한 객관적인 출발점을 제공한다.

1 What is a proof?
증명은 어떤 명제가 객관적으로 옳은 이유를 설명하는 것이다. 이것을 위해서는 명제가 객관적으로 참임을 효과적인 방법을 통해서 설명하는 것이다. 

형식적 증명 ( Formal proof) 과 전통적 증명(Traditional proof)
- 형식적 증명: 기계로 검증이 가능하도록 엄정한 형식에 맞춰서 작성된 것
- 전통적 증명: 잘 정의된 방법들을 이용해서 지루하고 반복적인 부분을 제거한 것

1.1 Formal Proof Systems
Definition 1. 형식적 증명은  명제들의 집합과 이것을 위한 추론 규칙(rules of inference)으로 구성된다. 

Definition 2. 공리(axiom)은 증명이 필요하지 않는 추론 규칙들의 결론이다. 

Definition 3. 어떤 명제가 증명가능하기 위해서는 그 명제가 선행된 명제(Q_1, ..., Q_n)들을 통한 결론이거나, 선행 명제로 필요한 명제들 (P_1, ... P_n)을 증명할 수 있을 때이다.

Definition 4. 선행하는 명제들이 없이 증명가능한 명제를 정리(theorem)이라고 한다.

Definition 5. 증명은 순차적으로 추론 규칙을 적용하여, 명제가 정리가 될 수 있음을 보이는 것이다. 

1.2 Environments and Statements
Environments serve two main purposes. 
- 특정한 가정이나 정의의 범위를 설정하고 알려주는 것. 
- ex) 이 증명에서  N 을 자연수의 집합으로 정의한다.
- Notation.
- 형식증명에서 P_1, ..., P_n 을 이용해서 Q를 증명할 수 있다면, 다음과 같이 표기합니다.
- P_1, ..., P_n ⊢ Q
- P_1, ..., P_n 은 증명에 대한 환경의 일부로 생각할 수 있고, 하위증명 혹은 명제(proposition)라고 합니다.
- 여러 명제를 대상으로 확장
- P_1, ..., P_n ⊢ Q_1, ..., Q_m
- ⊢ 의 왼쪽편인  P_1, ..., P_n 을 공리로서 가정한다면 , 오른쪽편인 Q_1, ..., Q_m 부분을 증명할 수 있다는 설명입니다.

Lurch : http://lurchmath.org/

2 The Language of Mathematics
2.1 Identifiers, Variables, and Constants
- 수학에서 식별자(identifier)는 상수와 변수의 두 가지 종류가 있습니다.
- 상수(constant) - 특정한 수학적인 대상을 지정하는 것
- ex)  "π", ‘ln’, ‘cos’, ‘+’
- 변수(variable) - 특정한 유형의 값이 정해지지 않은 대상들의 이름
- ex) x, k, a, ...

2.2 Expressions and Statements
- 단일 식별자는 기본문장(atomic expression)입니다.
- 하나 이상의 식별자로 구성된 것을 복합문장(compound expression)이라고 합니다.

어떤 명제가 성립한다는 사실과 명제의 참, 거짓은  서로 독립적임.

2.3 Substitution and Lambda Expressions
- Lambda Expressions
- x 를 대상으로 하는 표현 E를 λx, E 형태로 기술 하는 방법

수학적 증명에서 사용하는 공리(axiom), 정리(theorem), 상수, 변수 같은 수학적인 용어와 개념들에 대한 간략한 설명이 나와 있는 부분이다. 

Google Bard 에서 나온 Formal Proof에 대한 설명

공식 증명의 기본 원칙은 다음과 같습니다.

1. 공리: 증명을 시작하는 진술입니다. 공리는 증명 없이 참으로 받아들여집니다.
2. 정의: 용어의 의미를 설명하는 진술입니다. 정의는 공리로 간주됩니다.
3. 공리적 추론: 공리와 정의를 사용하여 새로운 진술을 도출하는 과정입니다.
4. 모순: 증명 중에 모순이 발견되면 주장이 거짓임을 의미합니다.
5. 완전성: 증명은 주장을 뒷받침하는 충분한 진술을 포함해야 합니다.