Spring 2011
Seminar in Computational Logic
Tuesday, 2:00pm – 4:00pm, room 3309 (Graduate Center)
May 17 meeting
Speaker: Roman Kuznets (University of Bern),
Title: Constructive Realization of Justi cation Logics via Nested Sequents
Abstract:
Justification counterparts for most modal logics in the so-called “modal cube” are known. However, until recently there was no uniform method of proving the Realization Theorem for all of them. We present such a method for all the normal modal logics formed from the axioms d, t, b, 4, and 5. The main tools used are cut-free nested sequent calculi a la Kai Brünnler and Melvin Fitting’s realization merging technique.
Based on our realization method, we discuss the question of modularity of realizations: each modal axiom has a natural justification counterpart. However, one modal logic may have several axiomatizations, accordingly it is natural to suggest there to be several natural justification counterparts, one for each axiomatization. Our goal is to completely classify these various realizations by introducing a natural equivalence relation on them that extends that of Fitting. The naturality of the equivalence relation here means that justification logics are equivalent iff they have the same forgetful projection.
This is a joint work with Kai Brünnler and Remo Goetschi (both from University of Bern).
April 12 meeting
Speaker: Giuseppe Primiero (Ghent University),
Title: A Type System with Modalities II: Procedural Semantics.
Abstract:
This talk will complete our presentation of a contextual modal type system for safe distributed computing. In this second presentation, I will start from briefly introducing the standard way to give a BHK-semantics for typed expressions. Then I will focus on the justification and the design of a procedural semantics for our system. Provided a functional typed term in our formal language can be interpreted as a (distributed) program in the form of a sequence of computational steps at various locations, the semantics consists in defining the allowed computational steps to change the configuration of an abstract machine from state to state and the specification of the locations valid for the next machine state. I will define a machine state, the typing rules for such states and the model in which reduction steps are performed. The main results for our calculus can be obtained via this semantics: Preservation (well-formedness of the rules), Progress (all states are value states) and Type Safety (termination).
April 5 meeting
Speaker: Giuseppe Primiero (Ghent University),
Title: A type system with modalities for safe distributed computing
Abstract:
Modal Logics have been largely used for epistemic purposes and the modeling of collective rationality in the form of Distributed and Common Knowledge is one of their most important tasks. In their increasing role as foundation of programming languages semantics, modalities have been applied as well to the design of distributed, staged and mobile computing. The analogies between the two applications are extensive and run deep. In this talk, I will start from mentioning a small non-exhaustive portion of modal calculi and then move to my main task: the introduction of a modal polymorphic typed system, whose basic idea is to distinguish computations valid everywhere (safe values) from locally bounded code. The result is a multi-modal type system, where modal formulas are induced from an appropriate interpretation of type constructors and with an appropriately defined derivability relation. The language simulates safe distributed programming using the bridging rules for its modal operators to define code mobility; the rules for the boxed formulas mimic axioms of a multi-modal S4. I will conclude by mentioning an embedding of Definitions for Common and Distributed Knowledge in this typed language.
March 29 meeting
Speaker: Nick Bezhanishvili (Imperial College London),
Title: Admissible fixed point logics
Abstract:
Modal fixed point logic is an extension of modal logic with a least and greatest fixed point operators. It is decidable, with reasonable complexity, yet very expressive: many widely used modal and temporal logics embed in it as fragments. These features make modal fixed point logic one of the best suited logics for computer science applications. However, the issue of completeness for fixed point logic for the standard Kripke semantics turned out to be very problematic. In this talk, I will illustrate how to remedy this problem using the semantics of admissible assignments. I will present a fixed point analogue of Sahlqvist’s well-known result and discuss the potential of admissible semantics as an alternative foundation for modal fixed point logic.
This is joint work with Ian Hodkinson.
March 22 meeting
Speaker: Yuri Gurevich (Microsoft Research),
Title: Infon Logic
Abstract:
Infons are declarative sentences viewed as pieces of information. We don’t ask whether a given infon is true or false; it may be neither. A better question is who knows that infon. We developed infon logic in connection with the cloud security problem. The connection will be explained this coming Thursday at the CUNY Computer Science Colloquium. This lecture is devoted to the logic if infons. In particular we will present so-called primal infon logic, very efficient and yet sufficiently expressive for many authorization purposes. The derivation problem for primal infon logic is solvable in linear time.
In this paper, we will discuss such a reformulation of the language of basic modal logic with some further advancement and applications. Our focus will be the nabla modality which was introduced by Larry Moss for coalgebraic purposes. Our goal here is to present as several results on nabla modality spanning various fields in epistemic logic.
March 15 meeting
Speaker: Can Baskent (CUNY Graduate Center),
Title: Some Observations on Nabla Modality
Abstract:
The traditional necessity and possibility operators of modal logic provide us with a direct insight about how modalities work in various frameworks. Especially, supported with simple-to-use Kripke semantics and its intuitive proof theory, such modalities have led to a variety of mathematical and philosophical developments in the ï¬eld. Nevertheless, from a mathematical point of view, one can put these two modalities together in a certain way to create a single modal operator, and obtain an equi-expressible language as the standard propositional modal logic.
In this paper, we will discuss such a reformulation of the language of basic modal logic with some further advancement and applications. Our focus will be the nabla modality which was introduced by Larry Moss for coalgebraic purposes. Our goal here is to present as several results on nabla modality spanning various fields in epistemic logic.
March 8 meeting
Speaker: Hsing-chien Tsai (National Chung Cheng University, Taiwan),
Title: On the Decidability of Mereological Theories up to the Theory of Boolean Algebra
Abstract:
A mereological theory is formed with axioms based on a binary relation “being a part of”; hence the formal language of such a theory will have only one non-logical symbol, a binary predicate P, which stands for the aforementioned relation. It is known that the origin of this kind of theory is due to Lesniewski. However, recently there have been other authors, such as Simons or Casati and Varzi , who have tried to reformulate mereological axioms using the formal language with which most logicians nowadays are familiar. I shall follow the recent formulation when making my inquiries.
Most philosophers believe that P must at least define a partial ordering, that is, it is reflexive, antisymmetric and transitive. Thus we have the following three basic axioms.
(P1) ∃Pxx
(P2) ∃x∃y((Pxy∧Pyx)→x=y)
(P3) ∃x∃y∃z((Pxy ∧Pyz)→ Pxz)
Let’s define three additional predicates as follows.
Proper Part: PPxy =df Pxy ∧x≠y
Overlap: Oxy =df ∃z(Pzx∧Pzy)
Underlap: Uxy =df ∃z(Pxz∧Pyz)
In the literature, there are some other mereological axioms which are arguably still philosophically motivated, such as extensionality principle (EP), weak supplementation principle (WSP), strong supplementation principle (SSP), finite sum (FS), finite product (FP), complementation (C) and the existence of the greatest member (G).
(EP) ∀x∀y(∀zPPzx↔(∀z(PPzx↔PPzy)↔x=y))
(WSP) ∀x∀y(PPxy↔∀z(PPzy∧¬Ozx))
(SSP) ∀x∀y(¬Pyx↔∃z(Pzy∧¬Ozx))
(FS) ∀x∀y(Uxy↔∃z∀w(Owz≡(Owx∨Owy)))
(FP) ∀x∀y(Oxy↔&existz∀w(Pwz≡(Pwx∧Pwy)))
(C) ∀x(¬∀zPzx↔∃z∀w(Pwz≡¬Owx))
(G) ∃x∀yPyx Now it turns out that any theory which can be formed by using the foregoing axioms is in a sense a subtheory of the theory of Boolean algebra. As a matter of fact, most of the mereological theories which can be found in the literature range from the theory of partial ordering to the theory of Boolean algebra. It is known that the theory of partial ordering is undecidable while the theory of Boolean algebra is decidable. It is interesting to look into the behaviors in terms of decidability of those mereological theories located in between. I will give results concerning these theories and from there we can see that any mereological theory (within the aforementioned range) cannot be decidable if it does not have the complementation axiom.
March 1 meeting
Speaker: Melvin Fitting (Graduate Center, CUNY),
Title: Nested Sequents and Prefixed Tableaus are Dual
Abstract:
People, especially those at CUNY, know that tableaus and sequent calculi are dual notions. A proof using one methodology is a proof in the other, “upside-down.” In the 1970’s I introduced so-called prefixed tableaus, which supply proof procedures for several modal logics that don’t have tableau systems in the conventional sense. Prefixed tableaus involve extra machinery, and it has been a nagging question what a sequent counterpart might be. Recently Kai Brunnler has been investigating something called nested sequent calculi. In these, reasoning is not just at the top level, but can occur deep inside a formula. It turns out these are what was wanted all along. The fit between prefixed tableaus and nested sequents is simple, and similar to that between ordinary tableaus and sequent calculi. Since prefixed tableaus have been around for some time, we can use the connection to create a number of interesting nested sequent proof systems. I will present the background, as well as recent work. In addition to modal systems, I will also discuss an interesting nested sequent system for constant domain intuitionistic propositional logic.
February 22 meeting
Speaker: Sergei Artemov (Graduate Center, CUNY),
Tatiana Yavorskaya (Moscow University),
Title: First-Order Logic of Proofs and Brouwer-Heyting-Kolmogorov Semantics
Abstract:
We offer an arithmetically sound first-order logic of proofs FOLP which has enough expressive power to realize the first-order modal logic S4 and therefore first-order intuitionistic logic HPC. This provides FOS4 with an exact provability semantics and formalizes the Brouwer-Heyting-Kolmogorov semantics of proofs for the first-order intuitionistic logic.
February 15 meeting
Speaker: Evan Goris (Graduate Center, CUNY),
Title: Strand Space Techniques for the Inductive Method II
Abstract:
Last talk I discussed an implementation in Isabelle of the bound on the penetrator from Guttman’s Strand Space model translated to Paulson’s model. This talk I will show how the theory on the penetrator can be extended to a theory on the regular events of a protocol and use it to show the correctness of the NSL Protocol. The method seems very general and I expect it to be applicable to other protocols too and for a very large part automatable. In any case the current state is an improvement of the Strand Space proof where the penetrator theory alone did not seem to work very well with public key protocols like NSL and one has to either construct a proof ad hoc or use more advanced techniques.
February 1 meeting
Speaker: Sergei Artemov (Graduate Center, CUNY),
Title: The ontology of justifications in the logical setting
Abstract:
Justification Logic provides an axiomatic description of justifications within the logical context and delegates the question about the nature of justifications to semantics. In this talk, we address the conceptual question of the logical type of justifications: we stipulate that justifications are abstract objects interpreted as sets of formulas with specific operations. We argue that this provides the proper understanding of justifications and leads to leaner models for the basic systems of Justification Logic. We recast the Mkrtychev and Fitting semantics accordingly and show that evaluations of justifications as sets of formulas cannot be given inductively.