Fall 2012
Seminar in Computational Logic
Tuesday, 2:00pm – 4:00pm, room 3309 (Graduate Center)
December 11 meeting
Speaker: Yuri Gurevich, Microsoft Research
Title: Quantum Computing: The 1st Field Report
Recently this logician became interested in quantum computing, for a number of reasons. What is it all about? Does it influence Church-Turing thesis? Is quantum computing feasible? We present our first field report — with no original contributions — from the journey to the land of QC.
December 4 meeting
Speaker: Konstantinos Pouliasis, CUNY GC
Title: Extending Curry – Howard Isomorphism With Justifications
In this talk we discuss JCalc — a typed lambda calculus in the extension of Curry-Howard isomorphism appropriate for the {->} fragment of Justification Logic. The system axiomatizes a dialogue between two calculi: an intuitionistic and a classical one. The first corresponds to a constructive theory T whereas the second to a classical T’ that is assumed to provide intended semantics for T. Justified necessity will be treated as a proof binding construct between proofs in T and T’. We will mainly focus on the type system of JCalc and then mention some first metatheoretic results as well as possible applications.
November 20 meeting
Speaker: Eva Antonakos, CUNY GC
Title: Explicit Generic Common Knowledge
The name Generic Common Knowledge (GCK) was suggested by Artemov to
capture a state of a multi-agent epistemic system that yields iterated
knowledge I( φ): ‘any agent knows that any agent knows that any agent
knows… φ’ for any number of iterations. In contrast, generic common
knowledge of φ, GCK(φ), yields I(φ),
GCK(φ) → I(φ)
but is not necessarily logically equivalent to I(φ). Modal logics with
GCK were suggested by McCarthy and Artemov. It has been shown that in
the usual epistemic scenarios, GCK can replace the conventional common
knowledge. Artemov noticed that such epistemic actions as public
announcements of atomic sentences, generally speaking, yield GCK rather
than the conventional common knowledge.
In this talk we introduce logics with explicit GCK and show that
they realize corresponding modal systems, i.e., GCK, along with the
individual knowledge modalities, can be always made explicit. As a
representative example of these explicit GCK systems, we assume that all
knowers as well as their GCK system are confined to LP. We call the
resulting system LPn(LP) which symbolically indicates n LP-type agents
with an LP-type common knowledge evidence system. We then show this
corresponds to the modal GCK system S4nJ by offering a realization
theorem. In particular, all epistemic operators in S4nJ, not only J,
become explicit in such a realization.
November 13 meeting
Speaker: Wojtek Moczydlowski, Google
Title: Applied higher infinities in impredicative constructive set theories
The Intuitionistic Zermelo Fraenkel set theory IZF was introduced by Myhill more than 30 years ago, starting investigations into the world of constructive set theories. I will give an overview of this area and describe the recent results that apply inaccessible sets to combine the proof-theoretical benefits of the version with Replacement with the consistency power of the version with Collection. Related open questions will be discussed.
October 23 meeting
Speaker: Cagil Tasdemir, CUNY GC
Title: On tolerance analysis of games with belief revision
Aumann’s Rationality Theorem claims that in perfect information games, common knowledge of rationality yields backward induction (BI). Stalnaker argued that in the belief revision setting, BI did not follow from Aummann’s assumptions. However, as shown by Artemov, if common knowledge of rationality is understood in the robust sense, i.e., if players do not forfeit their knowledge of rationality even hypothetically, then BI follows.
A more realistic epistemic model would bound the number of hypothetical non-rational moves by player i that can be tolerated without revising the belief in i’s rationality on future moves. We show that in the presence of common knowledge of rationality, if n hypothetical non-rational moves by any player are tolerated, then each game of length less than 2n + 3 yields BI, and that this bound on the length of model is tight for each n. In particular, if one error per player is tolerated, i.e., n = 1, then games of length up to 4 are BI games, whereas there is a game of length 5 with a non-BI solution.
October 16 meeting
Speaker: Giorgi Japardize, Villanova
Title: Give Caesar what belongs to Caesar
In this talk I will discuss the possibility and advantages of basing applied theories (e.g. Peano Arithmetic) on Computability Logic instead of the more traditional alternatives, such as Classical or Intuitionistic Logics.
October 9 meeting
Speaker: Eugene Tyrtyshnikov, Russian Academy of Sciences
Title: New tensor decompositions in numerical analysis and data processing
Tensor decompositions such as CANDECOMP/PARAFAC and Tucker’s have been discussed for a long time. However, the main issues were those connected with some algebraic varieties and fast matrix multiplication algorithms, and, sometimes, other issues such as Higher-Order SVD with a link to data processing. We consider some new tensor decompositions such as TT (tensor trains) and HT (Hierarchical Tucker) and the role they are beginning to play in matrix computations and related problems of numerical analysis.
Both TT and HT decompositions are the results of one and same scheme for the reduction of dimensionality. These decompositions are frequently applied to tensors after some, often ultimate, quantization of the original dimensions. This maximizes the number of modes and makes the number of counts at each mode minimal possible, e.g. 2. We consider how multilevel matrices become tensor trains with the use of the Kronecker-product operation.
Then we show how new wavelet transforms arise in the construction of tensor trains when forcing the TT ranks be limited. We also discuss some examples and perspectives for applications.
In the end, we present an ambitious research goal of design of fast tabulation procedures using a new interpolation instrument based a TT generalization of the skeleton (dyadic) decomposition from matrices to tensors.
REFERENCES
[1] I.Oseledets, E. Tyrtyshnikov, TT-cross approximation for multidimensional arrays, Linear Algebra Appl., 432 (2010), pp. 70-88. [2] I. Oseledets, E. Tyrtyshnikov, Algebraic wavelet transform via quantics tensor train decomposition, SIAM J. Sci. Comp., vol. 31, no. 3 (2011), pp. 1315-1328. [3] I. Oseledets, E. Tyrtyshnikov, N. Zamarashkin, Tensor-train ranks for matrices and their inverses, Comput. Meth. Appl. Math., Vol. 11, No. 3 (2011), pp. 375-384.October 2
Speaker: David Ellerman, (University of California, Riverside)
Talk1: Partition logic, logical information theory, and quantum mechanics
When ordinary “propositional” logic is seen, as Boole did, as the logic of subsets (“propositions” being modeled by the special case of subsets of the one-element universe set), then there is a dual form of logic. Partitions (or quotient sets or equivalence relations) are dual to subsets as we see all across algebra in the duality between subobjects and quotient objects (monics versus epis in categorical terms). This three-part talk will first describe the development of partition logic. (paper = Review of Symbolic Logic, June 2010)
Just as Boole’s logic of subsets leads naturally to a theory associating a quantity (finite probability) with each subset (event) of a finite universe, so the logic of partitions leads (by analogous moves) to a theory about a quantity associated with each partition that might be called the “logical entropy” of the partition. This leads to a logical information theory that is more conceptually basic than Shannon’s theory of communication (and its corresponding notion of entropy). The talk will secondly sketch logical information theory. (paper = Synthese, May 2009)
Last but not least, the common sense worldview of entities having a full set of properties (“properties all the way down”) is abstractly modeled by the Boolean logic of subsets. The major problem of interpreting quantum mechanics arises because that common-sense notion of fully-propertied entities does not apply at the quantum level. But how can we conceptalize an alternative view of quantum reality if the common-sense view described by subset logic does not apply?
Answer: use the dual logic, the logic of partitions. We will see how partition logic abstractly captures a dual concept of reality (stated abstractly using sets). We then show how these set concepts can be “lifted” to vector spaces (e.g., like how cardinality of a set lifts to dimension of a vector space), and the result turns out to be the mathematics of quantum mechanics! By showing that QM math is essentially the vector space lifting of partition math, we find corroboration that the alternative vision of reality given by partition logic is, in fact, accurate at the quantum level, and thus we see how to build a micro-realistic interpretation of QM. The third portion of the talk will outline this interpretation of QM arising out of partition logic.
Speaker: Abhishekh Sankaran, IIT Bombay
Talk2: Preservation under Substructures modulo Bounded Cores
We investigate a model-theoretic property that generalizes the classical notion of preservation under substructures. We call this property preservation under substructures modulo bounded cores, and present a syntactic characterization via \Sigma 0_2 sentences for properties of arbitrary structures definable by FO sentences. Towards a sharper characterization, we conjecture that the count of existential quantifiers in the \Sigma 0_2 sentence equals the size of the smallest bounded core. We show that this conjecture holds for special fragments of FO and also over special classes of structures. We present a (not FO-definable) class of finite structures for which the conjecture fails, but for which the classical Lo´s-Tarski preservation theorem holds. As a fallout of our studies, we obtain combinatorial proofs of the Lo´s-Tarski theorem for some of the aforementioned cases.
(Joint paper with Bharat Adsul, Vivek Madan, Pritish Kamath, and Supratik Chakraborty).
September 11 meeting
Speaker: Can Baskent, (IHPST, Université Paris 1 Panthéon-Sorbonne)
Title: Some Logical Approaches to Lakatos’s ‘Proofs and Refutations’
Lakatos’s seminal work ‘Proofs and Refutations’ presents a rational analysis of theorem improvement. The case in question in Proofs and Refutations is a familar one – Euler’s Theorem for polyhedra. In my talk, I will present various approaches to Lakatos’s methodology. First, I will explicate the method of proofs and refutations. Then, I will present, first a dialethetic approach, second an interrogative approach, and time permitting, a computational approach. Finally, I will conclude with some remarks.
September 4 meeting
Speaker: Tudor Protopopescu (Graduate Center)
Title: Discovering Knowability: A Semantic Analysis (a joint work with S. Artemov, just appeared in Synthese)
We provide a semantic analysis of the well-known knowability paradox stemming from the Church-Fitch observation that the meaningful knowability principle all truths are knowable, when expressed as a bi-modal principle
F -> <>KF,
yields an unacceptable omniscience property all truths are known. We offer an alternative semantic proof of this fact independent of the Church-Fitch argument. This shows that the knowability paradox is not intrinsically related to the Church-Fitch proof, nor to the Moore sentence upon which it relies, but rather to the knowability principle itself. Further, we show that, from a verifiability perspective, the knowability principle fails in the classical logic setting because it is missing the explicit incorporation of a hidden assumption of stability: `the proposition in question does not change from true to false in the process of discovery.’ Once stability is taken into account, the resulting stable knowability principle and its nuanced versions more accurately represent verification-based knowability and do not yield omniscience.
August 28 meeting
Speaker: Sergei Artemov (Graduate Center)
Title: Generic Common Knowledge
In four points of origin, each coming from a different body of motivations:
David Lewis in “Convention,” 1969;
John McCarthy in “On the model theory of knowledge,” 1970-78;
Robert Aumann in “Agreeing to Disagree,” 1976;
S.A. in “Justified Common Knowledge,” 2006.
the common knowledge operator C(F) was intended to capture the iterative knowledge “A knows that B knows that A knows … F” which, in the classical environment, is informally represented by the “infinite conjunction” I(F) F & E(F) & E^2(F) & E^3(F) & … & E^n(F) & … Here E^n(X) is the n-th iteration of the statement “every agent knows X.”
Despite differences in modes of presentation these approaches all agree that C(F) => I(F), (*)
thus postulating that “common knowledge” yields iterative knowledge. However, there is no consensus concerning a stronger assumption that common knowledge should be equivalent to iterative knowledge:
C(F) <=> I(F), (**)
Moreover, Lewis, McCarthy, and Artemov define C(F) as (*) whereas Aumann opted for (**), which subsequently became a dominant model for common knowledge, in particular, in Game Theory.
We suggest calling C(F) satisfying (*) Generic Common Knowledge, GCK. Note that whereas the standard common knowledge for a given Kripke model M is unique and determined by the reachability in M, there might be many logically non-equivalent GCK operators. In particular, the Universal Knowledge of F, U(F), meaning that F holds at all nodes, is an instance of GCK.
We argue that using GCK instead of common knowledge can be beneficiary in some meaningful situations. Public announcements of non-epistemic facts, the standard vehicle of obtaining common knowledge, actually yield GCK (in particular, Universal Knowledge) rather than common knowledge. In games of perfect information in belief revision setting, the standard `common knowledge of rationality’ assumption does not guarantee that `there is no irrationality in the system’ and hence should be replaced by some instance of GCK.