**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).

可计算性无疑是数学、哲学和计算机科学中最有趣的、基本的概念之一。人们自然会问它推导出来的是什么逻辑，可事实上这个问题不仅从未得到过回答，甚至在相关的广泛领域里从来还没有被提及过，这正是可计算性逻辑的起源。它是可计算性的形式理论，正如经典逻辑是真理的形式理论。更确切的说，可计算性逻辑不是一种特定的理论，而是一个充满雄心和挑战的计划 ，为在“从真理到可计算性”框架下重振逻辑。

计算和可计算问题在可计算性逻辑中被最普遍地理解为交互的，它们被当作一种博弈。博弈的一方是机器（计算机、智能体、机器人），另一方是环境（用户、自然、或者魔鬼本身 ），问题的可计算性意味着存在一个机器总能赢得这个博弈，逻辑运算表示在可计算问题上的操作，一个逻辑公式的有效性表示它存在“总是可计算的”问题。 由于这一语义，可计算性逻辑提供系统性的答案，“什么是可以计算的”的问题。就象经典逻辑是告诉我们“什么是真理”的系统性的工具。并且，可计算性逻辑的实例不仅是关于“什么是能计算的”，相同程度的也关于“如何被计算”。这个让可计算性逻辑不但在计算理论方面，而且许多应用领域也有潜在的优势。包括构造的应用理论、交互知识库系统、或者宣告式编程。在哲学方面，可计算性逻辑为逻辑的基础和构成主义提供新的视角。

可计算性逻辑目前还处于初级阶段，未解决的问题超过已解决的问题。因此，它可以为那些对逻辑感兴趣的人们提供很多研究的好机会。

**S****yllabus 教学大纲**

**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 non-logical
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. ** Constant
games**
Games as models of interactive computational tasks.The two players. Moves,
positions and runs. Constant 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. ** Not-necessarily-constant
games**
Propositional versus first-order CoL. Constants and
variables. Universes. Not-necessarily-constant games defined. Classical
predicates and functions revisited. Predicates as elementary games. Unilegal runs and unistructural games. Visualizing
unistructural games. 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 game 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 nonlogical 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

14. ** Logic CL4** The language of

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.