Ji-Haeng Huh @jhhuh@hackers.pub
Public

@ailrunAilrun (UTC-5/-4) 정말 좋은 글 정말 감사합니다. 아직도 CS관련 글을 보다가 가로로 긴 직선만 나오면 "이거 내가 읽어도 되나?" 싶은 생각이 들면서 읽기를 포기하곤 하는데 기초적인 부분부터 너무 잘 설명해주셔서 끝까지 읽을 수 있었습니다. (사실 두번 읽었습니다.)

자연 연역의 E/I 룰에서는 항상 가정의 목록이 유지되거나 줄어들어 "가정의 소비(?)"된 정도를 기준으로 증명을 순차적으로 구성하거나 파악하는게 유리한 대신 전건과 후건을 다루는데 있어서 그 대칭성이 보이지 않는다. 대신 이와 동등한 논건대수에서는 추론 규칙에 전건과 후건 사이의 대칭성을 명백히 드러냄으로써 추론 시스템 자체의 특정 구조적인 성질을 이해하는데 유리할 수 있다.

라는 생각이 들었는데 이게 올바른 관찰일까요?

"이 내용들이 2 편에서 다룰 본격적인 논리와 자료 표현의 관계에 대해 흥미를 불러일으켰기를 바라며" -> 2편 정말 기대됩니다. ㅎ

Ailrun (UTC-5/-4) @ailrun@hackers.pub
Quiet public

@jhhuhJi-Haeng Huh

자연 연역의 E/I 룰에서는 항상 가정의 목록이 유지되거나 줄어들어 "가정의 소비(?)"된 정도를 기준으로 증명을 순차적으로 구성하거나 파악하는게 유리한 대신 전건과 후건을 다루는데 있어서 그 대칭성이 보이지 않는다. 대신 이와 동등한 논건대수에서는 추론 규칙에 전건과 후건 사이의 대칭성을 명백히 드러냄으로써 추론 시스템 자체의 특정 구조적인 성질을 이해하는데 유리할 수 있다.

  • 증명을 위에서 아래로 읽으면 자연 연역의 경우 가정이 줄어들기만 하는 것이 맞습니다. 다만 프로그램적인 측면에서는 아래에서 위로 (가정이 늘어나는 방향으로) 읽는 것이 더 자연스러운데요, 이는 가정이 늘어나는 것이 프로그램에서 깊은 스코프(scope)로 들어갈 수록 더 많은 변수를 소개하는 것과 같은 개념이기 때문입니다.
  • "증명을 순차적으로 구성하기 쉽다"는 사실 약간 애매하기는 합니다. 둘 다에 익숙해지면 논건 대수의 증명이 (기계적으로 찾기에) 더 쉽기 때문에요. 실제로 증명 검색 알고리즘(proof search algorithm, 어떤 판단을 증명하는 증명을 찾는 알고리즘)도 논건 대수에 기반하는 경우가 더 많습니다. 다만 이미 만들어진 증명을 "파악"(혹은 이해)하는 데에 있어서는 (프로그래머로서는) 자연 연역의 함수형 프로그램스러운 증명이 훨씬 쉽지요.
  • "대칭성"과 관련한 관찰은 논건 대수의 발전에 있어서 핵심이라고 볼 수 있습니다. 뛰어난 직관을 가지고 계시네요.
3
1
0

If you have a fediverse account, you can reply to this note from your own instance. Search https://hackers.pub/ap/notes/01967868-2398-79fc-996d-43fa8a81ec5f on your instance and reply to it.

Ji-Haeng Huh @jhhuh@hackers.pub
Quiet public

@ailrunAilrun (UTC-5/-4) "뛰어난 직관"이라고 말씀해주셔서 감사합니다. (칭찬만 걸러듣는 성향 ㅎ) 근데 직관이라기 보단 원글에서 보여주신 "가정없이는 거짓을 증명하지 못한다"의 네줄짜리 증명의 배경 아이디어를 보고 떠오른 습관적인 "논리적 비약"이었던 거 같아요.

자연연역이 (인간에게 있어서) 프로그램으로 표현하기 좋은 어떤 구조적인 이유가 있지않을까 생각해보다가 제가 뭔가를 억지로 끼워 맞춘거 같네요. 논리적 사고를 더 훈련해야겠습니다. :)

1
0
0