Fall 2011
Seminar in Computational Logic
Tuesday, 2:00pm – 4:00pm, room 3309 (Graduate Center)
November 29 meeting
Speaker: Hidenori Kurokawa (Graduate Center CUNY)
Title: A structural-reflective view of logic
Abstract:
In this talk, we explore proof-theoretic foundations of logic. More specifically, we do this in putting an emphasis on understanding the nature of logical constants in non-classical logics from a uniform perspective. To do that, we first give a general view of logic by synthesizing a few philosophical views of logic currently available in the literature. In particular, we take a look at Dosen’s structural view of logic and Sambin et al.’s reflective view of logic (a similar view should be independently attributed to Avron). Based on these works and adding a twist, we present our own view, i.e., ‘a structural-reflective view of logic.’ Second, we claim that by adopting our own view we can give an answer to the conceptual question of whether or not modal operators are logical constants. We discuss what conditions are sufficient to accommodate significantly many modal logics from the point of view. We also argue that adopting the framework of hypersequents plays an important role in our way of handling modal logic.
November 22 meeting
Speaker: Robert Milnikel (Kenyon College)
Title: Embedding Answer Set Programming in Justification Logic
Abstract:
Answer Set Programming is a particular interpretation of logic programs with negation based on the Stable Model Semantics of M. Gelfond and V. Lifschitz. I will present a natural translation of finite propositional logic programs into the reflected fragment of the justification logic JD45 such that the JD45 models capture stable models of the original logic program. These are very preliminary results of a work in progress. No background in logic programming will be assumed, and relevant definitions and results of justification logic will be presented.
Speaker: Christian W. Bach
Title: Utility Proportional Beliefs
Abstract:
In game theory, basic solution concepts often conflict with experimental findings or intuitive reasoning. This fact is possibly due to the requirement that zero probability be assigned to irrational choices in these concepts. Here, we introduce the epistemic notion of common belief in utility proportional beliefs which also assigns positive probability to irrational choices, restricted however by the natural postulate that the probabilities should be proportional to the utilities the respective choices generate. Besides, we propose an algorithmic characterization of our epistemic concept. With regards to experimental findings common belief in utility proportional beliefs fares well in explaining observed behavior.
November 15 meeting
Speaker: Sergei Artemov (Graduate Center)
Title: Provability vs. computational semantics for intuitionistic logic
Abstract:
The intended semantics of first-order intuitionistic logic was the Brouwer-Heyting-Kolmogorov (BHK) semantics (1934) that explains intuitionistic validity using notions of proof and computable function (construction). BHK ideas inspired Kleene’s realizability (1945), which led to the class of computational interpretations based on the notion of a computable function. A good example of computational BHK semantics is given by Martin-Lof type theory. Since, in a formal mathematical setting, a computational program does not yield a proof of its correctness, a purely computational semantics cannot provide an adequate account of BHK proofs. On the other hand, formal proof of a sigma-formula yields a corresponding computational program, hence a proof-based semantics could, in principle, represent BHK in its entirety. In this talk we will discuss when exactly computational semantics deviates from BHK and show that the provability BHK developed in the framework of the logic of proofs (1995-2011) is free of these deficiencies.
November 8 meeting
Speaker: Andrei Rodin, ENS Paris
Title: Doing and Showing
Abstract:
The persisting gap between the formal and the informal mathematics is due to an inadequate notion of mathematical theory behind the current formalization techniques. I mean the (informal) notion of axiomatic theory according to which a mathematical theory consists of a set of axioms and further theorems deduced from these axioms according to certain rules of logical inference. Thus the usual notion of axiomatic method is inadequate and needs a replacement.
November 1 meeting
Speaker: Hidenory Kurokawa (Graduate Center)
Title: Tableaux and Hypersequents for Logic of Proofs and Provability
Abstract:
It is a natural question how we can combine GL and LP. Variants of the combined logic of proofs and provability (LPP, LPGL, and GLA) have already been explored. Arithmetic interpretations for LPP and LPGL have been established, and Fitting-style semantics is given for GLA. However, no tableau systems or sequent calculi for them have been proposed so far. In this talk, we present a cut-free prefixed tableau system and a cut-free hypersequent calculus for GLA. The main goal is to prove cut-admissibility of the hypersequent calculus for GLA by a semantic method. We prove this by using a translation from the prefixed tableau system to the hypersequent calculus. Along the way, we also study similar proof systems for a combined logic (GrzA) of proofs and strong provability, which means `provable in PA and true.’
October 25 meeting
Speaker: Junhua Yu (Graduate Center)
Title: Self-referentiality of the Brouwer-Heyting-Kolmogorov semantics for intuitionistic logic.
Abstract:
The problem of formalizing the intended provability semantics for intuitionistic propositional logic IPC (Brouwer-Heyting-Kolmogorov semantics, BHK semantics for short) was solved within Goedel-Artemov’s framework. According to this approach, IPC is embedded into modal logic S4 by Goedel translation, S4 is embedded into the Logic of Proofs LP via Artemov’s realization, and LP has a natural provability interpretation in Peano arithmetic. A principal feature of Artemov’s realization of S4 is that it makes use of self-referential LP-formulas of the form c:A(c), i.e., c is a proof of a formula containing c itself. Kuznets showed that there are S4-theorems that are impossible to be realized without using self-referential LP-formulas. In this paper we adapt Kuznets’ method to find IPC-theorems that call for such direct self-referentiality in LP. This suggests that BHK semantics of IPC is intrinsically self-referential.
October 18 meeting
Speaker: Rohit Parikh (Brooklyn College and CUNY Graduate Center)
Title: Knowledge and Uncertainty
Abstract:
We consider three issues.
– How does an agent choose in the face of uncertainty? Suppose an agent wants to choose between actions L and R. Each has a number of possible consequences, Some consequences of L are better than some of R and vice versa. Then how to choose?
– We show that there are various versions of rationality depending on whether an agent is cautious or aggressive or moderate. The famous experiment (reported by Kahneman) about the Asian Disease question can be explained as a switch from one version of rationality to another.
– Suppose agent M is in a position to control the knowledge that agents A and B (who are playing a game) have. Once their state of knowledge is determined they will play the game in a certain way. How should M pick the knowledge states of A and B so as to maximize the benefit to M herself.
Given the desired knowledge states of A and B (not only of facts but also of each other) we show that M can send signals to A and B so as to achieve this state of knowledge. Indeed a single (but complex) signal to each of A and B will suffice.
Note: This work was performed jointly with Cagil Tasdemir and Andreas Witzel (NYU). It is related to older work by Kannai, Peleg, Fishburn, Tauman, Zamir as well as to more recent work by Artemov and Aumann.
October 11
Speaker: Ren-June Wang (Graduate Center) – dissertation proposal
Title: Timed Modal Epistemic Logic
Abstract:
The thesis consists of three parts. In the first part, a survey of epistemic logic will be given. Epistemic logic was first introduced by philosophers, and later found its applications in fields such as Computer Science and Economics. This survey will cover both the philosophical debates and applications of epistemic logic and also discussions of the logical omniscience problem will be included.
The second part is the introduction of a new logical framework called timed Modal Epistemic Logic, tMEL. tMEL is extended from ordinary modal epistemic logic, MEL, by adding numerical labels to knowledge statement to indicate when the statement is known. We will argue that a logical framework with the expressivity for reasoning about both knowledge and the time of reasoning can help to resolve the problem of logical omniscience, and tMEL serves well as a logically non-omniscient epistemic system.
Finally, we will discuss the syntactical relations between MEL, tMEL, and Justification Logic, from which the study of MEL is originated, and the focus will be on the relations between axiomatic proofs in these logical frameworks. We will first determine a proper subclass of modal logical proofs called non-circular, and prove that this class of proofs is complete. And then we will show that every non-circular MEL proof can be turned into a tMEL proof by finding suitable number labels, and prove that there is a two-way translation between proofs in tMEL and Justification Logic. Combining these results, a formal connection between non-circular proofs and proofs in Justification Logic can be established, and the whole procedure will give us an alternative algorithm for the realization between theorems in modal logic and Justification Logic.
September 27 meeting
Speaker: Arnon Avron (Tel Aviv University)
Title: Non-deterministic Matrices and Modular Semantics of Rules
Abstract:
We show how one can provide in a lot of cases simple modular semantics for rules of inference, so that the semantics of a system is obtained by joining the semantics of its rules in the most straightforward way. Our main tool for this task is the use of finite non-deterministic matrices, which are multi-valued structures in which the value assigned by a valuation to a complex formula can be chosen non-deterministically out of a certain nonempty set of options.
September 20 meeting
Speaker: Melvin Fitting (Graduate Center CUNY)
Title: Possible World Semantics for FOLP.
Abstract:
First Order Logic of Proofs (FOLP) has been formulated by Artemov and Yavorskaya. Their work includes an axiomatic formulation, an arithmetic completeness theorem, and a realization theorem. Here we add to all this a possible world semantics, and an Mkrtychev semantics, for FOLP, with appropriate soundness and completeness proofs. We also show a first order analog of completeness with respect to fully explanatory models. We believe the possible world semantics provides additional insight into the handling of the quantifiers in FOLP. It is remarkable that the first order results do not involve any special tricks, but instead are natural extensions of what worked in the propositional setting.
September 13 meeting
Speaker: Sergei Artemov (Graduate Center CUNY)
Title: Toward first-order justification logic II
Abstract:
We will study first-order logic of proofs FOLP and outline first-order justification logic. In part I of this talk, we will revisit the Brouwer-Heyting-Kolmogorov semantics as the principal motivation and introduce FOLP in its current “official” form.
In this talk we will establish the realization theorem of modal logic FOS4 by FOLP. Together with the well known result about Goedel’s embedding of intuitionistic first-order logic HPC into FOS4, this provides the semantics of proofs for HPC as well. We will then show that this realization satisfies Brouwer-Heyting-Kolmogorov requirements.
Reading: the first three sections of Sergei N. Artemov and Tatiana Yavorskaya (Sidon). First-Order Logic of Proofs. Technical report TR-2011005 of the Ph.D. Program in Computer Science at CUNY Graduate Center.
September 6 meeting
Speaker: Sergei Artemov (Graduate Center CUNY)
Title: Toward first-order justification logic I
Abstract:
We will study first-order logic of proofs FOLP and outline first-order justification logic. In part I of this talk, we will revisit the Brouwer-Heyting-Kolmogorov semantics as the principal motivation and introduce FOLP in its current “official” form.