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.''
