§1.3 타당성과 추론🔗

x > 0의 참·거짓은 상태에 달려 있다. x가 3이면 참이고 -1이면 거짓이다. 단언 하나만으로는 진리값이 없고 상태가 있어야 정해진다는 것이 §1.2의 결론이었다.

그런데 상태를 하나 고르지 않고 전부 훑으면 단언 자체의 성질이 나온다. x > 0 ∨ x ≤ 0은 어떤 상태에서도 참이고, x > 0 ∧ x ≤ 0은 어떤 상태에서도 거짓이다. Reynolds는 §1.3에서 그런 성질 넷에 이름을 붙인다.

/-- **타당(valid)** — 모든 상태에서 참. Reynolds §1.3. -/
def Valid (p : Assert V) : Prop := ∀ σ : State V, ⟦p⟧ₐ σ

/-- **충족 불가능(unsatisfiable)** — 어떤 상태에서도 거짓. -/
def Unsat (p : Assert V) : Prop := ∀ σ : State V, ¬ ⟦p⟧ₐ σ

/--
`p`가 `q`보다 **강하다(stronger)**. `q`는 `p`보다 **약하다(weaker)**.

Reynolds가 곧바로 붙이는 단서가 있다.

> *"'stronger' and 'weaker' are dual preorders, which does not quite jibe with normal
> English usage. For example, any assertion is both stronger and weaker than itself."*

`Stronger`는 반사적이고 추이적인 준순서(preorder)다. 어떤 단언이든 자기 자신보다 강하면서
동시에 약한 것은 반사성 때문이다. 의미가 같지만 구문이 다른 단언도 서로 강하므로, 구문
등식에 대한 반대칭성은 일반적으로 성립하지 않는다.
-/
def Stronger (p q : Assert V) : Prop := ∀ σ : State V, ⟦p⟧ₐ σ → ⟦q⟧ₐ σ

/-- **동치(equivalent)** — 같은 뜻. -/
def Equivalent (p q : Assert V) : Prop := ∀ σ : State V, (⟦p⟧ₐ σ ↔ ⟦q⟧ₐ σ)

여기까지는 전부 뜻으로 정의했다. 상태를 훑어 보고 판정한다.

증명은 그렇게 하지 않는다. 공리에서 출발해 규칙을 적용해 가며 문장을 얻고, 그 과정에서 상태를 한 번도 보지 않는다. 그것을 따로 정의한다.

/--
술어 논리의 작은 추론 체계. Reynolds §1.3 p.13이 공리·공리꼴·두 전제 규칙·한 전제
규칙의 예로 직접 드는 넷 그대로다: `x + 0 = x`, `e₁ = e₀ ⇒ e₀ = e₁`, 전건 긍정,
보편 일반화.

완전한 체계가 아니고 그럴 의도도 없다. 책도 이 넷을 "예시"라고만 하고 나머지는
논리학 교과서로 미룬다(모듈 docstring의 "책과의 차이" 참고).
-/
inductive Proof : Assert V → Prop where
  /--
  공리: `x + 0 = x`. 책은 메타변수가 없는 구체적인 객체 변수 x로 든다 — 바로 다음
  공리꼴과 대조하려는 것이다(p.13, "notice the special role of axiom schemas").

  **책과의 차이**: 여기서는 모든 객체 변수 x에 대해 한 번에 선언한다. Lean에서 변수마다
  따로 공리를 선언하면 쓸 수 없는 정의가 되기 때문이다. 책의 "메타변수 없음"은 이 x 하나를
  구체적으로 고정했을 때의 이야기이고, 다형화 자체는 책에 없는 저장소의 선택이다.
  -/
  | addZero (x : V) : Proof (.cmp .eq (.bin .add (.var x) (.num 0)) (.var x))
  /--
  공리꼴: `e₁ = e₀ ⇒ e₀ = e₁`. 전제 없이 바로 쓸 수 있지만 `e₀`, `e₁`이 메타변수라서
  임의의 정수 식 쌍에 대한 사례를 전부 대신한다 — 공리와 공리꼴의 차이가 바로 이
  메타변수 유무다(p.13, "their instances are assertions that can appear anywhere
  in a proof, regardless of what, if anything, precedes them").
  -/
  | eqSymmSchema (e₀ e₁ : IntExp V) :
      Proof (.bin .imp (.cmp .eq e₁ e₀) (.cmp .eq e₀ e₁))
  /-- 두 전제 규칙 — 전건 긍정(modus ponens). -/
  | mp {p q : Assert V} : Proof p → Proof (.bin .imp p q) → Proof q
  /--
  한 전제 규칙 — 보편 일반화(∀-도입).

  전제가 타당할 때만 결론이 타당해진다. 이 파일 §4에서 이 규칙과 함의 `p ⇒ ∀v. p`를
  나란히 놓고 비교한다.
  -/
  | genAll (v : V) {p : Assert V} : Proof p → Proof (.quant .all v p)

Proof p는 "p를 이 규칙들로 유도할 수 있다"는 뜻이다. Valid p와 달리 상태가 어디에도 나오지 않는 것을 확인해 보라. 두 정의는 서로를 모른다.

규칙으로 얻은 것이 실제로 참임을 보장하는 성질이 건전성(soundness)이다. Validity.lean에서 Proof p → Valid p로 증명한다. 증명은 Proof에 대한 귀납법이다 — 규칙 하나하나가 타당성을 보존하는지 확인하면 된다.

반대 방향(Valid p → Proof p, 완전성)은 성립하지 않는다. 아래 곁가지에서 다룬다.

규칙과 함의는 다른 것이다🔗

보편 일반화 규칙은 건전한데, 같은 재료로 만든 함의는 타당하지 않다. 둘이 같은 말을 하는 것처럼 보여서 §1.3에서 가장 자주 걸리는 곳이다. 두 정리를 나란히 놓는다.

/-- 규칙 쪽. `p`가 타당하면 `∀v. p`도 타당하다. -/
@[exercise "§1.3 gen-sound" 1]
theorem valid_forall_of_valid (v : V) {p : Assert V} (h : Valid p) :
    Valid (.quant .all v p)

/--
함의 쪽. `x > 0 ⇒ ∀x. x > 0`은 타당하지 않다.

Reynolds의 반례를 그대로 쓴다. `x ↦ 3` 인 상태에서 왼쪽은 참이고,
오른쪽은 `x`에 0 을 넣으면 거짓이다.

같은 재료로 만든 규칙(위)과 함의(여기)의 판정이 갈린다.
-/
@[exercise "§1.3 gen-not-imp" 2]
theorem not_valid_imp_forall :
    ¬ Valid (.bin .imp (.cmp .gt (.var "x") (.num 0))
                       (.quant .all "x" (.cmp .gt (.var "x") (.num 0))) : Assert String)

규칙은 전제가 타당할 때 결론이 타당하다고 말한다. 함의는 한 상태 안에서 왼쪽이 참이면 오른쪽도 참이라고 말한다. x ↦ 3 인 상태 하나만 잡으면 뒤쪽이 무너진다.

곁가지 — 완전성과 괴델🔗

Reynolds는 §1.3을 닫으면서 이 책이 다루지 않을 것을 알려 준다. 코드로 옮기지 않기로 한 논의라 여기에 산문으로 남긴다.

건전성의 역이 완전성(completeness)이다. 타당한 것은 모두 유도되는가.

답은 "타당"을 어떻게 정의했느냐에 달렸다.

우리처럼 정수에 대한 표준 해석을 고정하면 참인 산술 문장까지 모두 다뤄야 한다. 산술을 충분히 표현하면서 공리와 증명을 기계적으로 열거·검사할 수 있는 일관된 체계는 그 참인 문장을 전부 증명할 수 없다. 괴델의 불완전성 정리는 이런 조건 아래에서 적용된다.
논리적 타당성(logical validity) — 연산 기호의 뜻까지 임의로 바꿔도 성립하는 것 — 으로 정의하면 일차 논리에는 건전하고 완전한 효과적 증명 체계가 있다. 괴델의 완전성 정리가 그것이다.

같은 이름의 두 정리가 반대 방향을 말하는 것처럼 보이지만, 두 "타당"이 다른 것이다.

Reynolds는 여기에 실용적인 단서를 붙인다. 프로그램 검증에서 논리적 완전성은 별 쓸모가 없다는 것이다. 우리는 +가 정말 덧셈인 해석에만 관심이 있기 때문이다. 그 예외는 §3.8에서 다룬다.

왜 코드로 만들지 않았나. 이 주제를 형식화하려면 증명론 전체가 따라온다 — 산술의 인코딩, 증명 가능성 술어, 대각화. Reynolds 본인이 다루지 않고, 1장의 목표와도 멀다. Lean으로 괴델을 보고 싶다면 mathlib 밖의 별도 프로젝트를 찾는 편이 낫다.