범주론 삽화: 논리 (2021)

 (abuseofnotation.github.io)
2P by GN⁺ | ★ favorite | 댓글 1개
  • 논리는 참으로 받아들이는 원자 명제에서 출발해 and, or, implies 같은 연산자로 더 큰 명제를 만들며, 범주론과 마찬가지로 합성이 핵심임
  • 고전 논리는 명제를 참/거짓 Boolean 값으로, 논리 연산자를 Boolean 함수로 해석하고 진리표로 부정·논리곱·논리합·함의·동치를 다룸
  • 직관주의 논리의 BHK 해석은 명제를 증명이 있는 대상으로 보고, A ∧ B는 증명 쌍, A → B는 A의 증명을 B의 증명으로 바꾸는 함수로 해석함
  • 일부 범주에서는 객체가 명제, 사상이 증명에 대응하며, 순서에서는 A ≤ B가 A → B를 뜻하는 preorder 또는 partial order로 나타남
  • 직관주의 논리는 순서론적으로 Heyting algebra, 일반 범주론적으로 bicartesian closed category에 대응하며, 논리곱·논리합·참·거짓·함의가 각각 meet/join, terminal/initial, exponential object에 대응함

명제에서 시작하는 논리

  • 논리는 관찰과 무관하게 자기 자신과 일관되는 형식적 규칙을 다루며, 어떤 것을 알 때 다른 것이 참임을 결론 내리거나 증명하는 체계임
  • 수학 이론은 논리에 추가 정의를 더한 것으로 볼 수 있음
    • 집합론은 표준 논리 공리에 집합 소속 관계라는 원시 개념을 더해 정의될 수 있음
  • 논리를 시작하려면 참 또는 거짓으로 받아들이는 초기 명제 집합이 필요함
    • 이는 전제, 원자 명제, primary proposition이라고 불림
  • 두 개 이상의 명제는 and, or, implies/entails 같은 논리 연산자로 하나의 합성 명제가 됨
    • ∧는 and
    • ∨는 or
    • →는 follows 또는 함의를 뜻함
  • 합성 명제도 원자 명제처럼 다시 다른 명제와 합성될 수 있음

Modus ponens와 항진명제

  • Modus ponens는 A가 참이고 A → B가 참이면 B도 참이라는 오래된 논리 패턴임
    • 형식은 (A ∧ (A ⇒ B)) → B
    • “Socrates가 인간이고, 인간이면 죽는다면, Socrates는 죽는다” 같은 예로 표현됨
  • 논리는 단일 연산만이 아니라 여러 논리 연산의 조합과 관계를 다룸
    • and와 implies의 관계는 modus ponens에서 드러남
    • and와 or의 분배 법칙도 주요 관심 대상임
  • 항진명제는 구성 명제들의 참·거짓 값과 관계없이 항상 참인 명제임
    • Modus ponens는 A와 B가 참이든 거짓이든 전체 공식이 항상 참임
    • 항상 거짓인 명제는 모순이라고 불림
    • 항진명제에 not을 붙이면 모순이 되고, 모순에 not을 붙이면 항진명제가 됨
  • 값에 따라 참 또는 거짓이 달라지는 명제는 contingent statement로 불리며, 논리의 주요 관심에서 벗어남
  • 가장 단순한 항진명제는 각 명제가 자기 자신을 함의한다는 동일률임

공리 스키마와 논리 체계

  • 항진명제는 공리 스키마와 추론 규칙의 기반이 됨
  • 공리 스키마는 자리표시자를 포함한 공식이며, 자리표시자를 명제로 대체해 구체적인 명제를 만들 수 있음
    • Modus ponens에서 색상이나 구체 명제를 지우면 일반 구조가 남음
    • 그 구조에 원자 명제나 합성 명제를 끼워 넣어 특정 modus ponens 명제를 만들 수 있음
  • 추론 규칙은 공리 스키마와 거의 같은 방식으로 쓰일 수 있고, 공리 스키마도 추론 규칙처럼 적용될 수 있음
  • 모든 항진명제는 공리 스키마로 사용할 수 있음
  • 논리 체계 또는 형식 체계는 공리 스키마와 추론 규칙의 모음이며, 이를 적용해 가능한 모든 명제를 생성함
    • 예시로 다섯 개 공리 스키마와 modus ponens 추론 규칙으로 구성된 체계가 제시됨
    • 이런 논리 체계가 완전하다는 사실은 Gödel의 완전성 정리와 연결됨

고전 논리의 진리 함수 해석

  • 고전 논리는 명제가 참 또는 거짓 중 하나라는 이분법에 기반함
  • 고전 해석에서 명제와 연산자는 다음처럼 정의됨
    • 명제는 Boolean 값처럼 참 또는 거짓인 것
    • 논리 연산자는 하나 이상의 Boolean 값을 받아 Boolean 값을 반환하는 함수
  • 부정 ¬p는 단항 연산이며, 참을 거짓으로, 거짓을 참으로 바꿈
    • 같은 내용을 진리표로 표현할 수 있음
    • 이중 부정 제거는 부정을 두 번 적용하면 시작한 값으로 돌아온다는 방식으로 증명됨
  • and는 두 Boolean 값을 받아 둘 다 참일 때만 참을 반환함
    • p ∧ q → p
    • p ∧ q → q
  • or는 두 Boolean 값 중 하나라도 참이면 참을 반환함
    • p → p ∨ q
    • q → p ∨ q
  • implies 또는 material condition은 p → q로 쓰이며, p가 참이고 q가 거짓일 때만 거짓임
    • 고전 논리에서 p → q는 ¬p ∨ q가 참인 경우와 같음
  • if and only if 또는 iff는 두 명제가 같은 값을 가질 때 참임
    • P ↔ Q는 P → Q ∧ Q → P와 동치임
  • 진리표뿐 아니라 공리와 추론 규칙으로도 p → q와 ¬p ∨ q의 동치를 증명할 수 있음
    • 완전한 동치 증명에는 양방향 증명이 모두 필요함

직관주의 논리와 BHK 해석

  • 직관주의 논리는 증명을 보편적 진리의 발견이 아니라 구성으로 봄
  • 이 관점에서는 모든 명제가 반드시 참 또는 거짓이라는 이분법을 사용할 수 없음
    • 어떤 명제는 거짓이라서가 아니라 주어진 논리 체계의 범위 밖에 있어 증명되지 않을 수 있음
    • 쌍둥이 소수 추측이 이런 예로 자주 제시됨
  • Brouwer–Heyting–Kolmogorov(BHK) 해석에서는 명제보다 증명이 중심에 놓임
    • 명제는 증명을 가진 것
    • 논리 연산자는 다른 증명들로부터 증명을 만드는 구성
  • A ∧ B의 증명은 A의 증명과 B의 증명으로 이루어진 쌍, 즉 product임
  • A → B는 A의 증명을 B의 증명으로 변환하는 함수가 존재한다는 뜻임
    • A → B의 증명 집합은 A에서 B로 가는 함수들의 집합, 즉 hom-set으로 표현됨
    • 이 집합이 비어 있으면 A의 증명을 B의 증명으로 바꿀 방법이 없음
  • BHK 해석에는 별도의 iff 연산이 없지만 화살표가 있음
    • A에서 B로, B에서 A로 가는 함수가 있을 때 두 명제는 동치처럼 다뤄짐
    • 집합 관점에서는 두 명제의 증명 집합이 동형인 상황임
  • 부정은 단순히 증명이 없다는 뜻이 아니라, A가 참이라고 가정하면 모순에 도달함을 보여야 함
    • ⊥는 증명이 없는 공식의 증명, 즉 False 또는 bottom value 역할을 함
    • BHK에서 ¬A는 A → ⊥로 읽힘
    • 집합론에서는 ⊥가 공집합으로 표현됨

논리를 범주로 보기

  • BHK 해석은 논리를 범주론으로 해석하기 위한 고수준 관점을 제공함
  • 일부 범주는 논리 체계처럼 볼 수 있음
    • 객체는 명제
    • 사상은 증명
  • 모든 범주가 논리 체계가 되는 것은 아니며, 유효한 논리 명제에 대응하는 객체가 있고 유효하지 않은 명제에 대응하는 객체가 없도록 하는 조건이 필요함
  • 그런 조건을 만족하는 범주는 bicartesian closed category라고 불림
  • 단순한 경우로 순서(order)를 먼저 보면, 논리 체계와 원자 명제 집합은 범주를 이룸
    • A에서 B로 가는 방법이 하나뿐이거나 차이를 무시하면 preorder가 됨
    • 서로 따라 나오는 명제들을 동치로 보면 partial order가 됨
    • A ≤ B는 A → B를 뜻함
  • Hasse diagram에서는 A가 B 아래에 있을 때 A → B가 성립함

논리 연산의 순서론적 대응

  • 논리의 and와 or는 BHK 해석에서 product와 sum으로 나타나며, 순서론에서는 meet와 join에 대응함
  • 논리 체계가 되려면 임의의 두 명제를 and 또는 or로 결합할 수 있어야 하므로, 순서는 모든 원소에 대해 meet와 join을 가져야 함
    • 이런 순서는 lattice라고 불림
  • and와 or 사이의 중요한 법칙은 분배성임
    • 모든 A, B, C에 대해 A ∧ (B ∨ C) ≅ (A ∧ B) ∨ (A ∧ C)가 성립하면 distributive lattice임
  • 직관주의 논리를 표현하려면 lattice에 True와 False에 대응하는 원소도 있어야 함
    • False는 ⊥로 쓰이며, False의 증명이 있으면 어떤 명제든 증명될 수 있다는 폭발 원리와 연결됨
    • True는 ⊤로 쓰이며, 모든 명제로부터 따라 나오지만 그 자체에서 유의미한 내용은 나오지 않음
  • 순서에서 True와 False는 각각 greatest object와 least object임
    • 범주론 용어로는 terminal object와 initial object에 대응함
    • least와 greatest를 가진 lattice는 bounded lattice임

함의 객체와 지수 객체

  • 논리 체계를 표현하는 lattice에는 각 A, B 쌍마다 A가 B를 함의한다는 명제를 나타내는 함의 객체가 필요함
  • 이 객체는 modus ponens 구조로 정의됨
    • A ∧ (A ⇒ B) → B가 성립해야 함
  • 단순히 이 조건만으로는 충분하지 않음
    • A ⇒ B ∧ C나 A ⇒ B ∧ C ∧ D 같은 다른 객체도 같은 자리에 들어갈 수 있음
    • 실제 A ⇒ B는 A ∧ X → B를 만족하는 X들 중 가장 큰 객체임
  • 순서론에서는 A ⇒ B를 exponential element 또는 relative pseudo-complement라고 부름
    • A ∧ X ≤ B를 만족하는 가장 큰 X임
  • 논리적으로는 A ∧ X → B를 만족하는 가장 사소한 명제 X가 함의 명제 A ⇒ B임
  • 범주론적으로는 exponential object 또는 internal homomorphism object로 정의됨
    • A × X → B라는 사상이 있어야 함
    • 같은 성질을 가진 다른 후보 객체에서 실제 지수 객체로 가는 유일한 사상이 존재해야 함
  • 이 함의 객체 정의는 직관주의 논리에 맞음
    • 고전 논리에서는 배중률 때문에 A ⇒ B가 ¬A ∨ B로 단순화됨
  • meet, join, 함의 객체처럼 A ⇒ B도 유일한 동형까지 정의됨

Heyting algebra와 bicartesian closed category

  • 직관주의 논리는 True, False, and, or, implies로 구성됨
  • 이를 순서로 표현하면 Heyting algebra가 됨
    • join과 meet를 가짐
    • greatest와 least 객체를 가짐
    • 함의 객체를 가짐
  • 직관주의 논리 체계는 Heyting algebra로 볼 수 있음
    • and와 or는 meet와 join
    • True와 False는 greatest와 least 객체
    • implies는 exponential object
  • 같은 정의를 일반 범주에 맞게 바꾸면 bicartesian closed category가 됨
    • product와 coproduct를 가짐
    • initial과 terminal object를 가짐
    • exponential object를 가짐
  • 직관주의 논리 체계는 bicartesian closed category로도 볼 수 있음
    • and와 or는 product와 coproduct
    • True와 False는 terminal과 initial object
    • implies는 exponential object
  • 고전 논리를 따르는 lattice는 bounded, distributive에 더해 complemented여야 함
    • 각 명제 A에 대해 고유한 ¬A가 있어 A ∨ ¬A = 1, A ∧ ¬A = 0을 만족함
    • 이런 lattice는 Boolean algebra라고 불림

범주적 논리로 보는 간단한 증명

  • A ∨ ⊤ ≅ ⊤는 join의 정의에서 바로 따라옴
    • join은 두 객체보다 크거나 같은 최소 상계임
    • ⊤보다 크거나 같은 객체는 ⊤ 자신뿐이므로, 임의의 A와 ⊤의 join은 ⊤임
    • 논리적으로는 “임의의 A 또는 True는 True”라는 항진명제임
  • A → B가 있으면 A ∨ B = B임
    • 두 객체 중 하나가 다른 하나보다 위에 있으면, join은 더 위에 있는 객체임
    • 이는 A ∨ ⊤ = ⊤의 일반화로 볼 수 있음
    • 모든 객체 A에 대해 항상 A → ⊤가 성립하기 때문임
  • 동일률은 함의 객체로도 증명됨
    • A ⇒ A는 A ∧ X → A를 만족하는 가장 큰 X임
    • 이 조건은 모든 X에 대해 성립하므로 가장 큰 객체 ⊤가 됨
    • 따라서 A → A는 항상 참임
  • A가 모든 모델에서 B를 함의하는 semantic consequence A ⊨ B라면 A ⇒ B도 ⊤에 대응함
    • A 자체가 이미 B를 함의하므로 A ∧ X → B가 모든 X에 대해 성립함
    • 이는 deduction theorem으로도 불림

Free Heyting algebra로 논리 만들기

  • 논리를 수행하려면 먼저 문제 영역에 따라 사용할 원자 명제를 고름
  • 선택한 논리의 종류가 직관주의 논리라면 모든 A, B에 대해 A ∧ B, A ∨ B 같은 합성 명제를 그래프로 그려야 함
  • 합성 명제들의 합성도 다시 포함해야 하므로 전체 목록은 무한해짐
  • 어떤 명제가 다른 명제를 함의하는지는 출발 명제에서 나가는 화살표의 경로를 따라가며 확인함
  • 논리 수행은 이미 아는 것에서 증명하고 싶은 것까지 가는 경로를 찾거나, 이미 가진 증명을 조작해 증명을 구성하는 과정임
  • 직관주의 논리에서는 일반적으로 어떤 사실이 공리로부터 도달 불가능하다는 것, 즉 증명될 수 없다는 것을 증명하기 어려움

함께 보면 좋은 글 β

GN⁺   [-]
Hacker News 의견들

  • 이 페이지는 정말 훌륭하고, 관련 내용을 공부할 때 여러 번 마주쳤음
    그래도 Milewski로 배우는 쪽에 한 표를 주고 싶음. 이걸 배우는 건 여정이고, ct-illustrated의 저자는 아직 그 여정 중간에 있는 것 같음
    Milewski는 이미 그 길을 여러 번 다녀온 사람이라 책과 블로그가 좋은 출발점임
    https://github.com/hmemcpy/milewski-ctfp-pdf Book
    https://bartoszmilewski.com/2014/10/28/category-theory-for-p... Blog

    • Milewski의 앞부분 십여 장을 읽었는데, 처음 몇 장은 정말 좋았지만 정확한 정의와 표기를 주지 않는 문체가 갈수록 짜증남
      가볍고 부정확한 산문으로 쓰면 뭐든 더 이해하기 쉽다고 보는 듯한데, 그 때문에 참고서로는 거의 쓸모가 없어짐
      전혀 그렇지 않음¹
      ¹) https://news.ycombinator.com/item?id=41756286
    • bartoszmilewski가 무슨 말을 하는지 이해가 안 돼서 그 책은 나에게 쓸모 없어 보임
      하지만 직장에서는 내 도메인 모델 전체에 범주론을 쓰고 있음

  • 예전에 다른 URL로 이미 논의됐음
    https://news.ycombinator.com/item?id=28660131 (댓글 2개)
    https://news.ycombinator.com/item?id=28660157 (댓글 112개)

  • 책의 초반부에서 수학을 과학이나 공학과 비교하며 이런 멋진 문장을 만났음
    “이 때문에 수학자들은 다른 학문 분야에 대한 가치라는 관점에서 자신들이 하는 일을 항상 변호해야 하는 이상하고, 독특하다고도 할 수 있는 위치에 놓인다. 다시 강조하지만, 다른 어떤 학문 분야에 대해서라면 이런 일은 터무니없는 것으로 여겨질 것이다.”
    직접적으로 돈이 되는 결과로 이어지지 않는 분야를 공부한 사람이라면 누구나 공감할 개념이고, 숫자 쪽 재능을 가진 사람들도 Milton Friedman의 면도날과 싸워야 한다는 걸 듣는 건 반갑다

    • 그렇다면 “문화연구”의 많은 프로젝트가 실제로는 미 국방부와 국무부에서 직접 자금을 받는다는 점은 다행임
      오늘날 “탈식민주의” 연구 전체는 미국 소프트파워의 백엔드에 지나지 않고, 전쟁이 나면 아마 하드파워의 백엔드도 될 것임

  • 안쪽 원들이 항상 세로 중앙에 배치된다면 원 안의 원 도식은 규모가 커질 때 잘 버티지 못함

  • 범주론을 써서, 범주론 없이는 풀 수 없었던 CS/SWE 문제를 유익하게 해결한 성공담이 있을까? 모나드는 해당 안 됨. 상황이 필요하면 자연스럽게 발명하게 되는 것이기 때문임
    대학원에서 1년 동안 공부했지만 결국 포기했음

    • 범주론 없이 모델링할 수 없는 문제는 없음
      범주론의 가장 기초적인 정리 중 하나인 요네다 보조정리는 범주의 언어로 표현된 모든 문제가 집합과 함수의 언어로 번역될 수 있음을 직접 말함. 집합으로 정의되는 모든 수학적 대상도 마찬가지라서, 이름을 언제든 정의로 대체할 수 있음
      범주론적 언어가 어떤 이론의 암묵적 틀에 기여하는 바는 “범주”의 정의보다 클 수 없고, 그 정의는 매우 작음. “결합법칙, 닫힘, 항등원, 역원을 갖는 집합 위의 연산”이 더 다가가기 쉬운데 왜 군을 쓰느냐고 묻는 것과 비슷함
      추상대수학은 충분히 흔할 만큼 단순한 집합 위 연산 유형들을 가리키는 정의들의 라이브러리에 기반함. 도구나 기법은 정의 안에서 찾을 수 있는 종류의 것이 아님
      환, 벡터공간, 가군은 그 자체로 즉시 받아들여지는 편인데, 범주는 믿는 사람과 믿지 않는 사람이 갈림. 왜 그런 일이 생기는지 궁금함
    • 내가 아는 가장 가까운 예는 UMAP 작업임
      Leland McInnes를 인터뷰했을 때, 최종 결과의 실제 코드에는 꼭 필요하지 않더라도 범주론이 여러 점을 연결하는 데 큰 역할을 했다고 자세히 설명해 줬음
      이전 최신 기법이던 t-SNE 대비 상대적 개선폭을 보면, 소프트웨어에서 범주론을 논하는 방식에 대한 내 비판을 다시 생각하게 만든 유일한 예임
      https://arxiv.org/abs/1802.03426
    • “걸어서 갈 수 없었던 곳에 자동차를 써서 간 성공담이 있나?”라고 묻는 것과 비슷함
      범주론은 언어이자 도구라서, 범주론의 언어로 말할 수 있는 것은 다른 언어로도 말할 수 있음
      자동차처럼 운전법을 익히면, 그리고 이건 학습 곡선이 매우 가파르지만, 더 빨리 갈 수 있음. 원칙적으로는 범주론 개념을 명시적으로 언급하지 않고 걸어서도 갈 수 없는 것은 아님
    • 이미 이해한 것을 더 일반적인 틀로 다시 정식화하면, 그것이 실제로 무엇을 뜻하는지 더 잘 보이고 지저분한 세부사항에서 본질을 분리할 수 있음
      내가 아주 제한적으로 이해한 바로는, 보편 성질로 대상을 특징짓는 것이 범주론의 중요한 부분임
      범주론의 또 다른 실용성은 컴퓨터과학자, 수학자, 물리학자가 함께 말할 공통 언어를 준다는 데 있음. 모두가 같은 패턴을 서로 다른 이름과 약간씩 호환되지 않는 정의로 부르면 협업이 쉽지 않음
    • Topos Institute에서 범주론 Kool-Aid를 아직 마시지 않은 사람들에게 훨씬 더 투명하게 보이길 기대하는 새 소프트웨어를 만들고 있음
      현재 프리알파는 주로 시스템 동역학 모델링용이지만, 목표로 하는 작업 범위에는 범주론적 기반이 필수적이라고 봄. 누구의 생각이든 기쁘게 듣고 싶음
      https://topos.site/blog/2024-10-02-introducing-catcolab/

  • 범주론은 유용하다고 생각하지만, 아직 컴퓨팅에서는 아닌 것 같음
    실제로 필요한 일이 없으면 어렵게 느껴질 수밖에 없음. 보편 성질, 수반 함자, 요네다 보조정리를 정말 이해해야 할 필요가 있는가? 필요가 없다면 그것들이 무엇인지 배우는 데 애먹게 됨
    흥미롭게도 함수형 프로그래밍 경험은 범주론 이해에 도움이 되지만, 그 반대는 그다지 아님. 예를 들어 매개변수 다형성은 자연 변환에 대한 직관을 주고, 자연 변환은 범주론의 모든 응용에서 핵심임
    범주론의 설득력 있는 응용은 매우 수학적임. 대수적 위상수학, 표현론, 대수기하학, 비고전 논리에서 찾을 수 있음

  • 오류가 있음
    “모두긍정논법은 다른 두 명제, 여기서는 A와 B로 표시한 명제로 구성된 명제이며, 명제 A가 참이고 명제 A --> B도 참이면, 즉 A가 B를 함의하면 B도 참이라고 말한다. 예를 들어 ‘소크라테스는 인간이다’와 ‘인간은 죽는다’를 알면, ‘소크라테스는 죽는다’도 안다.”
    이 예시는 명제논리의 규칙인 모두긍정논법의 사례가 아니라, 술어논리가 필요한 정언 삼단논법임

  • 여기서는 “논리는 가능한 것의 과학”이라고 하는데, 논리는 확정적인 것의 과학이어야 하지 않을까?
    핵심은 무엇이 유효한지 아닌지를 확정적으로 말할 수 있게 하는 데 있다고 봄

  • 도식 표기법이 흥미로움
    저자가 도식의 진리 보존 변환을 위한 추론 규칙도 제시하나?

답변달기