May 16 meeting
Speaker:
HIDENORI KUROKAWA (Graduate Center)
Topic:
Combining Classical and Constructive Logic
In this talk we first present some new results
concerning intuitionistic logic with classical
atoms (IPCca): Craig interpolation theorem,
arithmetical completeness, modal counterparts of
IPCca, etc. Then, we compare IPCca with other
known approaches to combining classical and
constructive logic.
May 9 meeting
Speaker:
Yegor Bryukhov (CCNY)
Topic:
Matrix-based proof method, part 2.
In this second part of the talk we will try to use
an implementation of matrix-based prover in
MetaPRL for S4nJ. We'll try to prove some facts,
talk about its performance and the ways of
controlling the search space manually. Time
permitting, I'll mention the recent paper of Jens
Otten "Clausal Connection-Based Theorem Proving in
Intuitionisitc First-Order Logic", how he performs
a dynamic increase of multiplicity and how it can
be added to the existing prover in MetaPRL.
May 2 meeting
Speaker:
Bryan Renne (Graduate Center)
Topic:
Propositional games and explicit strategies
We present a game semantics for the Logic of
Proofs, where terms are interpreted as specific
strategies on the subformula-choosing evaluation
games familiar from propositional (or first-order)
logic. Under this interpretation of terms, the LP
term operations act as specific operations on
strategies. We will close with a discussion of
potential interaction with other logic games.
April 25 meeting
There will be 20 min presentations of the members of the Research Laboratory for Logic and Computation (RLLC)
- Yegor Bryukhov. Incorporating decision procedures into proof assistants.
- Bryan Renne. Justifications in formal epistemology.
- Roman Kuznets. Complexity of explicit knowledge.
- Evan Goris. Feasibility of operations on proofs.
- Srikanth Gottipati. Finsler controls.
April 4 meeting
Speaker:
Yegor Bryukhov (CCNY)
Topic:
Matrix-based prover in MetaPRL
We'll talk about a matrix-based prover in MetaPRL logical framework:
- Some theory.
- A brief tutorial on how to use the prover for the logic of justified knowledge S4nJ.
- How to prepare a formula manually to achieve a reasonable performance.
- Directions of possible improvements.
- A recent algorithm enhancement by Otten that gives a huge performance boost to matrix-based provers.
I'll probably need to use two seminars to cover
this material.
March 28 meeting
Speaker:
Evangelia Antonakos (Graduate Center)
Topic:
Justified Knowledge is Usually Sufficient
We will compare the relative strengths
of three notions of public knowledge to try to
address the observation that the light-weight
systems of common knowledge due to McCarthy (`any
fool knows') and Artemov (Justified Knowledge)
suffice to solve standard epistemic puzzles for
which heavier and more problematic solutions based
on Common Knowledge due to Halpern and Moses are
offered by standard textbooks. Specifically, we
show that Common Knowledge systems are
conservative with respect to Justified Knowledge
systems on formulas of the form (d & Ja)-->b where
a,b,d, are C-free and J-free. These formulas seem
to be sufficient to formalize standard epistemic
puzzles.
March 21 meeting
Speaker:
Melvin Fitting (Lehman/Graduate Center)
Topic:
A Replacement Theorem for LP
The replacement theorem for classical and normal modal logics is a
fundamental tool. It says that if A and B have been proved equivalent,
occurrences of A can be replaced by occurrences of B to produce a
formula equivalent to the original one. This theorem does not hold for
LP, Logic of Proofs. A replacement to replacement is not easy to
formulate. In this talk we provide one, along with some machinery for
working with LP realizations that may prove useful for other things as
well.
March 14 meeting
Speaker:
Bryan Renne (Graduate Center)
Topic:
Bisimulation and public announcements in logics of explicit knowledge
We introduce a notion of bisimulation for Fitting models of Artemov's
logics of explicit knowledge. Bisimulation allows us to study the
effect of dynamic epistemic operations on language expressivity. It
will be shown that public announcements, a basic dynamic epistemic
operation, add expressivity to the language of explicit knowledge. It
will also be shown that public announcements are definable in the
language of explicit knowledge augmented with an explicit evidence
accessibility relation.
March 7 meeting
Speaker:
Walter Dean (Graduate Center CUNY)
Topic:
A Fregean logic of mathematical knowledge (Preliminary report)
In this talk I will present a preliminary attempt to provide a
first-order logic of knowledge that is capable of the accommodating
fact that otherwise rational agents may be ignorant of various true
mathematical statements. I will begin by contrasting three ways by
which we might attempt to account for such failures of mathematical
omniscience. These can be illustrated by comparing the sense in which
we are prepared to accept that any of the following statements can be
*false*:
1) i knows that there are infinitely many primes.
2) i knows that Con(PA).
3) i knows that 13! = 6227020800.
The sense in which we allow that 1) can be false can presumably be
accounted for by the fact that i can be mathematically
competent without explicitly knowing a proof of the infinitude of the
primes. Its falsity can therefore be modeled formally by adopting a
logic of explicit evidence terms such as that presented in Artemov and
Nogina [2005]. The sense in which 2) can be false is presumably to be
accounted for in terms of the fact that there are "mathematically
possible worlds" compatible with i's grasp of arithmetic (as given,
e.g., by axioms of PA) in which Con(PA) is false. Such failures of
mathematical omniscience can thus be accounted for in terms of the
familiar Hintikka indistinguishability analysis of the epistemic
modality. I will argue that the sense in which we are prepared to
regard 3) as false cannot be readily assimilated to either of these
approaches. Rather it must be explained in terms of a reading of "i
knows that f(a) = b" approximated by "i can compute that f(a) = b."
I will outline an attempt at developing a formal semantics and proof
theory for this interpretation of the epistemic modality based on a
combination of Fitting's [2004, 2005] First-Order Intensional Logic,
primitive recursive definitions and postive inductive definitions.
February 28 meeting
Speaker:
Roman Kuznets (Graduate Center CUNY)
Topic:
Epistemic Logics with Justification are decidable
Artemov and Nogina recently introduced explicit knowledge
mechanism into several logic of knowledge systems. It was shown that
this explicit knowledge is closely connected with the notion of common
knowledge. Several systems of epistemic logic with explicit
justifications were formulated and given Kripke-style semantics. In this
talk we provide the framework that allows to prove decidability of such
systems. It turns out that the standard Finite Model Property by itself
is not sufficient for proving decidability of these new logics. We show
how to generalize the notion of Finite Model Property to achieve the
desired result.
February 7 meeting
Speaker:
Evan Goris (Graduate Center)
Topic:
Realizability in the logic of proofs and formal provability
We will elaborate on the realization theorem for the logic of proofs
(LP). Roughly this theorem says that the theorems of S4 are exactly the
modal formulas that have explicit counterparts as theorems of LP. The
logic of proofs and formal provability (GLA) has potentially more
strength than LP in this respect: all theorems of S4 do have explicit
counterparts in GLA but there could be more. We will see that this is
not so.
This is all part of work in progress. After a general introduction to LP
and the realization theorem (depending on the audience) we shall present
a proof of the above claim and present two more issues that arise from
the proof for which there are no complete answers yet but are probably
of more interest.
January 31 meeting
Speaker:
Sergei Artemov
Topic:
Computer-Aided Proofs and Their Significance
Computer-assisted proofs are playing an increasingly visible role in
mathematics. Their scope ranges from routine uses of computational
algebra packages to dramatic new discoveries which make newspaper
headlines, such as the four-color problem, Kepler's conjecture, Robbins'
conjecture, etc. Some of these proofs rely heavily upon modules that
compute numerical values or decision procedures which do not produce
formally certifiable proof codes.
Proof assistants have also reached the stage where they can be used for
formalization and certification of real mathematical theorems. Theorems
which have been formally verified in this way include the Jordan curve
theorem, the prime number theorem, the first G\"odel incompleteness
theorem, the aforementioned four-color problem, and other famous
mathematical results.
These developments have become possible due to the gradual improvements
made by computer scientists in the fields of automated deduction and
verification. There are a variety of systems now available ranging from
model checkers and fully automated provers for propositional logic to
sophisticated proof assistants for higher-order theories; the latter
provide user-friendly and theoretically well-founded comprehensive tools
for creating, handling, and using formal proofs. Some of these
techniques have been used successfully in industry for hardware and
software verification. In the formal study of programming languages the
state of the art is almost at the point where mechanized metatheoretical
tools can be used routinely, and an electronic appendix with
machine-checked proofs accompanying papers is fast becoming the norm there.
In this talk we will discuss some methodological and philosophical
questions concerning these developments. To what extent can one trust
computer-generated proofs? Are such proofs more trustworthy than
conventional hand-checked proofs? Can computer proofs be "elegant," or
provide insights about the structure of mathematical objects? Do
incompleteness phenomena extend to the foundations of verification? For
that matter, can a verifier be verified? What kinds of reflection
mechanisms are needed to justify the use of computational and decision
procedures in formal proofs? What else should be done to make proof
assistance more attractive to users?
