Advances in Mathematical Logic:
Computability Logic
(可计算性逻辑)
Graduate course taught at the Institute of Logic and Intelligence, Southwest University (西南大学 逻辑与智能研究中心) in June 2018 by
Giorgi Japaridze (乔治。札帕日泽)
- The professor 教授
- Briefly about computability logic 可计算性逻辑简介
- Syllabus 教学大纲
- Lecture notes 讲稿
- Homework assignments 课外作业
Giorgi Japaridze holds two
PhDs, one in philosophy (logic) from Moscow State University and the other in
computer science from the University of Pennsylvania. Currently he works in the
Computer Science Department of Villanova University, USA. The primary area of
his research interests is logic and its applications in computer science.
Computability logic - the subject of the present course - is an approach
introduced by him.
乔治.札帕日泽 拥有两个博士学位：逻辑学(莫斯科大学) 和 计算机科学(宾夕法尼亚大学）。现在是美国维拉诺瓦大学计算机科学系的教授。主要研究领域：逻辑学以及逻辑学在计算机科学中的应用。可计算性逻辑 （这次课程的题目）-- 是他提出来的。
- 办公室: 何教授的办公室
- 办公时间: 上课前一个小时，或者预约.
- Email: giorgi.japaridze@villanova.edu
- 电话: (023) 682 931 91
- 个人网页: http://www.csc.villanova.edu/~japaridz/
- 最近的照片
Briefly about computability logic 可计算性逻辑简介
Computability is one of the most interesting and fundamental concepts in mathematics, philosophy and computer science, and it is natural to ask what logic it induces. This is where Computability Logic (CoL) comes in. It is a formal theory of computability in the same sense as classical logic is a formal theory of truth. In a broader and more proper sense, CoL is not just a particular theory but an ambitious and challenging program for redeveloping logic following the scheme “from truth to computability”.
Under the approach of CoL, logical operators stand for operations on computational problems, formulas represent such problems, and their “truth” is seen as algorithmic solvability. In turn, computational problems --- understood in their most general, interactive sense --- are defined as games played by a machine against its environment, with “algorithmic solvability” meaning existence of a machine which wins the game against any possible behavior of the environment. With this semantics, CoL provides a systematic answer to the question “what can be computed?”, just like classical logic is a systematic tool for telling what is true. Furthermore, as it happens, in positive cases “what can be computed” always allows itself to be replaced by “how can be computed”, which makes CoL of potential interest in not only theoretical computer science, but many applied areas as well, including constructive applied theories, interactive knowledge base systems, resource oriented systems for planning and action, or declarative programming languages. On the philosophical side, CoL provides new insights into the foundations of logic and constructivism.
Currently CoL is still at
an early stage of development, with open problems prevailing over answered
questions. For this reason it offers plenty of research opportunities, with
good chances of interesting findings, for those with interests in logic and its
applications in computer science.
Computability Logic Homepage (a comprehensive online overview
of the subject).
可计算性无疑是数学、哲学和计算机科学中最有趣的、基本的概念之一。人们自然会问它推导出来的是什么逻辑，可事实上这个问题不仅从未得到过回答，甚至在相关的广泛领域里从来还没有被提及过，这正是可计算性逻辑的起源。它是可计算性的形式理论，正如经典逻辑是真理的形式理论。更确切的说，可计算性逻辑不是一种特定的理论，而是一个充满雄心和挑战的计划 ，为在“从真理到可计算性”框架下重振逻辑。
计算和可计算问题在可计算性逻辑中被最普遍地理解为交互的，它们被当作一种博弈。博弈的一方是机器（计算机、智能体、机器人），另一方是环境（用户、自然、或者魔鬼本身 ），问题的可计算性意味着存在一个机器总能赢得这个博弈，逻辑运算表示在可计算问题上的操作，一个逻辑公式的有效性表示它存在“总是可计算的”问题。 由于这一语义，可计算性逻辑提供系统性的答案，“什么是可以计算的”的问题。就象经典逻辑是告诉我们“什么是真理”的系统性的工具。并且，可计算性逻辑的实例不仅是关于“什么是能计算的”，相同程度的也关于“如何被计算”。这个让可计算性逻辑不但在计算理论方面，而且许多应用领域也有潜在的优势。包括构造的应用理论、交互知识库系统、或者宣告式编程。在哲学方面，可计算性逻辑为逻辑的基础和构成主义提供新的视角。
可计算性逻辑目前还处于初级阶段，未解决的问题超过已解决的问题。因此，它可以为那些对逻辑感兴趣的人们提供很多研究的好机会。
Syllabus 教学大纲
Meeting times and place 授课时间：周三19:00-21:00, 周四19:00-21:00. 课室: 学术报告庁
There is no textbook for this course. All written materials that you may need (including lecture notes) will be made available through this web site.
Topics: Turing machines; The Church-Turing
thesis; The traditional notions of computability, decidability, recursive
enumerability; The fundamental limitations of algorithmic methods; Mapping
reducibility; Turing reducibility; Kolmogorov complexity; Games as universal
models of an agent's interaction with the environment; Static vs. dynamic
games; Interactive Turing machines; Interactive computability; Interactive
version of the Church-Turing thesis; Game operations (negation; choice,
parallel, blind and recurrence operations); Computational meanings of logical
formulas; "Truth" as computability; Logical versus extralogical
validity; Cirquent calculus; System CL4; Knowledgebase systems, planning
systems and applied theories based on computability logic.
Grading: There will be a comprehensive
examination at the end of the course, contributing 70% toward your final grade.
The remaining 30% will come from quizzes which will be given 2 to 6 times
without warning, during the first 10 minutes of the class. Homework will be
posted after every meeting. It will not be collected or graded. However, the
questions asked on a quiz or examination will be mostly based on (or be
identical with) homework questions. Students who listen actively, participate
in discussions and volunteer answering questions may receive some extra credit
at the time of deriving final grades.
1. Introduction What is computability logic.
Computability logic versus classical logic. Unifying classical,
“intuitionistic” and “linear” logics. The current state of development.
2. Mathematical
and computability-theoretic preliminaries Sets. Sequences. Functions.
Relations. Strings. Turing machines. The traditional concepts of computability,
decidability and recursive enumerability. The limitations of the power of
Turing machines. The Church-Turing thesis. Mapping reducibilty. Turing
reducibility. Kolmogorov complexity
3. Games Games as models of interactive
computational tasks.The two players. Moves, positions and runs. Games defined.
Prefixation. Traditional computational problems as games. Departing from
functionality. Departing from the input-output scheme. Departing from the
depth-2 restriction. Classical propositions as games.
4. Gameframes Propositional versus first-order
CoL. Constants and variables. Universes. Gameframes defined. Classical
predicates and functions revisited. Predicates as elementary gameframes.
Unilegal runs and unistructural gameframes. Visualizing unistructural
gameframes. Substituting functions for variables.
5. Negation
and choice operations
About the operations studied in computability logic. Negation. The double
negation principle. Choice conjunction and disjunction. Choice quantifiers.
DeMorgan's laws for choice operations. The constructive character of choice
operations. Failure of the principle of the excluded middle for choice
disjunction.
6. Parallel
operations
Parallel conjunction and disjunction. Free versus strict games. The law of the
excluded middle for parallel disjunction. Resource-consciousness. Differences
with linear logic. Parallel quantifiers. DeMorgan's laws for parallel
operations. Evolution trees and evolution sequences.
7. Reduction The operation of reduction and the
relation of reducibility. Examples of reductions. The variety of reduction
concepts and their systematization in computability logic. Mapping reducibility
is properly stronger than (simply) reducibility.
8. Blind quantifiers Unistructurality. The blind
universal and existential quantifiers defined. DeMorgan's laws for blind
quantifiers. The hierarchy of quantifiers. How blind quantification affects
gameframe trees.
9. Recurrence
operations What the recurrences are all about. An
informal look at the main types of recurrences. Parallel recurrence versus
branching recurrence. Formal definition of parallel (co)recurrence. Evolution
sequences for parallel recurrences. Rimplicative reductions. Primplicatively
reducing multiplication to addition. Primplicatively reducing the RELATIVES
problem to the PARENTS problem. Primplicatively reducing the Kolmogorov
complexity problem to the halting problem. Brimplication: the ultimate concept
of algorithmic reduction. Definition of branching (co)recurrence. Evolution
sequences for branching recurrences. A look at some valid and invalid
principles with recurrences. Alternative definition of branching
(co)recurrence.
10. Static games Some intuitive characterizations of
static games. Dynamic games. Pure computational problems = static games.
Delays. Definition of static games.
11. Interactive
computability Hard-play machines. Easy-play machines.
Definition of interactive computability. The interactive version of the
Church-Turing thesis.
12. The
language and formal semantics of computability logic The formal language. Interpretations.
Validity. Logical or extralogical validity? Computability versus “knowability”.
Closure under Modus Ponens. Other closure theorems. Uniform-constructive
closure.
13. Cirquent
calculus
About cirquent calculus in general. The language of CL5. Cirquents. Cirquents as circuits. Formulas as cirquents.
Operations on cirquents. The rules of inference of CL5. The soundness and completeness of CL5. A cirquent calculus system for classical logic. CL5 versus affine logic.
14. Logic CL4 The language of CL4. The rules of CL4. CL4 as a conservative extension of
classical logic. The soundness and completeness of CL4. The decidability of the blind-quantifier-free fragment of CL4. Other axiomatizations (affine and
intuitionistic logics).
15. Applied
systems based on computability logic Computability logic as a
problem-solving tool. Knowledgebase systems based on computability logic.
Constructiveness, interactivity and resource-consciousness. Systems for
planning and action based on computability logic. Applied theories based on
computability logic. CoL-based arithmetic.