Courses

Computability Theory

(KV Krishna)

Abstract

What are the fundamental limits of computation? Do there exist well-defined problems that no computer, regardless of its power, can ever solve? This course offers a concise introduction to the core ideas of computability theory (also known as recursion theory), focusing on the boundary between the computable and the uncomputable. We begin by formalising the intuitive notion of an algorithm through models such as Turing machines and recursive (μ-recursive) functions, highlighting their equivalence under the Church–Turing thesis. Building on this foundation, we explore the classification of problems into decidable and undecidable sets, culminating in the landmark result of the Halting Problem. The series then develops the key technique of reduction to demonstrate undecidability in a broad range of settings, alongside an introduction to Rice's theorem and its implications. We also examine how computable functions can be constructed from simple initial functions using composition, primitive recursion, and minimisation, offering an arithmetic perspective on computation. We also touch on the structure underlying degrees of unsolvability and reflect on the broader significance of these results in logic, computer science, and the philosophy of computation. The course shall be accessible to anyone with a basic background in discrete mathematics.

Proofs vs Programs Correspondence

(SP Suresh)

Abstract

Proofs vs. Programs Correspondence (aka the Curry-Howard Isomorphism, aka the Propositions as Types Correspondence) is the explication of a deep connection between logic and computation: propositions in a logic correspond to types in a programming language; proofs of propositions correspond to programs of the corresponding type; and simplification of proofs corresponds to evaluation of programs. This correspondence can be applied to a wide variety of logics (discovering the programming language analogue of intuionistic logic, classical logic, second-order logic, etc.). It can also be applied a wide variety of language features (discovering the logical analogue of polymorphism, continuations, concurrency, etc.). Many ideas discovered independently by logicians and computer scientists, have turned out to be intimately related via the Curry-Howard correspondence. We introduce the basics of this fascinating topic in this series of lectures.

Reference to Abstract Entities

(Eric Snyder)

Abstract

By definition, abstract entities are entities which exist outside of space and are causally inefficacious, i.e. they cannot causally interact with anything. Prototypical examples of abstract entities include numbers, sets, functions, properties, shapes, species, colors, linguistic types, and institutions. For each of these entities, we can seemingly use singular terms (expressions whose express purpose is to refer) to refer to them. For example, we can refer to numbers using expressions like 'the number two', and we can refer to colors using expressions like 'the color red'. Such reference is puzzling, however, for two reasons. First, in many cases it threatens paradox. Thus, even if we can refer to properties, we seemingly cannot coherently refer to the property whose instances are all and only properties. Secondly, many philosophers have thought that reference is causally constrained in the sense that we cannot refer to what we cannot causally interact with. The purpose of this course is to introduce the variety of abstract entities we can seemingly refer to, the linguistic means by which we do that, and the philosophical challenges such reference poses for our best semantic and metasemantic theories.

Abhāva: Categorising what there is not

(Shikha Rajpurohit)

Abstract

The Nyāya-Vaiśeṣika schools of Indian philosophy talk of abhāva (absence) as a category (padārtha) of knowledge, asserting that it is a perceptible reality. If there is no pen on the table, how do these schools prove that its absence is an objective fact and not imagination? What use is the category of objects that are not even present? How would their absence be defined, and on what basis would they be differentiated? We will analyse these issues by examining the historical evolution of the concept of absence within the Nyāya-Vaiśeṣika framework. The early Nyāya texts do not consider absence as a category of reality. The discussion is primarily to refute it as an independent pramāṇa (means of knowledge). According to the Nyāya Sūtra, absence cannot be a pramāṇa because there is no object which is known by it. While the Vaiśeṣika Sūtra defines four types of absences, they are initially not included in its list of categories. This talk traces this historical shift that moved absence from the realm of inferential knowledge to the core of realist ontology by syncretising both systems. While doing so, it highlights that conceptual frameworks evolve through a dynamic interaction between diverse philosophical standpoints.