A logical formula F(X,P) can be treated as an equation to be
satisfied by the solutions X(P). J. McCarthy considers the parameterization of the models of
formulas, gives the general solution in the case of propositional
logic and states the problem for other logics. We find the general
solution for the formulas in the first-order language with monadic
predicates and equality. The solutions are obtained via quantifier
elimination and parametrized by epsilon terms.
References
On the other hand, I do realize that starting with my real present interests,
without giving necessary background, would not do much good for the
audience. So, I will start with known things, and hope to have a chance to
discuss in some detail my Stanford research plans at some later point. Euler's polyhedron formula asserts for a polyhedron p that
V-E+F=2, where V, E, and F are,
respectively, the numbers of vertices, edges, and faces of p.
The history of Euler's formula is bumpy because it turns out to be
difficult to say just what a polyhedron is, and, even when a
definition is given, it turns out to be difficult to specify the
subclass of polyhedra for which Euler's formula holds. A history of
Euler's formula is given in Imre Lakatos's Proofs and
Refutations [1]. Lakatos's history illustrates a critical process
for improving mathematical knowledge; he calls it the method of proofs
and refutations. The process consists of refining a conjecture (such
as Euler's polyhedron formula) in the light of counterexamples and
incomplete proofs. The goal of the method of proofs and refutations
is to produce a valid proof, which, by definition, has no
counterexamples. Given its rocky history, then, formalizing Euler's formula presents
an interesting challenge for formal proof checking. In this talk I
discuss my recent work on a formalization of (a proof of) Euler's
polyhedron formula. The proof was carried out in the MIZAR [2], which
is a proof checking system based on classical first-order logic and
set theory. I try to disarm Lakatos's antipathy toward formal
mathematics by showing how the process of formalizing a proof mirrors
or exemplifies the method of proofs and refutations. References
Elga (2000) introduced the problem of Sleeping Beauty (SB). A
conceptual paradox for the treatment of diachronic uncertainty in a
Bayesian framework, SB seemed to show that, under certain
circumstances, rationality dictates that one adjust one's probability
assignment when no new information has been introduced. Rather than
address the philosophical literature which followed Elga's paper, I
will investigate the Game Theoretical literature which proceeded it.
In particular, a close investigation of the problem of the Forgetful
Passenger (FP) (Aumann, et al. (1997)) will demonstrate that, contra
Elga's claims: (i) FP is fundamentally different from SB; (ii) the
procedure for dealing with diachronic uncertainties recommended by
Aumann does not give the analysis of SB that Elga claims for it; and
(iii) (under Aumann's proposal) probability assignments do not change
unless information states change. Our discussion will begin by
formalizing an intuitive suggestion in Aumann, et al. We will then
explore the implications of this formalization, in particular its
application for translating games in extended form into Dynamic
Epistemic Logic.
References
Dynamic Topological Logic (DTL) is a tri-modal system for reasoning
about dynamical systems and their short- and long-term behavior. The
intended semantics are defined over dynamical systems, which are
pairs Different logics arise depending on the assumptions we make of the
space X and the function f. Surprisingly, the
computational complexity of these logics may vary wildly as we modify
these assumptions. For example, it has been shown that if we consider
the class of systems where X is arbitrary but f is a
homeomorphism, the resulting DTL is not axiomatizable. It has also
been shown that DTL of continuous functions is undecidable; however, I
will show that this logic is recursively enumerable. Further, I will
discuss minimal spaces, which are dynamical systems where the orbit of
every point is dense; in this setting we get decidability. In this
talk I will compare the three systems, and show what makes them so
different despite their apparent similarities. Category theory deals in a mathematically natural way with certain
kinds of algebraic structures on possibly very large collections of
structures, such as the category Grp of all groups and the
category Top of all topological spaces, in terms of the
structure preserving maps ("morphisms") between such objects. From
this point of view, the category Cat of all categories is
itself such a structure whose morphisms are the so-called functors
between categories. Grp, Top and Cat are
examples of objects in Cat. Even more, if A
and B are two categories, no matter how large, there is a
"still larger" category whose objects are all the functors
from A to B, and whose morphisms are the so-called
natural transformations between functors. Existing set-theoretical
foundations accounts for these kinds of constructions only in terms of
certain kinds of restrictions, e. g. by making a distinction between
"small categories" and "large categories" in a theory of sets and
classes. Nevertheless, it is plausible that the foundation of an
unrestricted category theory can be established without invoking such
distinctions. I shall present several criteria for such a theory and
show how they can be met to a considerable extent in a strong
consistent extension of NFU (Quine's system NF with
urelements). However, a full foundation is blocked in stratified
systems (with or without urelements) as presently treated. The talk
will go over the article, "Enriched stratified systems for the
foundations of category theory" to be found at
http://math.stanford.edu/~feferman/papers/ess.pdf
Solving Logical Equations in Monadic Logic
A Formal Proof of Euler's Polyhedron Formula
The Roots of Sleeping Beauty: A procedure for converting diachronic
uncertainties into synchronic uncertainties
Three Dynamic Topological Logics and their Very Different
Complexities
Will-o'-the-wisp? In Pursuit of a Foundation for Unrestricted
Category Theory