Fall 2007
Seminar in Computational Logic
Tuesday, 2:00pm – 4pm, room 3305 (Graduate Center)
December 4 meeting
Speaker: Guram Bezhanishvili, New Mexico State University
Topic: Topological completeness in modal logic
We give an up-do-date overview of modal logics of topological spaces when modal diamond is interpreted as the closure operator of a topological space. We provide a modern account of the famous McKinsey-Tarski result that S4 is the modal logic of every dense-in-itself metrizable space, and discuss new topological completeness results for such important modal systems as S4, S4.1, S4.2, and S4.Grz.
November 27 meeting
Speaker: Pavel Naumov, McDaniel College
Topic: Cryptographic Protocols, Non-Zero-Sum Games, and Intuitionistic Logic
The goal of a multiparty computation is to evaluate a function of the individual inputs of some number of parties. A protocol for such a computation preserves privacy if it reveals to each party as little as logically possible about the individual inputs of the other parties.
We will argue that privacy properties for such protocols could be established by providing a set of winning strategies for a curtain non-zero-sum game based on the protocol. We also will propose an extension of the propositional intuitionistic logic for reasoning about strategies in this type of games and illustrate how this new logic could be used to verify multiparty protocols.
The talk is based on a joint work with Sara Miner More.
November 13 meeting
Speaker: Evangelia Antonakos, Graduate Center
Topic: The Logic of Proofs LP and three central results
Evangelia Antonakos will present Artemov’s logic of proofs LP. The development of LP was motivated by longstanding goals of Goedel, Kolmogorov and others to represent intuitionistic proofs within classical logic: in 1933 Goedel embedded IPC into S4 and the gap from S4 to PA has been bridged by LP. Three crucial theorems of LP will be presented: soundness and completeness with respect to arithmetic semantics (Artemov ’95), soundness and completeness with respect to epistemic semantics (Mkrtychev’97 and Fitting ’03), and realization of S4 in LP (Fitting’s proof of Artemov’s theorem). This lecture is the speaker’s Second Exam.
November 6 meeting
Speaker: Walter Dean and Hidenori Kurokawa, CUNY Graduate Center
Topic: From the Knowability Paradox to the Existence of Proofs via QLPE
The Knowability Paradox purports to show that from the premise (KP) If for all F, F is true, then F is possibly known it follows that all truths are already known. The argument by which this result follows was first devised by Fitch in 1963. Fitch’s argument takes as premise the plausible claim that we are non-omniscient — i.e.
(NonO) For some G, G is true and unknown.
The argument is presented in a bi-modal logic with operators K (“it is known that”) and <> (“it is possible that”). In this setting, (KP) and (NonO) are respectively formalized as
(KP1) for all F, F -> <>KF
and
(NonO1) for some G, G & ~KG.
Using only plausible modal principles governing K and <>, it may be shown that ~(G & ~KG), which in turn is classically equivalent to G -> KG. In the hands of modern commentators, the Knowability Paradox is often presented as a challenge to verificationism — i.e. the view that all meaningful statements (and so all truths) are verifiable.
Modern proponents of verificationism notably include intuitionistic logicians such as Dummett, Prawitz, and Martin-L\”of. In this paper, we present a logical system — the Quantified Logic of Proofs with Existence [QLPE] — which we argue is capable of representing the views of these theorists more accurately than do (KP1) and (NonO1). In this system, possible knowledge of F is formalized in terms of the existence of a proof of F and ignorance of G is formalized as our failure to have constructed a proof of G. This leads to formalizing (KP) and (NonO) as follows:
(KP2) for all F, F -> (\E x) x:F
(NonO2) for some G, G & \A x[E(x) -> ~x:G]
We argue that not only do these readings provide an interpretation of (KP) and (NonO) which is faithful to the goals of intuitionism, but also when they are formalized in this manner, no paradoxical conclusion follows from (KP) and (NonO). We show this is true in a local sense that the original derivation of the Knowability Paradox fails in QLPE and in a global sense by developing a semantics (based on Mkrtychev models) relative to which it may be shown that an instance of (NonO2) is consistent with all instances of (KP2). We close by comparing our resolution of the Paradox with several recent proposals by Edgington, Kvanvig and Burgess.
October 30 meeting
Speaker: Evan Goris, CUNY Graduate Center
Topic: A semantical proof of the completeness of MC_n for Q_n
Last week Professor Artemov presented the completeness of MC_n for Q_n. Here MC_n is the modal theory obtained from the normal modal logic T together with the minimal description of the knowledge of the individual agents at the beginning of the Muddy Children Puzzle with n children. Q_n is the knowledge model used throughout the literature for representing this initial setup semantically.
Artemov’s proof is proof theoretic and required to check, at least in principle, a huge number of cases, rapidly increasing with n. I will present a semantical proof that is uniform in n. The proof itself is rather short but makes use of some fundamental tools in modal logic that are worth going over in full detail.
October 23 meeting
Speaker: Sergei Artemov and Elena Nogina, CUNY Graduate Center)
Topic: Topological semantics of Justification Logic
The major epistemic modal logic S4 which in the context of the Logic of Proofs may be regarded also as a logic of explicit provability has a well-known Tarski’s topological interpretation. In this talk we extend Tarski topological interpretation from Modal Logic to Justification Logic systems with both modality []F and explicit justifications t:F. The topological semantics interprets []X and the interior of X (a topological equivalent of the `knowable part of X’), and t:X as a subset of X (a topological equivalent of `measurement t confirms X’). We establish a number of soundness and completeness results.
October 16 meeting
Speaker: Can Baskent, CUNY Graduate Center)
Topic: Topics in Subset Space Logic
In this talk, I will present some simple results in topologic. Topologic is the bimodal logic developed by L. Moss and R. Parikh to formalize the reasoning about sets and points.
I will first introduce the logic and mention the validity preserving operations in this logic. After that, i will briefly talk about the extensions of this logic with some additional operators. Then I will present evaluation games and bisimulation games both in the basic and extended languages of topologic.
After equipped with all these tools, i will consider public announcement logic in the language of topologic and present the simple completeness proof.
Finally, I will suggest an application of all these tools to the “methodology of mathematics” considering Lakatosian heuristics.
The talk is based on my Master of Logic thesis defended at the Institute for Logic, Language and Computation in Universiteit van Amsterdam.
October 9 meeting
Speaker: Mel Fitting, Lehman/CUNY Graduate Center
Topic: Justification Logics and Conservative Extensions
Several justification logics have evolved, starting with the logic LP. These can be thought of as explicit versions of modal logics, or logics of knowledge or belief, in which the unanalyzed necessity operator has been replaced with a family of explicit justification terms. Modal logics come in various strengths. For their corresponding justification logics, differing strength is reflected in different vocabularies. What we show here is that for justification logics corresponding to modal logics extending T, extensions are actually conservative. Our method of proof is very simple, and general enough to handle several justification logics not directly corresponding to modal logics. Our methods do not, however, allow us to prove comparable results for justification logics corresponding to modal logics that do not extend T. That is, we are able to handle explicit logics of knowledge, but not explicit logics of belief. This remains open.
September 25 meeting
Speaker: Sergei Artemov (CUNY Graduate Center)
Topic: Justification Logic by example.
We will give a light introduction into the basic Justification Logic and revisit the famous Gettier example (Case I). Using Fitting models, we will perform a missing assumption analysis and show that Gettier’s example hides an instance of Frege’s substitution puzzle.
September 11 meeting
Speaker: Evan Goris (CUNY Graduate Center)
Topic: Kuznetsov-Goldblatt-Boolos translation of epistemic logics in a general setting.
In this talk I will discuss what is known as the Kuznetsov-Goldblatt-Boolos (KGB) translation. The KGB translation takes a modal formula A and translates it to a modal formula A* by replacing each sub-formula of the form \box B of A by the formula \box B & B.
This translation first emerged in provability logic, matching up the notions of provability and strong provability. It’s crucial property there being:
Grz |- A iff GL |- A* iff S |- A*.
The KGB translation also has a clear meaning in other applications of modal logic: topology and epistemology. In the former the KGB translation expresses that the closure of a set X equals the union of X with the derivative of X. In the latter it can be taken to formalize the definition of knowledge as true belief.
After a specific motivating example from topology I will discuss the KGB translation in a general setting: for what normal modal logics S and L do we have S |- A iff L |- A* ? And what does this mean semantically? Then I will discuss these questions for epistemic logics S and L that contain negative introspection.
Reading:
E. Goris. Interpreting Knowledge into Belief in the Presence of Negative Introspection. CUNY Ph.D. Program in Computer Science Technical Reports, TR-2007005, 2007.
https://www.cs.gc.cuny.edu/tr/techreport.php?id=325
September 4 meeting
Speaker: Bryan Renne (Graduate Center CUNY)
Topic: Expressivity Questions in Dynamic Epistemic Logic II (continued from August 28)
Dynamic Epistemic Logic is the study of how to reason correctly about knowledge and communication. In this line of research, the term “update” is used to refer to an occurrence of a communication. Updates generally consist of a mixture of private and public information; after all, a communication is not always heard by everyone, and, furthermore, the individuals that do hear the communication may understand the content in a different way.
In this talk, I will describe Dynamic Epistemic Logic from the ground up. Beginning with Kripke models, we will work our way toward a family of logical languages for reasoning about various complicated kinds of updates that capture very general types of communication. Our eventual goal will be to look at issues of language expressivity, where we ask whether one logical language for reasoning about certain kinds of updates is able to say more or less than another logical language for reasoning about other updates. Answering expressivity questions allows us to understand whether a given update is more or less powerful than another.
We will also see a case where two updates have incomparable power: a recent result of the speaker provides a rigorous proof that public and private communication are fundamentally different (something we can all believe and yet it is rather intricate to show). The talk will conclude with the statement of a difficult unsolved problem that the speaker hopes to answer as part of his dissertation work.
August 28 meeting
Speaker: Bryan Renne (Graduate Center CUNY)
Topic: Expressivity Questions in Dynamic Epistemic Logic
Dynamic Epistemic Logic is the study of how to reason correctly about knowledge and communication. In this line of research, the term “update” is used to refer to an occurrence of a communication. Updates generally consist of a mixture of private and public information; after all, a communication is not always heard by everyone, and, furthermore, the individuals that do hear the communication may understand the content in a different way.
In this talk, I will describe Dynamic Epistemic Logic from the ground up. Beginning with Kripke models, we will work our way toward a family of logical languages for reasoning about various complicated kinds of updates that capture very general types of communication. Our eventual goal will be to look at issues of language expressivity, where we ask whether one logical language for reasoning about certain kinds of updates is able to say more or less than another logical language for reasoning about other updates. Answering expressivity questions allows us to understand whether a given update is more or less powerful than another.
We will also see a case where two updates have incomparable power: a recent result of the speaker provides a rigorous proof that public and private communication are fundamentally different (something we can all believe and yet it is rather intricate to show). The talk will conclude with the statement of a difficult unsolved problem that the speaker hopes to answer as part of his dissertation work.