Spring 2010
Seminar in Computational Logic
Tuesday, 2:00pm – 4:00pm, room C415A (Graduate Center)
May 11 meeting
Speaker: Samuel Buchel, Bern University
Title: Road to Realization: Cut-Free Systems for Common Knowledge
By using justification terms to model common knowledge, Artemov’s systems of evidence based knowledge provide explicit versions for McCarthy’s `any fool knows’ common knowledge modality, where common knowledge of A is defined as an arbitrary fixed point of the operator \lambda X:(A and everyone knows X). Similarly our goal is to provide an explicit counterpart of the standard modal logic of common knowledge S4_n^C, where common knowledge is treated as the greatest fixed point of the same operator.
The process of realization which transforms theorems of modal logic into theorems of justification logics usually relies on well-behaved cut-free sequent systems. At the moment, realization is the major open problem for multi-agent justification logic with common knowledge. We give a survey of available cut-free sequent systems for the standard modal logic of common knowledge and discuss their suitability for realization. Most of these systems are of infinitary nature, i.e. they either employ a so-called \omega-rule which has infinitely many premises or they admit infinitely long branches in the proof trees.
May 4 meeting
room C415A
Speaker: Juha Kontinen, University of Helsinki
Title: Dependence logic. .
In this talk we discuss Dependence logic which incorporates the concept of dependence into first-order logic. We give the syntax and semantics of dependence logic and discuss its basic properties. We also show that, in expressive power, dependence logic coincides with that of existential second-order logic.
The main reference for the talk is the book by professor Jouko Väänänen: Dependence Logic: A New Approach to Independence Friendly Logic, London Mathematical Society Student Texts (No. 70) Cambridge University Press, 2007.
April 27 meeting
room C415A
Speaker: Sergei Artemov & Tudor Protopescu, Graduate Center, CUNY
Title: Knowability: A bigger picture
We suggest viewing knowability as a special case of a more general notion which we call verifiability. To say F is verifiable is to claim that it is possible to know F or it is possible to know ~F. We offer a bi-modal formalization of verifiability and study the corresponding Kripke models. This bigger picture allows us to explain why the Church-Fitch proof engenders the `paradox’ of knowability and how the more nuanced view of knowability which the verifiability framework provides does not, thus proving a resolution of the knowability paradox.
The general notion of verifiability opens the door to a formal logical framework for the representation of different kinds and strengths of knowability.
April 20 meeting (Two talks)
room C415A (NEW ROOM)
Speaker 1: Hidenori Kurokawa, Graduate Center
Title: Extended Dosen’s Pinciple and Proof-theoretic Semantics
Over decades we have seen proliferation of various non-classical logics in proof-theoretical foundations of logic. In this talk, we will attempt to give a uniform view of these logics. In order to do this, we introduce extended Dosen’s Principle, which is a generalized version of Dosen’s principle motivated by proof-theoretic studies of substructural logics using hypersequents. We then try to present a view of some issues discussed in proof-theoretic semantics that can be coherent with the extended Dosen’s principle.
Speaker 2: Ren-June Wang, Graduate Center
Title: Knowledge, Time, and Logical Omniscience
It is well-known that Modal Epistemic logic (MEL) suffers from the problem of logical omniscience. In this paper a new framework Timed Modal Epistemic Logic (tMEL) is introduced to deal with the problem. tMEL is modified from MEL such that the moment of time when an agent obtains his knowledge is present. With the help of such temporal components, we can determine what can be known by the agent within a reasonable time of reasoning, and hence agents modeled in tMEL is not logical omniscient. Our discussions will mainly be on the modal logic S4’s tMEL counterpart tS4, but the methods can be generalized to study the tMEL counterparts of other common modal logics. Both the semantics and axiomatic proof system will be provide, accompanied with the soundness and completeness results. Notice that the tS4 introduced here is parameterized by a set of logical formulas, which are supposed to be the agent’s initial logical knowledge of his own reasoning system. When this set of initial knowledge rich enough, every tS4 theorem is exactly an S4 theorem with temporal annotations. This work originates from the study of Justification Logic, which shapes many aspects of this paper; and it is also a direct response to the request to utilize the use of awareness functions such that time can be put into the picture. A generalized awareness function is used in the semantics to trace the time when each formula is deduced.
April 6 meeting
room C415A (NEW ROOM)
Speaker: J. Jeremy Meyers, Stanford
Title: Hybrid Logics for Boolean Algebras via Dominance Ordering
In this talk we consider axiomatizations in extended hybrid languages for Boolean algebras and Boolean contact algebras with the dominance relation as primitive. In particular we concentrate on completeness strategies up to bisimulation in several langauges for regular open/closed algebras over real fields. I also show how one can employ similar strategies to axiomatize complete and atomic Boolean algebras. We conclude musing over some related open questions in first order logic.
March 23 meeting
room C415A (NEW ROOM)
Speaker: Evangelia Antonakos, Graduate Center, CUNY
Title: Justified Knowledge is Sufficient
Three formal approaches to public knowledge are “any fool” knowledge by McCarthy et al (1970), Common Knowledge by David Lewis (1996) (and many others), and Justified (Common) Knowledge by Artemov (2004). We observe that the light-weight systems of Justified Knowledge and “any fool knows” coincide and suffice to solve standard epistemic puzzles for which heavier solutions based on Common Knowledge are offered by standard textbooks. Specifically we show that epistemic systems with Common Knowledge modality C are conservative with respect to Justified Knowledge systems on formulas p&Cq -> r, where p,q, and r are C-free. We then notice that formalization of standard epistemic puzzles can be made in the aforementioned form, hence each time there is a solution within a Common Knowledge system, there is a solution in the corresponding Justified Knowledge system.
March 16 meeting
room C415A (NEW ROOM)
Speaker: Antonis Achilleos, Graduate Center, CUNY
Title: Complexity upper bounds for JD4
In this talk, the basic concepts and methods needed to establish upper bounds for the computational complexity of justification logics J, J4, JT, LP and JD will be be presented. These concepts will be used to provide a missing upper bound concerning the complexity of JD4 and an algorithm that establishes this upper bound will be the result. It is discovered that a Fitting-like semantics of only two worlds is adequate to describe JD4; this proves to be very helpful in producing an effective tableau procedure, following the example of the cases of J, J4, JT, LP and JD.
The slides of this talk are available here: jd4semtalk.pdf
March 9 meeting
room C415A (NEW ROOM)
Speaker: Sergei Artemov, Graduate Center, CUNY
Title: Tracking the Evidence
In this case study we describe an approach to a general logical framework for tracking evidence within epistemic contexts. We consider as basic Russell’s well-known `prime minister example’ which features two justifications for a true statement, one which is correct and one which is not. We formalize this example in a system of Justification Logic with two knowers: the object agent and the observer, and we show that whereas the object agent does not logically distinguish between factive and non-factive justifications; such distinctions can be attained at the observer level by analyzing the structure of evidence terms. Basic logic properties of the corresponding two-agent Justification Logic system have been established, which include Kripke-Fitting completeness.
We also argue that a similar evidence-tracking approach can be applied to analyzing paraconsistent systems.
The full paper is available upon request.
February 16 meeting
Speaker: Mel Fitting, Lehman College, CUNY Graduate Center
Title: Formal models of knowledge-based rationality II
A mixture of propositional dynamic logic and epistemic logic is used to give a formalization of Artemov’s knowledge based reasoning approach (KBR) to game theory. The family of logics introduced is called PDL + E. It is not the same as Dynamic Epistemic Logic, instead PDL + E has its origins in work of Schmidt and Tishkovsky. Epistemic states of players, usually treated informally in game-theoretic arguments, are here represented explicitly and reasoned about formally. The heart of the presentation is a detailed analysis of the Centipede game using both the proof theoretic and the semantic machinery of PDL + E. The present work can be seen an argument for the thesis that PDL + E should be the basis of the logical investigation of game theory.
A preliminary version of a tech report presenting this work can be found here: CentipedeDraft.pdf. Comments are welcome.
On Feb 16 talk: I will continue with the second part of the talk begun last week. This time I will make the assumption that one of the players always plays irrationally, and use this as a device to help uncover missing formal assumptions concerning the Centipede game. The work in this part of the talk is in a less finished form than that of last week, and I will discuss what is still needed. I will also briefly discuss some related work of Johan van Benthem.
February 9 meeting
Speaker: Mel Fitting, Lehman College, CUNY Graduate Center
Title: Formal models of knowledge-based rationality
A mixture of propositional dynamic logic and epistemic logic is used to give a formalization of Artemov’s knowledge based reasoning approach (KBR) to game theory. The family of logics introduced is called PDL + E. It is not the same as Dynamic Epistemic Logic, instead PDL + E has its origins in work of Schmidt and Tishkovsky. Epistemic states of players, usually treated informally in game-theoretic arguments, are here represented explicitly and reasoned about formally. The heart of the presentation is a detailed analysis of the Centipede game using both the proof theoretic and the semantic machinery of PDL + E. The present work can be seen an argument for the thesis that PDL + E should be the basis of the logical investigation of game theory.
A preliminary version of a tech report presenting this work can be found here. Comments are welcome.
February 2 meeting
Speaker: Sergei Artemov, CUNY Graduate Center
Title: Knowing the Model
Why a typical epistemic problem, such as Muddy Children, Wise Men, etc., is normally formalized as an epistemic model with equivalence/partition possibility relations a.k.a. S5-models or Aumann structures? Even if agent’s logic is assumed to be S5, with both positive and negative introspection, the standard soundness theorems do not explain this phenomenon: S5-soundness =/=> S5-Aumann structure. The bare fact that all epistemic laws (S5) hold in a model M does not put any constraints on the accessibility of possible worlds in M.
We observe that in a typical epistemic scenario, the agent knows the model, i.e., knows possible worlds and accessibility relation. We then offer a formalization of knowing the model which uses nominals (propositional atoms true only at given nodes of the model). Speaking informally, knowledge of the model assumes that the agent knows which worlds are possible at any given node. A clear game-theoretical analogy to this is “knowledge of the game.” We show that knowledge of the model yields S5-Aumann structure of this model Knowledge of the model => S5-Aumann structure.
Conclusions.
– Using Aumann structures is justified by the virtue of knowing the model.
– There is an impossibility reading of this result: epistemic scenarios with non-S5 structure cannot be known in full to an S5-knower.
– The results extend to other logics of knowledge, such as T and S4.