Past Seminars – Fall 2010

December 8 meeting
Speaker: Evan Goris (CUNY Graduate Center),
Title: Strand Space Techniques for the Inductive Method.
Abstract:

Two popular formalisms for analyzing security protocols are the Strand Space Method, a pen and paper analysis technique developed by Joshua Guttman, and the Inductive Method, a formalization in Higher Order Logic using the proof assistant Isabelle developed by Lawrence Paulson. The Strand Space Method is characterized by a large body of protocol independent theory that can readily be applied when analyzing specific protocols. Similar protocol independent theories have been developed for the Inductive Method as well but as the reasoning styles of the Strand Space Method and the Inductive Method are in a way complementary to each other, the ideas from the Strand Space Method are first transformed into complementary ideas and then applied. This, witnessed by the relatively small body of work in this direction (to the best of my knowledge only three publications by Millen, Ruess, Cortier, and Blanqui) might not always be that easy or even possible. A uniform way of using ideas from one method within another would thus be of great benefit.

I will show that a direct formulation of some of the Strand Space techniques on the traces of the Inductive Method is possible. This started as a little experiment within a larger project that tries to get a Strand Space view of trace based models that borrow features from the Inductive Method. A little to my surprise this experimental development turned out to be extremely simple, a little elegant, and more importantly of benefit to the Strand Space theory as well: the formalization of the Strand Space definitions, theorems, and proofs allows them to be factored into their essential parts which clarifies some relationships between them.

I plan to treat the Inductive Method and my formalization of Strand Space techniques in it in some detail. Only a very rough understanding of The Strand Space Model and its basic proof technique is necessary so I will spend only a little time on this.

This talk is essentially a progress report about an ongoing research.

November 23 meeting
Speaker: Can Baskent (CUNY Graduate Center),
Title: Paraconsistency, Topological Semantics, Homotopies and Games
Abstract:

In this talk, we will discuss paraconsistency in topological semantics, and define homotopies in that framework as a truth preserving operation and classification. Moreover, such topologies will give us “nice” and “familiar” algebraic structures. Based on these constructions, we will make some observations within the context of Brandenburger-Keisler paradox.

This talk is essentially a progress report about an ongoing research.

November 16 meeting
Speaker: Antonis Achilleos (CUNY Graduate Center),
Title: Complexity Questions in Justification Logic (the Second Exam)
Abstract:

The study of the complexity issues for justification logic started in 2000 and has since developed enough to provide upper and lower bounds for a variety of justification logics. However, Justification Logic is a relatively new area, so unlike Modal Logic the landscape is still very much under formation as far as Computational Complexity is concerned. This text tries to summarize the results in this area, while focusing on an effort to provide insight to the methods used to obtain upper complexity bounds.

November 9 meeting
Speaker: Sergei Artemov (CUNY Graduate Center),
Title: Multiplicity of Common Knowledge
Abstract:

We will discuss the notion of common knowledge within the classical epistemic logic framework. We consider four points of origin, each coming from a different body of motivations: David Lewis in “Convention,” 1969; Robert Aumann in “Agreeing to disagree,” 1976; John McCarthy in “On the model theory of knowledge,” 1978; S.A. in “Justified common knowledge,” 2006. In all of these approaches, the common knowledge operator CK(F) was intended to capture the iterative knowledge “A knows that B knows that A knows … ” which, in the classical environment, is informally represented by the “infinite conjunction” IC(F):
F & E(F) & EE(F) & EEE(F) & … .
Here E(X) is the statement “every agent knows X.”

Despite the obvious differences in modes of presentation (informal in Lewis, set-theoretical in Aumann, mostly model-theoretical in McCarthy et al., and mostly proof-theoretical in S.A.), these approaches all agree that CK(F) should logically imply each of the conjuncts in IC(F):
CK(F) => IC(F), (*)
thus postulating that “common knowledge” captures iterative knowledge.

However, there is no consensus concerning the additional condition
CK(F) <=> IC(F), (**)

which postulates that CK(F) is the weakest epistemic condition on F capturing iterated knowledge of F. To be precise, Lewis, McCarthy, and Artemov define CK(F) as (*) whereas Aumann opted for (**), which subsequently became a fundamental dominant model for common knowledge, in particular, in Game Theory.

There is a growing body of evidence that using (*), in addition to (**), as the notion of common knowledge can be beneficiary.

1. The “relaxed definition” (*) is easier to axiomatize and analyze, whereas the standard applications of common knowledge to epistemic scenarios work equally well for (*) and for (**).

2. Some problems, in particular, in Game Theory, need stronger notions of common knowledge than the one provided by (**). In particular, such standard sources of common knowledge as Public Announcements, generally speaking, comply with (*) rather than with (**). In belief revision, common knowledge (**) of rationality does not guarantee that “there is no irrationality in the system” and hence should be replaced by some versions of (*).

These considerations warrant a broad logical study of model (*) for common knowledge.

Slides of this lecture can be found here: CLseminarNov2010.pdf

October 26 meeting
Speaker: Junhua Yu (CUNY Graduate Center),
Title: Prehistoric Phenomena and Self-referentiality
Abstract:

In the Logic of Proofs (LP), terms are allowed in types, including types of the form t:F(t) which has a self-referential meaning. Kuznets showed that self-referentiality is necessary in S4-LP realization by offering an S4-formula such that any realization of it calls for a self-referential constant specification. In this work, we consider in a general setting why an S4-theorem can yield self-referentiality in the standard realization procedure. This work, though not finished, suggests that some structure on G3s (a Gentzen-style formulation of S4) proof trees may play an essential role here. In this presentation, we will first recall related results by Artemov and Kuznets and then define prehistoric relations in G3s trees, explain its role in realization procedure and the reason why they affect self-referentiality. We will also consider subsystems of G3s that are restricted by properties of prehistoric relations and study their connections to the realization procedure.

October 19 meeting
Speaker: Samson Abramsky (Oxford),
Title: From Lawvere to Brandenburger-Keisler: interactive forms of diagonalization and self-reference
Abstract:

We analyze the Brandenburger-Keisler paradox in epistemic game theory, which is a `two-person version of Russell’s paradox’. Our aim is to understand how it relates to standard one-person arguments, and why the `believes-assumes’ modality used in the argument arises. We recast it as a fixpoint result, which can be carried out in any regular category, and show how it can be reduced to a relational form of the one-person diagonal argument due to Lawvere. We give a compositional account, which leads to simple multi-agent generalizations. We also outline a general approach to the construction of assumption complete models.

October 13 meeting
Speaker: Sergei Artemov & Tudor Protopopescu (CUNY),
Title: Knowability from a Logical Point of View.
Abstract:

Knowability is analyzed in a logical framework with the alethic modality [] and the epistemic modality K. The Church-Fitch paradox shows that the verificationist knowability principle `all truths are knowable,’ F -> <>KF, yields an unacceptable omniscience property. Our semantical analysis establishes that the paradox is due to the knowability principle itself rather than to the Church-Fitch proof. The knowability principle fails because it misses the monotonicity assumption `F does not change from true to false in the process of discovery,’ hidden in the verificationist approach. Even if it was raining when Ann asked Bob to check for the rain, but the rain had stopped by the time Bob looked out, Bob’s answer will be “no rain.” Once monotonicity is made explicit, the resulting monotonic knowability accurately represents verificationist knowability and escapes the Church-Fitch paradox. Moreover, the conception of knowability from an intrinsically intuitionistic perspective leads to the same monotonic knowability, which we hence offer as the correct version of verificationist knowability and a resolution of the knowability paradox.

We also consider an alternative knowability principle `it is possible to know whether or not a given proposition holds’ and establish that it is stronger than monotonic knowability but also free from the Church-Fitch paradox.

These observations open the door to a bi-modal framework for the systematic study of knowability.

October 5 meeting
Speaker: Sergei Artemov & Melvin Fitting, CUNY
Title: Justification Logic II.
Abstract:

Justification logics are epistemic logics which allow knowledge and belief modalities to be `unfolded’ into justification terms: instead of []X one writes t:X, and reads it as `X is justified by reason t.” One may think of traditional modal operators as implicit modalities, and justification terms as their explicit elaborations which supplement modal logics with finer grained epistemic machinery. For all common epistemic logics their modalities can be completely unfolded into explicit justification form (Realization Theorem). In this respect Justification Logic reveals and uses the explicit, but hidden, content of traditional Epistemic Modal Logic.

The realization algorithms sometimes produce self-referential justification assertions c:A(c), that is, assertions in which the justification occurs in the asserted proposition. Self-referentiality of justifications is a new phenomenon which is not present in the conventional modal language. The self-referentiality of justifications is unavoidable in realization of some major modal logics, most notably S4.

This is the second part of the two-part survey. In addition to technical machinery, the survey examines in what way the use of explicit justification terms sheds light on a number of traditional problems in epistemology.

September 28 meeting
Speaker: Sergei Artemov & Melvin Fitting, CUNY
Title: Justification Logic I.
Abstract:

You may say, “I know that Abraham Lincoln was a tall man.” In turn you may be asked how you know. You would almost certainly not reply semantically, Hintikka-style, that Abraham Lincoln was tall in all situations compatible with your knowledge. Instead you would more likely say, “I read about Abraham Lincoln’s height in several books, and I have seen photographs of him next to other people.” One certifies knowledge by providing a reason, a justification.

Of Plato’s three criterion for knowledge as justified true belief, epistemic logic really works with only two of them: Hintikka semantics captures knowledge as true belief. Possible worlds and indistinguishability model belief, factivity brings a trueness component into play. But there is no representation for the justification condition. Justification logics supply the missing third component of Plato’s characterization of knowledge as justified, true belief.

This two-part survey presents the general range of justification logics as currently understood. It discusses their relationships with conventional modal logics. In addition to technical machinery, the survey examines in what way the use of explicit justification terms sheds light on a number of traditional problems in epistemology.

September 21 meeting
Speaker: Eric Martin, Sydney Australia
Title: Quantified modal logic, kappa-structures, and an application to the Rondogiannis-Wadge semantics of logic programs
Abstract:

We generalize the notion of structure to a notion of kappa-structure where kappa is an ordinal. Basically, a kappa-structure is a set consisting of closed atoms and lambda-structures, lambda kappa. A kappa-structure offers a natural interpretation to kappa-formulas, that is, formulas in which the modal operators of possibility and necessity are indexed by ordinals smaller than kappa, with indices going down as one goes inside the formula (e.g., Box_5(p wedge Diamond_3(q wedge Diamond_1 r wedge Diamond_2 s)) is a propositional 6-formula). We distinguish between the vocabulary V used to define a kappa-structure and the vocabulary V^* — a subset of V — used for reasoning (the language of axioms and theorems). In other words, we make some function (and predicate) symbols “unspeakable of”, which can be seen as a dual of the usual technique of enriching the language to build a canonical interpretation as far as completeness results are concerned. This justifies why using closed atoms in the definition of a kappa-structure is not restrictive. More essentially, it allows one to define a simple and general semantics for quantified modal formulas, by letting quantifiers range over (possibly “unspeakable”) names rather than individuals. It provides the power needed to go beyond the restrictions imposed by the fixed domain semantics, but avoids all the issues associated with quantification over arbitrary domains. We show how to embed the classical Kripke semantics into the proposed framework: a simple constraint on the class of kappa-structures under consideration allows one to retrieve that semantics (for which the indexes assigned to the modal operators are of course shown to be irrelevant). Then we discuss other classes of kappa-structures of interest. We show that one such class allows one to provide a classical semantics as a counterpart to the Rondogiannis-Wadge treatment of the well founded semantics of logic programs. where atoms are true_alpha or false_alpha for some ordinal alpha — true_0 and false_0 corresponding to classical true and false values, and true_alpha and false_alpha values getting less and less “true” and “false”, respectively, as alpha increases. Essentially, an atom p receives the value true_alpha or false_alpha in Rondogiannis-Wadge semantics of a logic program P if it is possible to logically derive Box_alpha p or Box_alpha neg p, respectively, from the modal expression of P in our framework.

August 31 meeting
Speaker: Sergei Artemov, GC CUNY
Title: To believe, or not to believe: that is the question
Abstract:

Imagine two rational players, Ann and Bob, with common belief of rationality playing a game of perfect information. The belief revision approach takes into account how Bob would react to being surprised by Anna’s hypothetical irrational move. There are various options:

1. Bob forfeits his belief in Anna’s rationality for the remainder of the game

2. Bob revises some of his beliefs, but maintains the belief in Ann’s rationality for the remainder of the game.

Stalnaker describes what happens when the first option is allowed and shows that the backward induction solution is not the only possible outcome. We show that the second case always leads to the backward induction solution.

This result demonstrates that the Stalnaker Theorem cannot be interpreted as stating that common knowledge of rationality does not yield backward induction. Stalnaker’s setup allows players to revise their beliefs about others’ rationality. This is not the epistemological understanding of ‘knowledge of rationality,’ which is not supposed to be defeasible, and, unlike belief, is not the subject of revision. Rather, the Stalnaker Theorem deals with ‘rationality and common belief of rationality.’

Slides of this lecture can be found here: CLseminarAug31-2010.pdf