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.
[A good introduction to the Paradox and its history may be found here:
http://plato.stanford.edu/entries/fitch-paradox/.]
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.
http://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.
