Blog ArchivesThese are the items posted in this seminar, currently ordered by their post-date, rather than by the event date. We will create improved views in the future. In the meantime, please click on the Seminar menu item above to find the page associated with this seminar, which does have a more useful view order.
We will survey the standard modal logic approach to model the “knowledge vs justified true belief” scenarios, in particular its recent account in Williamson, Timothy “A note on Gettier cases in epistemic logic” Philosophical Studies 172.1 (2015): 129-140. We argue that the “old school” approach by Williamson to model justified belief as a modality without going deeper to the level of individual justifications is rather limited. Whereas it indeed suffices to satisfactory treat Gettier examples with a unique justification in the picture, it fails even on simplest examples with more than one justification, e.g., Russell’s Prime Minister Example. On the constructive side, we offer a principled way to building epistemic models entirely from systems of justifications; standard epistemic models are special cases of these evidence-based epistemic models. New models cover wide range of epistemic scenarios, including Russell’s example, in a natural way.
Evidence aggregation is a well-known problem which appears naturally in many areas. A classical approach to this problem is via Bayesian probabilistic evidence aggregation. Our approach is radically different. We consider the following situation: suppose a proposition X logically follows from a database — a set of propositions D which are supported by some known evidence, vector u of events in a probability space. We answer the question of what is the best aggregated evidence for X justified by the given data. We show that such aggregated evidence e(u) could be assembled algorithmically from the collection of all logical derivations of X from D. This approach can handle conflicting and inconsistent data and allows the gathering both positive and negative evidence for the same proposition. The problem is formalized in a version of justification logic and the conclusions are supported by corresponding completeness theorems.
Intuitionistic epistemic logic, IEL, introduces to intuitionistic logic an epistemic operator which reflects the intended BHK semantics of intuitionism. The fundamental assumption concerning intuitionistic knowledge and belief is that it is the product of verification. The BHK interpretation of intuitionistic logic has a precise formulation in the Logic of Proofs, LP, and its arithmetical semantics. We show here that the Gödel embedding, realization, and an arithmetical interpretation can all be extended to S4 and LP extended with a verification modality, thereby providing intuitionistic epistemic logic with an arithmetical semantics too.
Intuitionistic truth is proof-based, and intuitionistic knowledge is the result of verification. The corresponding logic IEL of intuitionistic knowledge (Artemov and Protopopescu, 2014) has offered a principled resolution of the Fitch-Church knowability paradox. In this talk we will analyze paradigmatic Russell and Gettier examples from intuitionistic epistemic positions, both informally, and formally within proper versions of IEL.
Time permitting, we will discuss the list of possible research projects.
In this talk, we discuss several topics in extensive-form games. First, we consider perfect information games with belief revision with players who are tolerant of each other’s “hypothetical” errors. Second, we study imperfect information games with players who have no way of assigning probabilities to various possible outcomes, and we analyze how players might choose in such games. We then look into how a truthful manipulator whose motives are not known to players can create a certain knowledge situation about a game, and change the way the game will be played.
We suggest an epistemic logic analysis of strategic games with ordinal payoffs, including Nash’s justification of the equilibrium solution concept: the solution is derived by the players from the game description. We show that most of the classes of games do not have Nash solutions, and for those that have, stronger solution concepts (e.g, domination) and/or refinements of Aumann rationality are needed.
In this talk I will present a theorem justifying an intuitive semantical interpretation of rules of sequent proof systems. This theorem is based on the one hand on a generalization of Lindenbuam maximalization theorem and on the other hand on a general semantical theory of bivaluations, not necessarily truth-functional, originally developed by Newton da Costa for paraconsistent systems. I will show that this theorem gives a better understanding of sequent calculus and that it can fruitfully be applied to a wide class of logical systems providing instantaneous completeness results. This is a typical example of work in the line of the universal logic project, of which I will say a few words.
Reference: Logica Universalis, Special Double Issue – Scope of Logic Theorems. Volume 8, Issue 3-4, December 2014.
Gentzen introduced cut-free proofs in 1934. In these, all formulas are subformulas of what is being proved (and with the same polarity). This is an important feature for many reasons, proof search among them. In 1957 Ohnishi and Matsumoto extended Gentzen’s ideas to several modal logics. Beth introduced tableaus in the 1950’s, with their modern version coming from Smullyan in the 1960’s. Roughly, tableaus are sequent calculi upside-down. I (probably) introduced tableau versions of Ohnishi and Matsumoto’s calculi in the 1970’s. All this treated a small number of modal logics.
Based on an idea of Fitch, I introduced prefixed tableaus in 1972. These add new machinery, but are able to handle many more modal logics. Today they are rather common in automated theorem proving.
In a recent (yet unpublished) paper I introduced set prefixed tableaus. We now have machinery that can handle an infinite family of modal logics, including all the most common ones. And they do this in a uniform way, separating logical rules from so-called structural rules.
The idea that tableaus and sequent calculi are dual to each other continues. Nested sequents have been much studied. In a paper from 2012 I showed that nested sequents and prefixed tableaus were dual, in this sense. And I have a new construct, indexed nested sequents, which is dual to set prefixed tableaus. The pattern continues.
I will cover as much of this as time permits. (My talk is intended to be a trial run for a talk to be given at UNILOG, In Istanbul, this summer.)
We provide a lower complexity bound for the satisfiability problem of a multi-agent justification logic, establishing that there are certain NEXP-complete multi-agent justification logics with interactions. We then use a simple modification of the corresponding reduction to prove that satisfiability for all multi-agent justification logics in a general class we consider is $Sigma_2^p$-hard — given certain reasonable conditions. Our methods improve on these required conditions for the same lower bound for the single-agent justification logics, proven by Buss and Kuznets in 2009, thus answering one of their open questions.
Link to paper on arXiv:
In this talk we discuss truth preserving bi-simulations of multi-agent Kripke models. As an application, we present a semantic proof of the completeness of the syntactic formulation of Muddy Children Puzzle with respect to its standard model.
A mixture of propositional dynamic logic and epistemic logic that we call PDL + E is used to give a formalization of Artemov’s knowledge based reasoning approach to game theory. Epistemic states of players are represented explicitly and reasoned about formally. We give a detailed analysis of the Centipede game using both syntactic proofs and semantical arguments. Formal proofs are used establish what is the case and what is needed to show this. Semantical machinery is used to establish what cannot be the case. All this makes a case that PDL + E can be a useful basis for the logical investigation of game theory.
In this talk we consider knowledge structures used to model epistemic components of extensive-form games. We show that the traditional semantic mode of specification by a single model cannot capture some natural epistemic notions, e.g., mutual knowledge of rationality, used in Epistemic Game Theory. In contrast, Syntactic Epistemic Logic handles this and many other conditions that lie outside the scope of the semantic tradition. We outline general principles of Syntactic Epistemic Logic in connection to Game Theory.
We discuss the Muddy Children puzzle MC, identify and fix the gap in its solution: a completeness analysis is required if the problem is specified syntactically, but analyzed by reasoning on a specific model. We show that the syntactic description of MC is complete w.r.t. its model used in the standard solution. We will present two proofs of completeness: syntactic, by induction on a formulas, and semantic, which makes use of bounded morphisms, a special case of bisimulations. We then present a modification of MC, MClite, and show that it is not deductively complete, has no semantic characterization and cannot be handled by traditional semantic methods. We give a syntactic solution of MClite.
Time permitting, we will venture further into extensive games and their epistemic models
The Syntactic Epistemic Logic, SEL, suggests making the syntactic formalization of an epistemic scenario its formal specification. Since SEL accommodates constructive model reasoning, we speak about extending the scope of formal epistemology. SEL offers a cure for two principal weaknesses of the traditional semantic approach.
1. The traditional semantic approach in epistemology covers only deductively complete scenarios in which all epistemic assertions of any depth are specified. However, intuitively, “most” of epistemic scenarios are not complete. SEL suggests a way to handle incomplete scenarios with reasonable syntactic descriptions.
2. In addition, SEL seals the conceptual and technical gap, identified by R. Aumann, between the syntactic character of game descriptions and the semantic method of analyzing games.
Among the different propositional justification logics, JT45 is the justification counterpart of the modal logic S5. Although there is a growing literature about propositional justification logic, there are only a few papers about the first-order version of justification logic. And most of those papers focus on the first-order version of LP. The goal of this talk is to present a first approach to first-order JT45 (FOJT45). Using Fitting models we will present a possible worlds semantics for FOJT45 and with that establish a Completeness Theorem. We will also discuss some topics related to first-order modal logic such as the Barcan Formula and the failure of the Interpolation Theorem.
The received notion of axiomatic theory, which stems from Hilbert, is that of set T of propositions (either contentful or non-interpreted aka propositional forms) with subset A of axioms provided with a notion of consequence, which generates T from A in the obvious way. I argue that this standard notion is too narrow for being an adequate theoretical model of many mathematical theories; the class of such counter-examples is apparently very large and it includes such different theories as the geometrical theory of Euclid’s Elements, Book 1, and the more recent Homotopy type theory. In order to fix this problem I introduce a more general notion of theory, which uses typing and a generalized notion of consequence applicable also to objects of other types than propositions. I call such a theory constructive axiomatic theory and show that this particular conception of being constructive indeed captures many important ideas concerning the mathematical constructivity found in the earlier literature from Hilbert to Kolmogorov to Martin-Lof. Finally I provide an epistemological argument intended to show that the notion of constructive axiomatic theory is more apt to be useful in natural sciences and other empirical contexts than the standard notion. Disclaimer: The notion of constructive axiomatic theory is not my invention. The idea and its technical implementation are found in Martin-Lof ‘s constructive type theory if not already in Euclid. My aim is to make this notion explicit and introduce it into the continuing discussions on axiomatic method and mathematical and logical constructivity.
We argue that the traditional way to specify an epistemic situation via a single model is unnecessarily restrictive: there are numerous scenarios which do not have conventional single-model characterizations: less-than-common knowledge (e.g., mutual knowledge), partial, asymmetric knowledge, etc. Syntactic Epistemic Logic, SEL, suggests a way out of this predicament by viewing an epistemic scenario as specified syntactically by a set of formulas which corresponds to the characterization via a class of models rather than a single model. In addition, in Game Theory, SEL helps to seal the conceptual and technical gap, identified by R.Aumann, between the syntactic character of game descriptions and the predominantly semantical way of analyzing games.
This will be the first in the series of talks on SEL. We will consider natural examples of epistemic or game theoretic scenarios which have manageable syntactic description but do not have acceptable single model characterizations.
Solutions to the paradoxes of semantic self-reference which endorse the unrestricted T-schema (and cognate principles) normally assume that the conditional involved in the schema is a detachable one (i.e., one that satisfies modus ponens). In a paraconsistent setting, there is another possibility: to take it to be the material conditional. In this talk, I will discuss some of the ramifications of this possibility.
Paraconsistent justification logics are justification logic systems for inconsistent beliefs or commitments. In other words, these systems are intended to model the agent’s justification structure, when she has inconsistent beliefs or commitments.
Realization theorem is one important meta-theorem in the discourse of justification logic. Quasi-realization theorem can be taken to be a major step toward proving realization theorem. In the last semester, I introduced one paraconsistent justification logic, called PJ_b. The main focus of the talk on the coming Tuesday is quasi-realization. It will be proved that quasi-realization theorem – which holds for standard justification logic systems – also holds for PJ_b.