Notes #BrainDump
콘차로프스키 (2022) 파이썬:을 통한 수리논리 괴델 정리 구현

콘차로프스키 (2022) 파이썬:을 통한 수리논리 괴델 정리 구현

2024-06-20 Bibliography bib mathmaticallogic python c006
  • Gonczarowski Yannai A (2022) Mathematical Logic Through Python
  • ⊢⊨ 기호가 빠진 부분을 채워 넣다.

관련노트

아마 관련 논의가 있는 노트가 있다. 아래가 그것이다.

不完全性定理 incompleteness theorems

아마 이 책은 번역서가 나올 법 한데 문제는 영어를 읽으려면 용어 충돌 때문에 난삽한다는 것이다.

역시 뭐니 뭐니 해도 마틴 데이비스 (2023) 유니버셜 컴퓨터 에서 다루는 것이 이 이야기다. 여기서 다 다루고 있다. 그렇다면 멀리 갈 필요가 없다. 하나로 쭉 연결할 수 있다. 단 코드가 없다. 그렇게 해서는 코드가 없다. 코드가 필요하다.

괴델 정리는 수리논리 책의 목표이기도 하다. 말로 읽으면 도대체 뭔지 모르겠다.

더글러스 호프스태터 (1979) GEB: 괴델, 에셔, 바흐 - 지식 사상 독창적 통합 이 책에 수리논리학:을 배울 수 있다니까

도서

  • “괴델, 에셔, 바흐: 영원한 황금 노끈 (1979) - 지식 사상 독창적 통합” (더글러스 호프스태터 2017) 원서 : Godel, Escher, Bach: An Eternal Golden Braid
  • “아인슈타인이 괴델과 함께 걸을 때” 짐 홀트 2020 노태복 (짐 홀트 2020)
  • “괴델 불완전성 정리 - 이성의 한계 발견” 요시나가 요시마사 2015 (요시나가 요시마사 2015)
  • 이 책에서 튜링 머신이 괴델 이론의 구현체 임을 말한다. (이광근 2017)

위키백과

  • “괴델의 완전성 정리” 2024

    (“괴델의 완전성 정리” 2024) 수리논리학에서 괴델의 완전성 정리(Gödel-完全性定理, 영어: Gödel’s completeness theorem)는 1차 논리에서 증명 가능한 명제의 집합은 모형을 갖는다는 정리다. 즉, 증명 이론으로 정의한 진리와 모형 이론으로 정의한 진리가 서로 일치한다. 이는 1차 논리의 가장 중요한 성질 가운데 하나이며, 고차 논리에서는 성립하지 않는다. 린드스트룀 정리에 따르면 1차 논리는 완전성과 콤팩트성을 만족하는 가장 강한 논리이다. 2차 논리 이상의 고차 논리에서는 완전성이 성립하지 않는다. 크립키 의미론을 이용하여 많은 경우 정규 양상 논리의 경우에도 완전성이 성립한다.

  • “괴델의 불완전성 정리” 2024 (“괴델의 불완전성 정리” 2024)

    • 괴델의 불완전성 정리(영어: Gödel’s incompleteness theorems)는 수리논리학에서 페아노 공리계를 포함하는 모든 무모순적 공리계는 참인 일부 명제를 증명할 수 없으며, 특히 스스로의 무모순성을 증명할 수 없다는 정리다.

  • “불완전성 정리” 2024 나무위키

“Mathematical Logic Through Python” Gonczarowski Yannai A 2022

Using a unique pedagogical approach, this text introduces mathematical logic by guiding students in implementing the underlying logical concepts and mathematical proofs via Python programming. This approach, tailored to the unique intuitions and strengths of the ever-growing population of programming-savvy students, brings mathematical logic into the comfort zone of these students and provides clarity that can only be achieved by a deep hands-on understanding and the satisfaction of having created working code. While the approach is unique, the text follows the same set of topics typically covered in a one-semester undergraduate course, including propositional logic and first-order predicate logic, culminating in a proof of Gödel’s completeness theorem. A sneak peek to Gödel’s incompleteness theorem is also provided. The textbook is accompanied by an extensive collection of programming tasks, code skeletons, and unit tests. Familiarity with proofs and basic proficiency in Python is assumed.

이 책은 독특한 교육적 접근 방식을 사용하여 학생들이 파이썬 프로그래밍을 통해 기본 논리적 개념과 수학적 증명을 구현하도록 안내함으로써 수학적 논리를 소개합니다. 프로그래밍에 능숙한 학생들의 독특한 직관과 강점에 맞춘 이 접근 방식은 이러한 학생들이 수학적 논리를 편안하게 접할 수 있도록 하며, 실습을 통한 깊은 이해와 실제 작동하는 코드를 만들었을 때의 만족감으로만 얻을 수 있는 명확성을 제공합니다. 접근 방식은 독특하지만, 괴델의 완전성 정리의 증명으로 마무리되는 명제 논리 및 일차 술어 논리 등 한 학기 학부 과정에서 일반적으로 다루는 주제와 동일한 내용을 담고 있습니다. 괴델의 불완전성 정리에 대한 간략한 설명도 제공됩니다. 이 교재에는 광범위한 프로그래밍 과제, 코드 골격, 단위 테스트가 함께 제공됩니다. 증명에 익숙하고 Python에 대한 기본적인 숙련도가 있다고 가정합니다

코드

  • </home/junghan/sync/code/logicpython> 홈페이지 그래도 가져옴

학습자들의 코드

목차

교과서 “Python을 통한 수학 논리"는 컴퓨터 과학 학부생에게 기본 논리 과정의 자료를 가르치는 새로운 접근 방식을 제시하며, 고유한 기술을 활용하여 점점 늘어나는 프로그래밍에 정통한 학생들에게 수학 논리를 편안한 영역으로 가져옵니다. 직관과 강점.

이 책의 접근 방식은 Python 프로그래밍 언어로 세심하게 설계된 일련의 프로그래밍 프로젝트를 사용하여 Logic의 수학적 분석의 본질을 포착합니다. 이 책의 각 장은 관련 프로그래밍 프로젝트에 대한 배경, 설명, 의미 및 수학적 처리를 제공합니다. 우리의 독특한 교육적 접근 방식과 그 동기에 대한 자세한 내용은 책의 소개(아래 “제 0장”)를 참조하세요.

DONE Preface 서문

Mathematical Logic 101 is a beautiful course. Gödel’s Theorems are arguably the most profound and deep truths taught throughout the entire undergrad theoretical curriculum. Nonetheless, it seems that among many computer science and engineering students this course suffers from the reputation of being an unintelligible course full of technical, unin- sightful proofs. Students lose themselves in endless inductions and do not fully understand what it means, e.g., to “prove that anything that is true can be proven.” Indeed, how can this not be confusing when the two occurrences of “prove” in that sentence have two distinct meanings – the latter referring to a precise very strict mathematical “proof” object that is defined during this course, while the former refers to the free-text proofs that we have been taught since our first year of undergrad? This book drastically reenvisions the Mathematical Logic 101 course, conveying the same material but tapping into the strengths of the ever- growing cohort of programming-oriented students to do so.

수학 논리 101은 훌륭한 강의입니다. 괴델의 정리는 틀림없이 학부 이론 전체를 통틀어 전체 학부 이론 커리큘럼에서 가르치는 가장 심오하고 깊은 진리입니다. 커리큘럼을 통틀어 가장 심오하고 깊은 진리입니다. 그럼에도 불구하고 많은 컴퓨터 과학 및 공학 학생들 사이에서 공학 학생들 사이에서 이 과목은 기술적인 내용으로 가득 찬 기술적이고 눈에 보이지 않는 증명으로 가득 찬 이해할 수 없는 과정이라는 평판을 받고 있습니다. 학생들이 잃는 것 끝없는 귀납에 빠져 그 의미를 완전히 이해하지 못합니다, 예를 들어, “참인 것은 무엇이든 증명할 수 있다는 것을 증명하라"는 식입니다. 사실, 어떻게 이 문장에서 “증명하다"가 두 번 등장할 때 혼란스럽지 않을까요? 두 가지 다른 의미를 가지고 있는데, 후자는 매우 엄격하고 정확한 이 과정에서 정의되는 수학적 “증명"객체, 반면에 전자는 우리가 처음 배운 이후로 배운 자유 텍스트 증명을 나타냅니다. 학부 1학년? 이 책은 수학 논리 101을 대폭 재구성하여 동일한 자료를 전달하지만 끊임없이 성장하는 프로그래밍 집단의 강점을 활용하는 과정 프로그래밍을 지향하는 학생 집단의 강점을 활용합니다.

How does one help programming-oriented students to not lose themselves among end- less little details in proofs, failing to see the overarching message of the course? We set out to make this course less abstract, more intuitive, and maybe even exciting, by tapping into the context where such students are used to comfortably dealing with endless little details on the way to a larger goal without ever missing the forest for the trees: computer programming. We redesigned the entirety of this very theoretical course from scratch to be based upon a series of programming exercises, each corresponding to either a theorem/lemma/corollary or a step toward such.

프로그래밍 지향적 인 학생들이 자신을 잃지 않도록 어떻게 도울 수 있습니까? 증명의 작은 세부 사항이 적고 중요한 메시지를 보지 못함 어떻게 도울 수 있을까요? 우리는 이 강좌를 덜 추상적이고 직관적이며 그러한 학생들이 익숙한 맥락을 활용하여 흥미 진진 할 수도 있습니다. 더 큰 목표를 향해 나아가는 과정에서 끝없는 작은 세부 사항을 편안하게 다루고 컴퓨터 프로그래밍이라는 큰 숲을 놓치지 않고 편안하게 다룰 수 있는 맥락을 활용했습니다. 우리는 이 이론적인 과정 전체를 처음부터 다시 설계했습니다. 일련의 프로그래밍 연습을 기반으로 하며, 각 연습은 다음 중 하나에 해당합니다. 정리/정리/결론 또는 이를 위한 단계에 해당하는 일련의 프로그래밍 연습을 기반으로 합니다.

For example, the main result of the first half of a standard Mathematical Logic 101 course is the “Tautology Theorem” (a variant of the Completeness Theorem for propositional logic), which asserts that every tautology – every statement that holds in every possible model or setting – can be proven to hold using a small set of axioms. The corresponding programming exercise in this book is to write a function (based on functions from previous exercises, of course) whose input is a formula (an object of class Formula, which the students implement in a previous exercise) and whose output is either a model in which this formula does not hold (i.e., a counterexample to the formula being a tautology) or a proof (an object of class Proof, which the students implement in a previous exercise) of this formula. Obviously, whoever can write such a function, including all its recursively implemented helper functions, completely understands the reasoning in the proof of the Tautology Theorem, including all its inductively proven lemmas. (And this holds even more so for students who naturally grasp recursive code far better than they do inductive proofs.) In our experience, students with a background in programming for the most part even understand this proof better having actively coded its functionality themselves than had they only passively seen the proof being written on the blackboard by a teacher. In the process of moving from proving to programming, we have in fact also disambiguated the two meanings of “prove” in the earlier statement of “prove that whatever is true can be proven”: we transformed the former “prove” into “program in code” and the latter “can be proven” into “is the conclusion of a valid Proof object.” This disambiguation by way of defamiliarization of each of these occurrences of “prove” achieves great clarity and furthermore allows the students to more easily reexamine their intuitions and unconscious assumptions about proofs.

예를 들어, 표준 수학 논리 101 강의 전반부의 주요 결과는 “긴장 정리”(명제 논리에 대한 완전성 정리의 변형)로, 모든 긴장 정리(가능한 모든 모델이나 설정에서 성립하는 모든 진술)가 작은 공리 집합을 사용하여 성립함을 증명할 수 있음을 주장합니다. 이 책의 해당 프로그래밍 연습은 입력이 공식(이전 연습에서 구현한 Formula 클래스의 객체)이고 출력이 이 공식이 성립하지 않는 모델(즉, 공식이 공리인 반례)이거나 이 공식에 대한 증명(이전 연습에서 구현한 Proof 클래스의 객체)인 함수(물론 이전 연습의 함수를 기반으로 합니다)를 작성하는 것입니다. 재귀적으로 구현된 모든 도우미 함수를 포함하여 이러한 함수를 작성할 수 있는 사람은 귀납적으로 증명된 모든 정리를 포함하여 긴장 정리 증명의 추론을 완전히 이해한 사람임이 분명합니다. (귀납적 증명보다 재귀적 코드를 훨씬 더 잘 이해하는 학생의 경우 더욱 그렇습니다.) 경험상, 프로그래밍에 대한 배경 지식이 있는 학생들은 교사가 칠판에 적는 증명을 수동적으로 보기만 했던 학생들보다 직접 코딩을 해본 후 이 증명을 더 잘 이해하기도 합니다. 증명에서 프로그래밍으로 넘어가는 과정에서 사실 “참인 것을 증명할 수 있다는 것을 증명한다"라는 앞의 진술에서 “증명하다"의 두 가지 의미도 모호해졌습니다. 전자의 “증명하다"는 “코드로 프로그램하다"로, 후자의 “증명할 수 있다"는 “유효한 증명 객체의 결론이다"로 바꿨습니다. 이러한 “증명하다"의 각 용례를 명확히 하는 방식으로 모호성을 제거함으로써 명확성을 높이고 나아가 학생들이 증명에 대한 직관과 무의식적 가정을 더 쉽게 재검토할 수 있도록 했습니다.

This book evolved from a course that we have been teaching at the Hebrew University of Jerusalem since 2017, first as an elective (we limited our class to 50 and then to 100 students as we fine-tuned the course, and there had been a waiting list) and later as an alternative for computer science and engineering students to the mandatory Mathematical Logic 101, to the clear satisfaction of the students, who continuously rank this course highly. In our experience, having the tasks of a single chapter due each week (if the schedule permits, then we try to allow an additional week for Chapter 10), with the tasks of Part I (Chapters 1 through 6) being solved by each student individually and the tasks of Part II (Chapters 7 through 12) being solved in pairs, has consistently proven to work well.

이 책은 2017년부터 예루살렘 히브리대학교에서 처음엔 선택 과목으로, 나중에는 컴퓨터 과학 및 공학 전공 학생들을 위한 필수 과목인 수학 논리 101의 대체 과목으로(수강 인원을 50명으로 제한했다가 수업을 미세 조정하면서 100명으로 늘렸고 대기자 명단이 생겼음) 가르치던 것을 발전시킨 것으로, 학생들의 만족도가 매우 높으며 계속해서 이 과목에 대한 평가가 매우 높습니다. 지금까지의 경험에 따르면, 매주 한 장의 과제를 제출하도록 하고(일정이 허락하는 경우 10장의 경우 1주일을 더 허용하려고 합니다), 파트 1(16장)의 과제는 각 학생이 개별적으로 풀고 파트 2(712장)의 과제는 짝을 지어 풀도록 하는 것이 꾸준히 효과적이라는 것이 입증되었습니다.

We are grateful to the Hebrew University students who took our course for their valuable questions and comments, and to our earlier students also for the faith they have put in us. We are indebted to our first TA and beta-solver, Alon Ziv, as well as to our subsequent TAs Noam Wies, Asaf Yehudai, Ofer Ravid, and Elazar Cohen, and beta-solvers Omri Cohen and Matan Harsat. A special thanks goes to Chagit Schiff-Blass, at the time a Law and Cognitive Science student, who showed us that our way of teaching Mathematical Logic really does appeal to an even more diverse student population than we had imagined, by first being an excellent beta-solver and then joining our teaching team. We thank Henry Cohn for valuable advice, and thank Aviv Keren and Shimon Schocken for their valuable detailed feedback on portions of earlier drafts of this book. We especially thank David Kashtan for careful and valuable scientific editing of this book on the logic side; any deviations from standard definitions or nomenclature are, of course, our own responsibility. Finally, we thank Kaitlin Leach, Rebecca Grainger, and the entire team at Cambridge University Press for their support and for their flexibility throughout the COVID pandemic. The cover picture by Vasily Kandinsky is titled “Serious-Fun,” and we hope that this will describe your experience as you work through this book. We always appreciate feedback from readers.

저희 강의를 수강한 히브리대학교 학생 여러분들의 소중한 질문과 의견에 감사드리며, 저희를 믿어주신 이전 수강생 여러분께도 감사드립니다. 첫 번째 조교이자 베타 해결사인 Alon Ziv를 비롯하여 이후 조교인 Noam Wies, Asaf Yehudai, Ofer Ravid, Elazar Cohen과 베타 해결사인 Omri Cohen과 Matan Harsat에게 큰 빚을 지고 있습니다. 특히 당시 법학과 인지과학 학생이었던 차짓 쉬프-클래스(Chagit Schiff-Blass)에게 특별한 감사를 표합니다. 그는 훌륭한 베타솔버로 활동한 후 저희 교육팀에 합류함으로써 수학 논리 교육 방식이 상상했던 것보다 훨씬 더 다양한 학생 집단에 어필할 수 있다는 사실을 보여주었습니다. 귀중한 조언을 해준 Henry Cohn에게 감사드리며, 이 책의 초기 초안 부분에 대한 귀중한 세부 피드백을 제공해준 Aviv Keren과 Shimon Schocken에게도 감사드립니다. 특히 이 책의 논리 측면에서 세심하고 가치 있는 과학적 편집을 해준 데이비드 카슈탄에게 감사드리며, 표준 정의나 명명법에서 벗어난 부분은 당연히 우리 자신의 책임입니다. 마지막으로, 코로나19 팬데믹 기간 동안 지원을 아끼지 않고 유연하게 대처해 준 케틀린 리치, 레베카 그레인저, 그리고 캠브리지 대학 출판부의 모든 팀원에게 감사의 말씀을 전합니다. 바실리 칸딘스키가 그린 표지 그림의 제목은 ‘진지한 재미’로, 이 책을 읽으면서 여러분의 경험을 묘사하는 데 도움이 되기를 바랍니다. 독자들의 피드백은 언제나 환영합니다.

1장: 명제 논리 구문

Chapter 1: Propositional Logic Syntax

2장: 명제 논리 의미론

Chapter 2: Propositional Logic Semantics

3장: 논리 연산자

Chapter 3: Logical Operators

4장: 공제에 의한 증명

Chapter 4: Proof by Deduction

5장: 증명 작업

Chapter 5: Working with Proofs

6장: 동어반복 정리와 명제논리의 완전성

Chapter 6: The Tautology Theorem and the Completeness of Propositional Logic

7장: 술어 논리 구문 및 의미론

Chapter 7: Predicate Logic Syntax and Semantics

8장: 함수와 평등의 제거

Chapter 8: Getting Rid of Functions and Equality

9장: 술어 논리 공식의 연역적 증명

  • Chapter 9: Deductive Proofs of Predicate Logic Formulas

10장: 술어 논리 증명 작업

Chapter 10: Working with Predicate Logic Proofs

11장: 연역정리와 Prenex 정규형

Chapter 11: The Deduction Theorem and Prenex Normal Form

12장: 완전성 정리

Chapter 12: The Completeness Theorem

13장: 수학적 논리 엿보기 II: 괴델의 불완전성 정리

Chapter 13: Sneak Peek at Mathematical Logic II: Gödel’s Incompleteness Theorem

치트시트: 이 책에 사용된 공리 및 공리적 추론 규칙

Cheatsheet: Axioms and Axiomatic Inference Rules Used in this Book

Index 색인

수리 논리 프로그래밍 파이썬 인덱스 목록

D

axiom, 76–78, 83, 85, 172 deduction theorem for predicate logic, 212, 242 for propositional logic, 78, 79, 82, 90, 101, 211 derivation tree, 15, 18, 21, 118, 119 diagonalization, 261 disjunction operator, see or operator disjunctive normal form, see DNF DNF, 32, 33, 35, 36, 39, 40, 46 DNF theorem, 32, 33, 46 double implication operator, see iff operator

EI axiom schema, 179, 181, 185, 216 encoding an inference rule by an axiom, 74, 86, 92 entailment in predicate logic, 169, 170, 254, 257 in propositional logic, 54, 55, 66, 67, 73, 92, 93, 97 equality relation semantics, 126, 138, 139, 141, 179 syntax, 112, 116, 138, 142, 231, 232, 238 equality-free analog of a formula, 138 of a model, 139–141 of a set of formulas, 142 ES axiom schema, 179, 181, 185, 216 evaluation of a formula, see truth value of a term (in predicate logic), see value exclusive or operator, see xor operator existential derivation, 192 existential introduction, see EI axiom schema existential quantifier semantics, 126, 127, 171, 178, 236 syntax, 112, 179, 215–217, 233, 237–239, 248, 249, 251, 252 existential simplification, see ES axiom schema existential witness, 233, 245, 248, 249, 251 existentially closed set of sentences, 232, 236, 245, 248, 249, 252 expression (in predicate logic), 121

F constant (nullary operator) semantics, 26, 49–52 syntax, 13, 79, 98 field, 205, 257

first-order logic, see predicate logic first-order predicate logic, see predicate logic formula in predicate logic, 112, 115, 116, 119, 121, in propositional logic, 13, 15, 16, 18, 20–22, 25,

Formula class :

of the predicates package (predicate logic), 112, 115 of the propositions package (propositional logic), 15, 16 free instantiation, 198 free occurrence (of a variable name), 120, 126, 127, 170, 171, 181, 216, 222 free variable name, 120, 126, 133, 159, 170, 171, 180, 212, 214, 216, 231, 238, 254 @frozen decorator, 16, 115 function invocation semantics, 125, 130, 133 syntax, 110, 129, 132, 133, 137, 231, 232, 238 function name, 110, 122, 125, 130, 131, 133 function-free analog of a formula, 132–134 of a model, 130, 131, 133 of a set of formulas, 137 Gödel numbering, 258, 259 group, 195, 256, 257 H, see Hilbert axiomatic system halting (by a program), 259–264 halting problem, 261–264 Henkin constant, see witnessing constant name Hilbert axiomatic system, 86, 89, 92–94, 97, 99, 101, 103, 104, 177 hypothetical syllogism, 78, 101 I0 axiom, 65, 76–78, 80, 83, 85, 172 I1 axiom, 76–78, 83, 85, 87, 172 I2 axiom, 80, 81, 83, 85, 87, 172 iff operator semantics, 42, 50, 51 syntax, 42 implication operator, see implies operator implies operator semantics, 26, 27, 49, 50, 73, 170 syntax, 14, 74, 77, 78, 87, 112 incompleteness, see completeness of a set of axioms incompleteness theorem, 258, 261–263 inconsistency, see consistency induction axiom schema, 206 inference (in predicate logic), 169, 170, 182, 189

inference rule in predicate logic, 160, 164, 166, 264 in propositional logic, 53–56, 60, 66, 67, 71, 72, 74, 76, 78, 92, 189 InferenceRule class, 53 instance (of a schema), 145–148, 152, 159, 161, 172, 173, 181, 245 instantiation (of a schema), see instance interpretation, 122, 130, 136, 138, 232 lemma, 69, 71, 72 lemma theorem, 71, 72, 77, 78, 83, 86, 99, 101, 103, 104 Löwenheim–Skolem theorem, 252 ME axiom schema, 181, 185, 196, 200, 202 meaning of equality axiom schema, see ME axiom schema model in predicate logic, 122, 123, 125, 126, 128, 130, 131, 133, 137, 140–142, 159, 169–171, 182, 231, 232, 236, 237, 239, 249, 252–254, 260, 265 in propositional logic, 25–30, 32, 34, 36, 37, 54, 55, 67, 73, 86, 87, 89, 90, 94–98, 101, 170, 254 Model class, 123 modus ponens, see MP inference rule monotonicity of a Boolean function, 50 MP inference rule, 73, 74, 77, 78, 80, 83, 85, 86, 160, 161, 164, 169–171, 173, 177, 190, 245 multiplexer operator, see mux operator mux operator, 43, 49, 50, 52 N axiom, 82, 83, 85, 172 n-ary function, see arity of a function n-ary operator, see arity of an operator n-ary relation, see arity of a relation nand operator semantics, 42, 49 syntax, 42 negation operator, see not operator NI axiom, 85, 87, 172 NN axiom, 85, 87, 172 non-implication operator, 52 nor operator semantics, 42, 49 syntax, 42 not operator semantics, 26, 30, 35, 49, 51 syntax, 13, 31, 33, 40, 79, 80, 86, 87, 103, 112, 214, 224, 233, 236, 239, 241, 242, 251, 254 notation infix, 22, 115 polish, 22, 115 postfix, see notation, reverse polish prefix, see notation, polish reverse polish, 22, 115

NP-completeness, 39, 40, 79 nullary operator, 41, see also arity of an operator operator, 14, 41, 43, 46, 49, 52, 97, 112, 238 or operator semantics, 26, 32, 35, 50, 52 syntax, 14, 32, 33, 40, 98, 104, 112 parametrized formula, 147, 149, 178–181, 217 parsing, 15, 18, 20, 117, 262 Peano arithmetic, 206, 258–260, 264, 265 predicate logic, 109 prefix-free, 20, 116 prenex normal form, 215, 216, 236, 237, 241, 249, 251 prenex normal form theorem, 216, 217, 230, 231, 252 primitive sentence, 232, 233, 236, 238, 239, 241, 242, 249 primitively closed set of sentences, 232, 236, 241, 242, 249, 252 program, 258–260, 262–264 proof, see also provability in predicate logic, 144, 160, 161, 169, 171, 172, 177, 182, 245, 251, 253, 255, 258, 262–265 in propositional logic, 60, 61, 66, 67, 69, 70, 74, 77, 87, 89, 90, 92, 94, 171, 172 proof by way of contradiction, 79, 80, 82, 83, 213, 214 Proof class of the predicates package (predicate logic), 161, 182 of the propositions package (propositional logic), 61, 69 propositional formula, see formula in propositional logic propositional logic, 13 propositional skeleton of a predicate-logic formula, 167, 170–173, 180, 240, 245 of an inference (in predicate logic), 189 provability, see also proof in predicate logic, 169, 170, 177, 182, 214, 216, 246, 250, 254, 257, 264 in propositional logic, 60, 66, 71, 72, 74, 77, 78, 80, 82, 83, 85, 89, 90, 92, 93, 97, 101, 172 Prover class, 182 quantification existential, see existential quantifier universal, see universal quantifier Quine arrow operator, see nor operator R axiom, 85, 90, 172 reduction, 39, 40 redundance of equality theorem, 142, 231, 232, 238 redundance of functions theorem, 137, 231, 232, 238 reflexivity axiom schema, see RX axiom schema of equality, 138

relation invocation syntax, 112 relation corresponding to function, 130, 131, 133, 135, 136 relation invocation semantics, 126, 130, 232 syntax, 133, 136, 233, 238 relation name, 112, 122, 126, 130, 131, 133, 138, 251 as a template (in a schema), 147, 181 Russell’s paradox, 209 RX axiom schema, 179, 181, 185, 196, 200 satisfiability, 30, 36, 37, 39, 40 schema, 145–147, 159, 169, 177–182, 231, 250, 252, 253, 255, 258, 264 Schema class, 145–147 schema equivalents of a propositional axiomatic system, 171, 172, 177, 178, 240, 250, 266 scope of quantification, 112, 127, 216 sentence, 180, 212, 231, 236–239, 241, 242, 244, 248, 249, 251, 254, 257, 260, 262, 265 Sheffer stroke operator, see nand operator Skolem’s paradox, 252 soundness of a predicate-logic formula, 159, 170 of a propositional formula, see tautology in propositional logic of a schema, 159, 170, 172, 181 of an inference (in predicate logic), 169, 170, 182 of an inference rule, 54, 55, 66, 67, 73, 74, 76, 80, 82, 85, 92–94, 98, 190 soundness theorem for predicate logic, 170, 172, 182, 231, 249, 252–254, 257, 264 for propositional logic, 66, 67, 84, 92, 93, 98, 254 of proofs by way of contradiction for predicate logic, 214, 254 for propositional logic, 82, 83, 93, 97 specialization (of an inference rule), 56, 57, 60, 66, 67, 71, 173 specialization provability lemma, 70, 71 specialization soundness lemma, 66, 67, 159 syllogism, 144, 184, 187, 191, see also hypothetical syllogism symmetry of equality, 138, 196 T constant (nullary operator) semantics, 26, 50, 51 syntax, 13, 98 T-preservation, 50 tautological implication, 188, 190, 191, 214, 240 tautology in predicate logic, 160, 161, 167, 169–172, 177, 180, 214, 231, 240, 245, 250 in propositional logic, 30, 36, 39, 55, 73, 90, 92, 160, 167, 171, 172 tautology theorem predicate-logic version, 176, 177, 240 propositional-logic version, 90, 92, 143, 172

template (in a schema), 145–147 term (in predicate logic), 110, 111, 116, 118, 121, 125 Term class, 110, 111 ternary operator, 43, see also arity of an operator testing, 7, 8 transitivity of equality, 138, 202 truth table, 29, 32–35, 43, 46, 49, 84 truth value of a predicate-logic formula, 126, 128, 133, 170, 180, 182, 240 of a propositional formula, 25–30, 32–35, 54, 67, 89, 97, 101, 170 UG inference rule, 160, 161, 166, 169–171, 180, 212, 214, 232, 245, 250 UI axiom schema, 178, 180, 181, 185, 216, 232, 249, 254 unary operator, 14, 41, 112, see also arity of an operator undecidability theorem, 261–263 unique readability theorem of predicate-logic formulas, 119 of propositional formulas, 21 of terms (in predicate logic), 118 uniquely named variables, 222 universal generalization, see UG inference rule universal instantiation axiom schema, see UI axiom schema of a predicate-logic formula, 186, 233, 243, 244, 249, 251 universal quantifier semantics, 126, 127, 170, 171, 178, 180, 182, 236 syntax, 112, 144, 178, 179, 215–217, 232, 233, 237–239, 244, 249, 251, 252, 254 universal simplification, see US axiom schema universally closed set of sentences, 232, 236, 243, 244, 249, 252 universe (of a model), 122, 130, 141, 232 US axiom schema, 179, 181, 185, 212–214, 216 value (of a term in predicate logic), 125, 139, 182 variable name in predicate logic as a template (in a schema), 146, 181 semantics, 125–127, 133, 182 syntax, 110, 112, 116, 133, 217, 222, 238 in propositional logic semantics, 25, 26, 28, 29, 32–37, 86, 97, 170 syntax, 13, 20, 22, 31, 33, 40, 56, 57, 86, 96, 167, 189 witnessing constant name, 245, 248 xor operator semantics, 42, 51, 52 syntax, 42 ZF, 210 ZFC, 210, 252, 253, 255, 258

Related-Notes

References

이광근. 2017. 컴퓨터과학이 여는 세계. https://www.yes24.com/Product/Goods/17976737.
요시나가 요시마사. 2015. 괴델 불완전성 정리 - 이성의 한계 발견. https://www.yes24.com/Product/Goods/59680.
더글러스 호프스태터. 2017. 괴델, 에셔, 바흐: 영원한 황금 노끈 (1979) - 지식 사상 독창적 통합. Translated by 박여성 and 안병서. https://www.yes24.com/Product/Goods/43828727.
짐 홀트. 2020. 아인슈타인이 괴델과 함께 걸을 때. Translated by 노태복. https://www.yes24.com/Product/Goods/90225942.
“불완전성 정리.” 2024. 나무위키. May 25, 2024. https://namu.wiki/w/%EB%B6%88%EC%99%84%EC%A0%84%EC%84%B1%20%EC%A0%95%EB%A6%AC.
“괴델의 불완전성 정리.” 2024. In 위키백과. https://ko.wikipedia.org/w/index.php?title=%EA%B4%B4%EB%8D%B8%EC%9D%98_%EB%B6%88%EC%99%84%EC%A0%84%EC%84%B1_%EC%A0%95%EB%A6%AC&oldid=37152926.
“괴델의 완전성 정리.” 2024. In 위키백과. https://ko.wikipedia.org/w/index.php?title=%EA%B4%B4%EB%8D%B8%EC%9D%98_%EC%99%84%EC%A0%84%EC%84%B1_%EC%A0%95%EB%A6%AC&oldid=37154029.
마지막 수정일자
스캇 (2023) LPFP: 하스켈 함수형-프로그래밍으로 배우는 물리학#이맥스 #인공지능 #패키지 #활용법