SPRING 2005
CSc 85200.
Seminar in Computational Logic
Code: 66368
Tuesday, 2pm – 4pm, room 3306 (Graduate Center)
April 12 meeting
Speaker: Melvin Fitting
Topic: A Quantified Logic of Evidence
This is yet another paper in the cluster centered on LP. There are two new features introduced in this paper that, I think, will be of interest and use
April 12 meeting
Speaker: Melvin Fitting
Topic: A Quantified Logic of Evidence
This is yet another paper in the cluster centered on LP. There are two new features introduced in this paper that, I think, will be of interest and use.
The first new item is the introduction of quantification into LP, where quantifiers range over proofs. The resulting logic is called QLP, and it has the following satisfying features.
1. It is a conservative extension of LP.
2. S4 embeds into it, translating the necessity operator as an existential quantifier.
One of the axioms for QLP iscalled a uniform Barcan formula. It has relationships with the usual Barcan formula, but the later can be seen as akin to an omega-rule of proof in arithmetic, while the uniform version is more closely related to the way we actually establish universally quantified sentences. I don’t think I fully understand the uniform Barcan formula more work is needed here.
The second new feature is a more general version of what A calls F semantics. As originally presented, F semantics for LP had a strong syntactic flavor — the evidence function mapped proof polynomials and worlds to sets of formulas. In the new version, each model has an abstract domain of things called reasons, an evidence function is defined on these rather than on proof polynomials, and separately, there is a mapping from proof polynomials to reasons, though not necessarily to all of them. Thus the domain of reasons is rather like the domain of a first-order model; its members can be named using terms of the language, but there may be members who lack names. This extra machinery makes the semantics more flexible, and also (I believe) more natural. It can be introduced for LP itself, and not just for QLP, and I hope people will give it due consideration.
April 5 meeting
Speaker: Bryan Renne
Bryan Renne will speak on updates in the logic of knowledge.
March 29: no meeting
March 22: no meeting
March 15 meeting
Speaker: Robert Milnikel (Kenyon College)
Title: “Deducibility in Certain Explicit Modal Logics is Пp2-complete”.
Abstract for people who are knowledgable about LP:
In 2000, R. Kuznets presented a 
p2 algorithm for satistfiability in the Logic of Proofs and several subsystems. This talk presents a proof that the dual problem of deducibility is Пp2-complete for the subsystems LP(K) and LP(K4) as well as for full LP under strong assumptions about the constant specification.
Abstract for people who don’t know anything about LP:
Explicit modal logic realizes the modalities from traditional modal logics with proof polynomials, so an expression []F becomes t:F where t is a proof polynomial representing a proof of or evidence for F. The pioneering work on explicating the modal logic $\mathcal{S}4$ is due to S. Artemov and was extended to several subsystems by V. Brezhnev. In 2000, R. Kuznets presented a p2 algorithm for satisfiability in these logics; this talk presents a proof that the dual problem of deducibility is under many circumstances Пp2-complete. (The analogous problem for traditional modal logics is PSPACE-complete.)
March 8 meeting
Speaker: Sergei Artemov
Title: “Evidence-based knowledge II”
We will describe the basics of a new approach to common knowledge logic systems. This approach leads to lighter and much flexible logic systems with better complexity bounds and proof theoretical behavior.
We will consider multi-agent systems with evidence-based common knowledge TnLP, S4nLP, and S5nLP. Those are multi-agent modal logics Tn, S4n, S5n, with an evidence calculus taken from the Logic of Proofs LP. The above logics will be supplied with epistemic semantics (AF-models), completeness will also be established.
Then we will consider forgetful versions of the above systems, TnJ, S4nJ, S5nJ, when evidence terms are squashed to a special modality J (justified), reminiscent to McCarthy’s `any fool knows’ modality. We establish cut-elimination in TnJ and S4nJ, and then prove that the common knowledge modality J in TnJ and S4nJ can be realized by proof polynomials from TnLP, and S4nLP, respectfully.
We will discuss to what extend evidence-based common knowledge systems could compete with the usual common knowledge systems based on fixed points and induction principles.
We will end by providing a list of important open problems in this area.
Reading (for those who are not familiar with the concept of cut-elimination): A.Troelstra and H.Schwichtenberg. Basic proof theory, Cambridge University Press, 1996, Chapters 3 and 4.
Current problems on evidence-based knowledge systems. Solving any of this problems merits a publication.
1. Consider TnJ, S4nJ and S5nJ– models augmented by the usual common knowledge modality C based on the reachability relation along R1,…,Rn. Call the resulting sets of tautologies in the language with K1,…,Kn,J,C logics TnJC, S4nJC and S5nJC respectively. Find complete axiom systems for TnJC, S4nJC and S5nJC and prove the corresponding completeness theorems. Establish decidability.
2. The same for TnLP, S4nLP and S5nLP with both J and C added.
3. Study TnLP, S4nLP and S5nLP with the weak negative introspection principle -t:F=>[]-t:F. Find models, establish completeness.
4. Answer the question about the Craig interpolation property for TnJ, S4nJ, and S5nJ. Each of T, S4, S5 enjoys interpolation.
5. Analyze the Coordinated Attack problem and Simultaneous Byzantine Agreement problem from the evidence-based point of view in S4nJ and S5nJ.
6. Study the evidence based logics of beliefs. Consider K45 and KD45 as logics for individual agent beliefs. Combine them with LP or “LP minus reflexivity”. Find models, establish completeness.
7. Prove that the satisfiability problems for TnJ, S4nJ and S5nJ are PSPACE-complete.
8. Prove the realization theorem for S5nJ in S5nLP.
9. What kind of interpolation property holds for TnLP, S4nLP and S5nLP? The reading: T.L.Sidon. Craig Interpolation Property for Operational Logics of Proofs (Russian). Vestnik Moskovskogo Universiteta. Ser. 1 Mat., Mech. 1998, no.2 pp.34-38. English translation: Moscow University Mathematics Bulletin, v.53, n.2, pp.37-41, 1999.
March 1 meeting
Speaker: Eric Pacuit
Title: “Classical Systems of First-Order Modal Logic”
This talk will report on a recent paper with Horacio Arlo-Costa.
The paper focuses on extending to the first order case the semantical program for modalities first introduced by Dana Scott and Richard Montague. We focus on the study of neighborhood frames with constant domains and we offer a series of new completeness results for salient classical systems of first order modal logic. In the talk, we will discuss the relevant background on neighborhood systems and first-order modal logic and then discuss completeness results for classical systems of first order modal logic.
We conclude by introducing general first order neighborhood frames (which we call cylindrical general frames) and we offer a general completeness result in terms of them which circumvents some well-known problems of propositional and first order neighborhood semantics (mainly the fact that many classical modal logics are incomplete with respect to an unmodified version of neighborhood frames). We argue that the semantical program that thus arises surpasses both in expressivity and adequacy the standard Kripkean approach, even when it comes to the study of first order normal systems.
February 22 meeting
Speaker: Walter Dean
Title: “Logical omniscience and mathematical omniscience”
This talk is intended to serve both as an overview of the problem of logical omniscience and an introduction to a related topic which I refer to as the problem of mathematical omniscience. The standard analysis of the knowledge modality K in terms of epistemic indiscriminablity of worlds has the following consequences which are each identified as forms of logical omniscience: a) if |= A, then K(A); b) if K(A) and A |= B, then K(B); and c) if |= A <-> B and K(A), then K(B). These are all taken to be negative features of such an analysis since it follows from a) that an agent knows all propositional tautologies, from b) that his knowledge is closed under logical consequence and from c) that it is closed under substitution of logically equivalent formulas.
I will suggest that implicit accounts of knowledge fare even worse as an analyses of mathematical knowledge (i.e. knowledge of mathematical propositions such as 2 + 2 = 4, e(i \pi) = -1 or that there are infinitely many prime). Since mathematical statements are necessarily true (i.e. true in all possible worlds), from a) it follows that agents know all true mathematical propositions (e.g., the Goldbach conjecture, if true), from b) that if an agent knows the axioms of PA, then he knows the prime number theorem and from c) that he knows that f: R -> R is (delta-epsilon) continuous if and only if he knows that for all open X, f-1(X) is open.
I will review several proposals mentioned by Halpern et al. which are intended to avoid the problem of logical omniscience in the light of the problems posed by accounting for mathematical knowledge. One upshot of these considerations is that in order to capture even simple inferences which we expect mathematical reasoners to be able to be draw (e.g. K(2 + 2 = 4) => K(4 = 2 + 2), K(Prime(3)) => K(Prime(2+1)), the objects of mathematical knowledge must be represented using a first-order language. It thus becomes apparent that a potential logic of mathematical knowledge must confront many of the well known problems related to the interpretation for first-order modal logic such as the failure of substitutivity of co-refering terms (e.g. from K(Composite(11 * 13)) and 11 * 13 = 143, it does not follow that K(Composite(143)). Time permitting, I will discuss attempts to resolve this problem based on the notion of algorithmic knowledge as first introduced by Parikh [1987, 1995] and reviewed by Halpern et al. (ch. 10). Relevant background includes Halpern et. al sec. 3.7, ch. 9, ch. 10, Parikh’s “Knowledge and the problem of logical omniscience” and “Logical omniscience” and Stalnaker’s “Logical omniscience I/II.”
February 15 meeting
Speaker: Sergei Artemov
Title: “Evidence-Based Knowledge I”
We will rigorously prove completeness theorems for the basic epistemic logics with justification S4LP ands S4LPN with respect to F-models and AF-models respectively (improved versions of proofs from [5]). We will then introduce a general evidence-based approach to logics of knowledge and beliefs. Specific systems TnLP, S4nLP and S5nLP ([6]) will be considered and compared with the traditional common knowledge systems. We will establish cut-elimination theorem for TnLP, S4nLP.
Homework assignment 3:
1. Read the handout “Basic systems of epistemic logic with justifications”, of February 15. Report all the typos to me.
2. Fitting’s theorem shows that one could trivialize the evidence accessibility relation Re in AF-models by setting Re=R without compromising the completeness property. Show that AF-models with total evidence function (each term is an admissible evidence for any formula) do not provide completeness.
3. Change the monotonicity condition on the evidence function to u Re v => E(u,t) = E(v,t). Is S4LP complete with respect to the new class of S4LP-models?
4. The same question for S4LPN models.
Research Project:
Establish the Finite Model Property of S4LPCS and S4LPNCS. There are two ways of doing it: filtration or via saturation algorithm. The former has not been done yet. The finite countermodels for S4LPNCS were found in [5].
February 8 meeting
Speaker: Sergei Artemov
Title: “Epistemic logic with justification.”
We will systematically cover the Logic of Proofs and its constructive features: internalization, realization of modal logic ([4]); epistemic Fitting-Mkrtychev semantics and completeness ([7]). Time permitting we will also introduce the epistemic logic with justification LPS4 and establish its completeness w.r.t. the FM-semantics ([5]).
Homework assignment 2 (Due February 15):
1. Read the paper “Basic systems of epistemic logic with justifications” by Artemov and Nogina of February 8. Report all the typos to me.
2. Build realizations in LP of the following S4-theorem: []A v []B -> [](A & [](A->B))
3. Prove that LPS4 does not derive the weak negative introspection principle: -x:F -> []-x:F.
Hint: look for an F-countermodel.
4. Prove that LPS4N does not prove x:[]P -> x:P.
Hint: look for an AF-countermodel.
February 1 meeting
Speaker: Sergei Artemov
Title: “Paradigmatic examples and basic principles of reasoning about knowledge.”
Homework assignment 1(Due February 8):
1. Read the book of four FHMV “Reasoning about knowledge”, chapters 1, 2, 3.1-3.3.
2. Prove that S5nC derives all axioms of S5 for C.
3. Prove that McCarthy’s system 4 is equivalent to S4n+1 + (0F->SF).
4. Prove that McCarthy’s system 4 + (F & 0(F->EF) -> 0F) is equivalent to S4nC (with 0 as C).
This semester the seminar will offer an introduction to the logics of knowledge and belief from the mathematical point of view. Reasoning about knowledge can be traced back to the early Greek philosophers. Since the beginning of mathematization in the 1960s it has absorbed a good part of modal logic. Now reasoning about knowledge and beliefs extends to computer science, artificial intelligence, economics, linguistics, and other areas. An emphasis will be made on a new emerging line of research in this area, the evidence-based knowledge.
Seminar references.
Textbooks:
1. R.Fagin, J.Halpern, Y.Moses, M.Vardi. Reasoning About Knowledge. MIT Press, 1995.
3. J.-J.Ch.Meyer, W.van der Hoek. Epistemic Logic for AI and Computer Science. Cambridge University Press, 2004.
Papers:
1. J. McCarthy, M. Sato, T. Hayashi, and S. Igarishi. On the model theory of knowledge, Technical Report STAN-CS-79-725, Stanford University, 1979.
2. J. van Benthem. Reflections on epistemic logic, Logique & Analyse, v.133-134, pp.5-14, 1991.
3. R.Parikh. Logical omniscience. In Logic and Computational Complexity, Ed. Leivant, Springer Lecture Notes in Computer Science No. 960, pp. 22-29, 1995.
4. S.Artemov. Explicit provability and constructive semantics. The Bulletin for Symbolic Logic, v.7, No.1, pp.1-36, 2001.
5. S.Artemov and E.Nogina. Logic of knowledge with justifications from the provability perspective. Technical Report TR-2004011, CUNY Ph.D. Program in Computer Science, 2004.
6. S.Artemov. Evidence-Based Common Knowledge. CUNY Ph.D. Program in Computer Science, Technical Report TR-2004018, 2004.
7. M.Fitting. The logic of proofs, semantically. Annals of Pure and Applied Logic, v.132, Issue 1, pp.1-25, 2005.