§1.4 자유 변수와 일치 정리🔗

∀x. x > y에서 x와 y는 처지가 다르다. y의 값은 바깥 상태가 정하지만, 양화사는 모든 정수 n에 대해 상태를 σ[x := n]으로 갱신한 경우를 다룬다. 그래서 x의 바깥 값은 결과에 영향을 주지 않는다. 앞을 자유(free), 뒤를 속박(bound) 이라고 부른다.

"자유" 라는 말은 결합자가 있어야 뜻이 생긴다. 정수 식에는 결합자가 없으니 나오는 변수가 전부 자유롭고, 단언 쪽에서 한 절만 다르다.

def Assert.fv : Assert V → Finset V
  | .tru | .fls  => ∅
  | .cmp _ e₀ e₁ => e₀.fv ∪ e₁.fv
  | .not p       => p.fv
  | .bin _ p q   => p.fv ∪ q.fv
  | .quant _ v p => p.fv.erase v

erase가 붙은 절 하나가 결합의 전부다. ∀v. p의 자유 변수는 p의 자유 변수에서 v를 뺀 것이다. ∀x. x > y로 계산해 보면 {x, y}에서 x를 빼 {y}가 나온다.

이 정의가 옳다는 근거가 일치 정리(coincidence theorem, 명제 1.1) 다. 두 상태가 FV(p) 위에서 같으면 p의 뜻이 같다는 것이다. 다시 말해 fv는 뜻에 영향을 줄 수 있는 변수를 빠뜨리지 않는다. 그렇다고 적어 둔 변수가 전부 실제로 영향을 주는 것은 아니다. x - x에는 x가 자유롭게 나타나지만 값은 어느 상태에서나 0이다.

증명에서 한 군데가 걸린다. Reynolds는 ∀v. p를 다룰 때 귀납 가설을 원래 상태가 아니라 σ[v := n], σ'[v := n]에 적용하라고 설명한다. Lean으로 옮기면 진술을 ∀ (p) (σ σ') 꼴로 써야 한다는 요구가 된다. σ, σ'를 정리의 인자로 빼면 귀납 가설이 그 특정 상태에만 붙어서 이 단계가 막힌다.

"진술을 더 일반화해야 귀납이 돈다" — 이 저장소에서 가장 자주 쓰는 요령이고, 1장에서만 여섯 번 나온다. 2장 명제 2.7 에서 더 어려운 모습으로 다시 만난다.