Spring 2008
Seminar in Computational Logic
Tuesday, 2:00pm – 4:00pm, room 3212 (Graduate Center)
October 26 meeting
Speaker: ROMAN KUZNETS, CUNY Graduate Center
Topic: COMPLEXITY ISSUES IN JUSTIFICATION LOGIC (Ph.D. Defense)
Justification Logic is a relatively new field that purports to study provability, knowledge, and belief via explicit proofs or justifications that are part of the language. Many justification logics were developed that closely resemble modal epistemic logics of knowledge and belief with one important difference: instead of modality box with existential epistemic reading ‘there exists a proof of F’ justification logics operate with constructs t :F, where a justification term t represents a blueprint of a Hilbert-style proof of F. The first justification logic, LP, was introduced in by Sergei Artemov. It was shown to be a justification counterpart of modal logic S4 and served as a missing link between S4 and Peano arithmetic, thereby solving a long-standing problem of arithmetic semantics for S4. The machinery of explicit justifications can be used, for example, to analyze a well-known epistemic paradox such as Gettier’s examples of justified true belief that can hardly be considered knowledge. Explicit justification terms can be combined with the traditional epistemic modality providing for a more nuanced structure of knowledge. The use of explicit justifications also suggests a new approach to the concept of common knowledge. The language of explicit justification allowed to study self-referential properties of modal logics through their justification counterparts. These results will be discussed in detail in this thesis. Yet another possible application of the justification logic language is the Logical Omniscience Problem. Logical omniscience is an undesirable property of knowledge as described by modality, when an agent knows all the logical consequences of his/her knowledge. The language of justification logic opens new ways to tackle this problem. This thesis is focused on quantitative analysis of justification and EBK (Evidence-Based Knowledge) logics. We will explore their decidability and complexity of validity problem for them. A closer analysis of the realization phenomenon in general and the specific procedure in particular will enable us to deduce interesting corollaries about self-referentiality in various modal logics. In particular, a framework for proving decidability of various justification and EBK logics is developed by generalizing the Finite Model Property. Limitations of the method are demonstrated by presenting an example of a simple justification logic that is undecidable. Reflected fragments of justification and EBK logics are studied; they are provided with an axiomatization and a decision procedure whose complexity (the upper bound) turns out to be uniform for all justification and EBK logics. Lower and upper bounds are found also for many justification and EBK logics.
October 19 meeting
Speaker: Ren-June Wang, CUNY Graduate Center
Topic: On Proof Realization
S4 is taken as a logic of provability by Gödel, and in it \Box A is interpreted as that A is provable. This motivated Artemov presenting the Logic of Proof, LP, as its explicit proof counterpart, where formula like t:A is introduced with its intending meaning that g is a proof of A. Realization is the process turning each S4 formula into a LP formula by replacing provability modals with symbolism representing proofs in LP. One of the fundamental theorems concerning LP is the Realization Theorem, which states that every theorem of S4 can be realized into a theorem of LP.
This paper tries to realize proofs, not theorems, and it shows that not every proof in S4 can be realized. Only those proofs called non-circular are realizable. Here the definition of non-circularity and an algorithm realizing non-circular S4 proofs into LP proofs will be given. And then we prove that every theorem of S4 has a non-circular proof. These in turn will give us an efficient algorithm for realization S4 theorems.
October 2 meeting
Speaker: S. Artemov, CUNY Graduate Center
Topic: What operations of Brouwer-Heyting-Kolmogorov proofs are appropriate.
In the beginning of the past century, Brouwer, Heyting, and Kolmogorov introduced informally a new, constructive semantics for logical languages where the truth value of a formula is determined by proofs and operations on then. This BHK semantics became a base for many further developments in Computer Science and Mathematical Logic: constructive realizability semantics for intuitionistic theories, lambda-calculi and Curry-Howard isomorphism, typed theories and their applications in programming languages, justification logic and evidence-based epistemic semantics, etc.
In this talk we assume the Logic of Proofs LP to be a formal model for BHK-semantics and analyze what operations on proofs are appropriate there. We show that the original set of operations in LP: application, sum, and proof checker, determine all invariant operations on proofs, which can be specified by a propositional condition. We will also show natural ways to impose an additional structure on LP terms, hence BHK-proofs.
January 29 meeting
Speaker: J. R. Moschovakis, Occidental College (emerita) and MPLA
Topic: Varieties of Reverse Constructive Mathematics
Each of the three main schools of constructive mathematics (Brouwer’s intuitionism INT, Markov’s recursive mathematics RUSS, and Bishop’s cautious constructivism BISH) accepts intuitionistic (Heyting) arithmetic HA as evident, then uses intuitionistic logic to study a more or less restricted class of number-theoretic functions, arriving at a distinct theory of real number generators or “constructive analysis.” RUSS studies recursive sequences, accepting Markov’s Principle and a form of Church’s Thesis contradicting classical arithmetic PA. INT accepts countable choice, effective bar induction, and a nonclassical principle of continuous choice. BISH lies in the intersection of RUSS, INT and CLASS (classical analysis).
Although Brouwer and Bishop worked informally, in order to compare the three approaches — to study what can and what can’t be proved in each, and how much of CLASS can consistently be represented without losing the constructive viewpoint — a formal treatment is useful. HA is like PA but with intuitionistic logic. Kleene and Vesley [1965] formalized INT; BISH can be represented up to a point within INT by reinterpreting the sequence variables and trimming the axioms; Troelstra and van Dalen [1988] formalized RUSS as a nonclassical extension of HA. Each of these formal theories satisfies Markov’s Rule and the Church-Kleene Rule: “Only recursive function(al)s can be proved to exist.”
BISH and INT are now being studied from the reverse mathematics viewpoint, as RUSS has been in the past. We give sample results of each of these programs, then discuss Markov’s Principle and other classically correct axioms which preserve Brouwer’s Rule: “Only continuous functionals can be proved to exist.”