The literature on the epistemic foundations of game theory uses a variety of mathematical models to formalize talk about the players' beliefs about the game, beliefs about the rationality of the other players, beliefs about the beliefs of the other players, beliefs about the beliefs about the beliefs of the other players, and so on. A recurring issue involves defining a space of all possible beliefs of the players and whether such a space exists. Studying this issue led Adam Brandenburger and H. J. Keisler to a Russell-style paradox which shows that no such space exists if the players' beliefs (about the other players' beliefs) are assumed to be definable in first-order logic. We will discuss this paradox and related issues.

Review of the book *Reasoning with Arbitrary Objects* by Kit
Fine. The book describes modification of familiar semantics for first
order logic suitable for systems with existential instantiation rule:
From (∃*x*)*A*(*x*)
infer *A*(*b*). The modification looks complicated, but
can be clarified by connecting with Skolem functions and epsilon
symbols. We hope to discuss philosophical implications of this
semantics and its possible connections with other work by Kit
Fine.

Review of the book *Reasoning with Arbitrary Objects* by Kit
Fine. The book describes modification of familiar semantics for first
order logic suitable for systems with existential instantiation rule:
From (∃*x*)*A*(*x*)
infer *A*(*b*). The modification looks complicated, but
can be clarified by connecting with Skolem functions and epsilon
symbols. We hope to discuss philosophical implications of this
semantics and its possible connections with other work by Kit
Fine.

“Small” large cardinal notions in the language of ZFC are those large cardinal notions whose existence is consistent with *V* = *L*. We have the original (1) and analogues (2-7) of small large cardinal notions in:

- Classical set theory
- Admissible set theory
- Admissible recursion theory
- Constructive set theory
- Explicit mathematics
- Constructive type theory
- Recursive ordinal notation systems for proof theory.

The long term aim is to develop a common language for small large cardinal notions to include 1–7. This is a program in progress; at present it is shown how to cover 1–3 in an expansion of the language of set theory to allow us to talk about general set theoretical operations (possibly partial); the large cardinal notions in question are then formulated in terms of operational closure conditions. This is a partial adaptation of Explicit Mathematics notions to the set-theoretical framework. The approach is illustrated for inaccessibles, Mahlo cardinals and weakly compact cardinals. An open problem is to formulate a general reflection principle from which these and other standard “small” large cardinal statements follow.

The concept of a stable model was proposed twenty years ago as a tool for defining a declarative semantics for logic programs with negation. This talk is a survey of recent research on the mathematics of stable models. This work showed, in particular, that stable models are closely related to a much older idea -- to the three-valued superintuitionistic logic, called the logic of here-and-there, which was invented by Heyting in 1930.

Many languages used in computer science (e.g., in knowledge representation, XML querying, system verification) are extensions of modal logic. But what does it mean to be an ‘extension of modal logic’? There are at least three different dimensions along which basic modal logic can be extended:

- Axiomatic extensions (or, restricting the class of structures)
- Language extensions (or, increasing the expressive power)
- Signature extensions (or, changing the type of structures considered)

In this talk I will discuss each of these three dimensions, with a special focus on the second, and I will also discuss some interesting interactions between them. The central question is to what extent we can extend modal logic while preserving its attractive model theoretic and computational properties.

The genesis of the notion of proof in mathematics seems to be lost in the sands of time. We remark on how mathematical proof developed, and what it is today.

Of particular interest is how our idea of proof has changed in the past 50 years. The Appel-Haaken proof of the four color theorem, Hales's proof of the Kepler sphere-packing problem, Perelman's proof of the Poincare conjecture, Thurston's proof of the geometrization program, and many others suggest that our accepted concept of proof continues to evolve. These changes have taken place alongside an increased communication among mathematicians, engineers, physicists, and biomedical researchers. Probably this is not a coincidence, and the causality is worth exploring.

An instance of Stratified Comprehension

∀x_{1}…∀x_{n}∃y∀x(x∈y↔ φ(x,x_{1},…,x_{n}))

is called *strictly impredicative* iff, under minimal
stratification, the type of *x* is 0. Using the technology of
forcing, we prove that the fragment of NF based on strictly
impredicative Stratified Comprehension is consistent. A crucial part
in this proof, namely showing genericity of a certain symmetric
filter, is due to Robert Solovay.

We consider a predicate extension SQHT= of the propositional logic of
here-and-there had been introduced by V. Lifschitz, D. Pearce, and
A. Valverde to characterize the notion of strong equivalence of logic
programs with variables and equality with respect to stable models. It
is determined by intuitionistic Kripke models with two worlds
{*h*,*t*}, where *hRt* and a constant individual
domain. Equality is decidable. Derivable objects of our formulation
are
hypersequents *X*⇒*Y***Z*⇒*U* to
be read: *X*⇒*Y* here or *Z*⇒*U*
there.

The system has familiar axioms, classical Gentzen rules for all
connectives in *Z*⇒*U* and for all connectives
except implication and negation in *Y*. There are special
rules for those two connectives as well as h-t-transfer. Theorem. The
rules are sound and complete.

Existence is definable: ∃*x**P**x* ↔
&forall*y*(∀*x*(*P**x*
→*P**y*)→*P**y*).

*(Abstract TBA)*