Conference in
Honor of Harvey M. Friedman, May 14-17, 2009
List of titles
and abstracts as of May 4, 2009
_______________________________________________________________
Andrew Arana
Department
of Philosophy
Kansas
State University
Title: On Purity of Methods
Abstract: There is a long-standing
tradition in mathematics of preferring the pure to the impure in proofs of
theorems and solutions of problems. ÒPurity'Ó of the relevant type has
generally been taken to signify a preferred relationship between the resources
used to prove a theorem or solve a problem and the resources used or needed to
understand or comprehend it. In this sense, pure proof or solution is that
which uses only means that are in some sense intrinsic to (a proper
understanding of) the theorem proved or problem solved. In this talk we will
aim at clarifying the character and epistemic significance of what we think is
the central conception of purity. We will also consider the question of whether
purity is sometimes impossible, focusing in particular on how Harvey Friedman's
work concerning Boolean Relation Theory bears on this question.
_______________________________________________________________
Sergei Artemov
Graduate
Center
City
University of New York
Title: Mathematical Logic of
Justification
Abstract: Since Plato, the notion of
justification has been an essential component of epistemic studies. However,
until recently, the notion of justification has been conspicuously absent from
mathematical models of knowledge within the epistemic logic framework.
Commencing from seminal works by von Wright and Hintikka,
the notions of Knowledge and Belief have acquired formalization by means of
modal logic with modals ÔF is knownÕ and ÔF is believed.Õ Within this approach,
the following analysis was adopted: For a given agent,
F is known ~ F
holds in all epistemically possible situations.
The
deficiency of this approach is displayed most prominently, in the Logical
Omniscience feature of the modal logic of knowledge.
Justification Logic had been anticipated by Goedel as the logic of explicit
mathematical proofs and has been first developed as the Logic of Proofs. It
introduces a mathematical notion of justification, making epistemic logic more
expressive. We now have the capacity to reason about justifications, simple and
compound. We can compare different pieces of evidence pertaining to the same
fact. We can measure the complexity of justifications, which leads to a
coherent theory of logical omniscience. Justification Logic provides a novel
mechanism of evidence-tracking which seems to be a key ingredient in the
analysis of knowledge. Finally, Justification Logic furnishes a new,
evidence-based foundation for the logic of knowledge, according to which
F is known ~ F
has an adequate justification.
_______________________________________________________________
John Burgess
Department of
Philosophy
Princeton
University
Title: Axiomatic Theories of Truth: What
We Know and What We DonÕt Know
Abstract: Kripke
distinguishes intuitively a pre-reflective from a reflective stage in our
understanding of truth and suggests a model of each. The complexity of the
models is well-understood. Various attempts have been
made to axiomatize the one and the other intuitive
notion. Results of considerable technical interest on the
proof-theoretic strength of such axiomatic theories have been obtained, notably
by Friedman and Sheard, but not a really convincing
argument that any one of the axiomatizations
corresponds to either of the intuitive notions. Obstacles to achieving
this philosophical goal will be described, and a strategy for surmounting some
of them.
_______________________________________________________________
Sam Buss
Department of
Mathematics
University of
California at San Diego
Title: Lengths of proofs and
self-reference
Abstract: We survey results on the lengths of
proofs of partial self-consistency statements for first-order theories of
arithmetic and for much weaker systems.
We also discuss situations when a theory can diagonalize
away from a weaker theory even when it cannot prove the consistency of the
weaker theory.
_______________________________________________________________
Norman Carey and
David Clampitt
CUNY Graduate
Center OSU
School of Music
Title: Foundations of Western Music:
Mathematical Theory of Well-formed Modes
Abstract: At the heart of the western musical tradition lies the diatonic
scale, exemplified by the white keys of the piano, the notes of the familiar
major scale. The use of this pitch collection dates back at least three and a
half millennia, as recorded on Assyrian and Babylonian cuneiform tablets. This
paper accounts for the prominence of the diatonic in terms of its structure as
a well-formed scale, a structure it has in common with the pentatonic scale
(exemplified by the black keys of the piano, a common scale in world music), as
well as with the 12-note chromatic scale, and 17-tone Arabic and 53-tone
Chinese theoretical systems. A scale is understood to be a collection of notes ordered
according to pitch height, repeating periodically at some interval, usually the
octave (corresponding to the frequency ratio 2:1). A scale is well-formed if all of its notes (modulo the octave) may be
derived by a generating interval (usually the perfect fifth, corresponding to
the frequency ratio 3:2), where the generating interval is always spanned by
the same number of scale step intervals (intervals between adjacent notes in
scale order). The musical consequences of this definition are manifold, entailing
limits on the complexity of musical materials and consistency between
descriptions of these materials in terms of the scale itself as an underlying
metric, on one hand, and in terms of perceived pitch heights, on the other.
The theory of
well-formed scales, as developed over the past two decades by the authors and
other music theorists, addresses the robust nature of the usual diatonic and
pentatonic scales as pitch collections, but until recently it has not explored
in detail the properties of the various scale orderings, or modes. The field of
algebraic combinatorics on words, which has also had
much of its development in the past two decades, provides the tools for such
explorations. The modes of well-formed scales correspond abstractly to certain
privileged words of the free monoid of words on a
two-letter alphabet, the conjugates of Christoffel
words. In particular, the usual major mode and the corresponding natural minor
mode, the modes underlying most of the music of the common practice era, correspond
to standard and anti-standard words, respectively. In our paper we present an
introduction to the theory, and outline the recent developments.
_______________________________________________________________
Gregory Cherlin
Department
of Mathematics
Rutgers
University
Title: Structure/Nonstructure
for Classes of Finite Models.
Abstract: If one looks for Ôdividing linesÕ
between highly structured and unstructured classes of finite relational
systems, one natural criterion is the property of well quasi-ordering with
respect to isomorphic embedding; a quite different dividing line is the existence
of a universal countable structure in the corresponding class of countable
models (whose finite substructures lie in the specified class). For any such
dividing line, we have a corresponding decision problem: to determine, for any
specified class of Ôforbidden substructures,Õ on which side of the line the
corresponding class of finite structures lies. For the two criteria just
mentioned, these decision problems remain open.
I will discuss
work with Latka on the former in the context of
tournaments, where Kruskal's tree theorem makes an
appearance, and work with Shelah on the latter in the
context of graphs, where model theoretic notions (aleph_0-categoricity,
algebraic closure) play a leading role.
_______________________________________________________________
Martin Davis
Department of
Computer Science
New York
University
Title: Empirical Platonism
Abstract: In his Gibbs lecture of 1951,
Gšdel said: ÒIf mathematics describes an objective world just like physics,
there is no reason why inductive methods should not be applied in mathematics
just the same as in physics.Ó I will track Gšdel's changing philosophical views
over his lifetime, and try to make sense of this suggestion.
_______________________________________________________________
Michael Detlefsen
Department of Philosophy
University of Notre Dame
Title: Freedom and Its Ends
Abstract: Freedom has been an enduring theme
of writings in the foundations
of mathematics. In this paper I explore the ends it has been taken
to serve and
limits on its legitimate exercise.
_______________________________________________________________
Solomon Feferman
Departments
of Mathematics and Philosophy
Stanford
University
Title: WhatÕs definite? WhatÕs not?
Abstract: Most axiomatizations
of set theory that have been treated metamathematically
have been based either entirely on classical logic or entirely on intuitionistic logic.
But a natural conception of the set-theoretic universe is as an
indefinite (or ÒpotentialÓ) totality, to which intuitionistic
logic is more appropriately applied, while each set is taken to be a definite
(Òor completedÓ) totality, for which classical logic is appropriate; so on that
view, set theory should be axiomatized on some
correspondingly mixed basis.
Similarly, in the case of predicative analysis, the natural numbers are
conceived to form a definite totality, while the universe of sets (or
functions) of natural numbers are viewed as an indefinite totality, so that,
again, a mixed semi-constructive logic should be the appropriate one to treat
the two together. In the first
part of the talk I will present ways of formulating such semi-constructive
systems of analysis and set theory and survey some results characterizing their
proof-theoretic strength.
Interestingly, though the logic is weakened, one can usefully strengthen
certain principles. In the
last part of the talk I will relate this work to the controversial discussion
as to whether certain statements in the language of set theory such as the
Continuum Hypothesis express definite or indefinite problems.
_______________________________________________________________
Hartry Field
Department
of Philosophy
New
York University
Title: Truth and Quasi-Impredicativity
Abstract: Friedman and Sheard
1975 is a definitive exploration of the most attractive classical options for
truth and satisfaction. Supplemented with McGee's omega-inconsistency theorem,
it shows how bleak the options for a classical theory are, and invites
reconsideration of non-classical options. Part of my paper will survey the
current state of play with the non-classical options on truth and
satisfaction—and on the closely-related theory
of properties. I will then raise some questions about whether this theory of
properties might be of interest in connection with FriedmanÕs program of
reverse mathematics, and about the relation of this theory to the subsystems of
second order arithmetic (esp. ATR_0) standardly
considered there.
_______________________________________________________________
Harvey Friedman
Department of
Mathematics
The Ohio State
University
Title: Foundational Adventures for the Future
Abstract: As I start the serious part of my
career, I have been reflecting on some Foundational Adventures for the Future. I
will briefly touch on several adventures about which I have some definite
ideas:
Boolean Relation
Theory, Strict Reverse Mathematics, Concept Calculus, Systematic Finitization, Finite to Infinite, Incompleteness/Unsolvability, Completeness/Solvability, Interpretability,
New Axioms (set theory), Practical Proof Theory, Foundational Exposition.
Programming
Language Design, Program Verification, Computer Assisted Education, Certainty.
Foundations of: Ultrafinite and Applicable Mathematics,
Probability/Statistics, Physical Theories, Randomness, Isms (philosophy of
mathematics), Law/Politics/Ethics.
Digitally
Sculptured Piano Performance, Piano Pedagogy, Extraordinary
Ordinary Piano Performance.
_______________________________________________________________
Geoffrey Hellman
Department of
Philosophy
University of
Minnesota
Title: On the Gšdel-Friedman
program
Abstract: After reviewing the leading
ideas and some of the striking post-Gšdel developments of the program of
identifying and justifying (old and) new set-theoretic axioms, we turn to a
closer examination of indispensability claims relating to strong axioms of
infinity. In addition to the question of the Ôgenuine mathematicalityÕ
of the statements of Ôordinary mathematicsÕ that are loosely said to Ôrequire
large cardinalsÕ—a question debated by Feferman,
Friedman, and others—we discuss two main gaps: (1) that between (even
strong) consistency statements and mathematical existence; and (2) that between
literal truth of strong set-theoretic axioms as standardly
formulated and truth of more general (and strictly weaker) formulations not
committed to the fixed universe view of sets as abstract particulars. On (1),
we promote the cogency of GšdelÕs idea of explanatory power. On (2), we
highlight the multiplicity of ways of expressing Ôabstract mathematical
contentÕ and draw some inferences bearing on ÔWhat is (really) indispensable
for what?Õ
_______________________________________________________________
Denis Hirschfeldt
Department of
Mathematics
University of
Chicago
Title: What I Would Tell My Graduate
Student Self About Reverse Mathematics
Abstract: The program of reverse mathematics
was introduced by Harvey Friedman in the mid-1970s, and has since attracted the
attention of a large number of researchers. Many of us have come from
computability theory, because of the close relationship between reverse
mathematics and effective mathematics. I first learned about the subject as a
graduate student, and while I appreciated the technical elements involved, I
had some trouble seeing what it had to say for someone who is in a certain
sense an anti-foundationalist. By way of a partial
answer, this survey will focus on some recent results in the reverse
mathematical and effective analysis of combinatorial and model theoretic
principles, treating them as case studies in the similarities and differences
between these two approaches, and the kinds of insight into the nature of
mathematical statements and constructions that they both can yield.
_______________________________________________________________
Jeff Hirst
Department of
Mathematical Sciences
Appalachian State
University
Title: Reverse mathematics of Ramsey theory
Abstract: By 1976, Harvey Friedman had finalized the hierarchy of
axiom systems that form the foundation of reverse mathematics. Over the intervening decades, the
methodology of reverse mathematics has been used to analyze the relative
strength of hundreds of mathematical theorems. In this talk, we will explore some applications to variations
of Ramsey's theorem, including both early and recent results.
_______________________________________________________________
Victor Marek with
J.B. Remmel
Department of
Computer Science Computer
Science and Mathematics
University of
Kentucky University
of California
Title: Reasoning about infinite sets
Abstract: The Answer Set Programming
mechanism [MT99,NIE99] can be used for
reasoning about infinite sets. A number of formalisms allows for
suitable encoding of (some) infinite set so that there are algorithms that
allow test if the sets so encoded are included in each other or are
disjoint.
Examples of such
formalisms include sets defined by finite automata, convex
polygons in the plane over rationals, and other
classes of infinite sets.
Additional
elements of a reasoning mechanism may involve monotone idempotent
operators. In a series of papers [CRM05,BMR08,MR09]
we developed a
formalism that allows one to reason about codable
infinite sets when some abstract
conditions are met.
In this
presentation we discuss both general results related to such
formalisms, and specific examples that may give rise to practical systems.
[BMR08]
H.A. Blair, V.W. Marek, and J.B. Remmel
Set-based Logic Programming.
Annals of Mathematics and Artificial Intelligence 52, 81–105, 2008
[CRM05]
D.W. Cenzer,
J.B. Remmel, and Marek,
V.W.
Logic Programming with Infinite
Sets.
Annals of Mathematics and Artificial Intelligence 44,
309–339, 2005
[MR09]
Marek, V.W. and J.B. Remmel
Automata and Answer Set Programming.
Proceedings of LFCS 2009.
[MT99]
Marek, V.W. and Truszczynski, M.
Stable Models and an Alternative
Logic Programming Paradigm.
The Logic Programming Paradigm, pp.
375–398.
Series Artificial Intelligence,
Springer-Verlag, 1999.
[Nie99]
NiemelŠ, I.
Logic programs with stable model
semantics as a constraint programming paradigm.
Annals of Mathematics and Artificial Intelligence 25, 3,4, 241–273, 1999
_______________________________________________________________
Dave Marker
Department of
Mathematics, Statistics, and Computer Science
University of
Illinois at Chicago
Title: Isomorphism for first order
theories
Abstract: I will report on some results
about the Borel complexity of isomorphism relations
for countable models of a first order theory.
_______________________________________________________________
Grigori Mints
Department
of Philosophy
Stanford
University
Title: Analytic Cut in Modal Logic:
System B
Abstract: When standard approaches to cut
elimination do not work, analytic cut (on subformulas
of the proved formula) can be sufficient. We present a general framework for
proving corresponding normalization theorem and apply it to two difficult
cases: S5 and the system B characterized by Kripke
models with reflexive and symmetric accessibility relations. The system B
appeared in studies of vagueness by K. Fine and T. Williamson, and in
a recent study of safe reasoning by T. Williamson.
_______________________________________________________________
Antonio Montalban
Department of
Mathematics
University of
Chicago
Title: Theories of Hyperarithmetic
Analysis.
Abstract: Subsystems of second order
arithmetic, all whose models are closed under hyperarithmetic
reduction and which have HYP as a model, are called Theories of Hyperarithmetic analysis. Friedman and others started
studying these in the seventies. The work on these theories has started again
in the last few years because we found the first example of a natural theorem
of mathematics that falls in this category. I will present the work done in
this area in the seventies and in the last few years, and directions for future
work.
_______________________________________________________________
Anil Nerode
Mathematics,
Cornell University
Title: Update Transducers
Abstract: Update transducers formalize systems of automata governing evolution of input-output networks of agents or databases or other structures. Inputs and outputs are infinite sequences of discrete or continuous objects such as integers, real numbers, elements of a Banach space, or elements of algebra. Continuous entities are NOT treated by approximation. Update transducers allow one to analyze, by automata theoretic methods, evolutions where the input and output sequences consist of elements from structures of any cardinality. This work is joint with J.B. Remmel. Update transducers were announced as a topic of research at the International Workshop on Topological Methods in Logic, June 3—5, 2008, Tbilisi, Georgia.
My motivation for introducing update automata was to justify a longstanding conviction that underlying every mathematical algorithm working on abstract entities there is a finite guiding automaton. (How longstanding this was is indicated by the fact that update transducers finally extend Nerode's 1958 characterization of linear automaton transformations over finite rings to infinite rings in a simple way.) In 2008 dissertations under my direction Bryant Adams developed update transducers induced by systems of linear differential equations with forcing functions, while Eduardo Carta developed Green's functions (generating functions, transfer functions) for update transducers induced by linear recurrences with variable coefficients over semirings. I suggested these investigations in order to show the strength of the notion, and specifically in order to use update transducers linear over tropical semirings to describe the evolution of state of distributed databases and multi-agent systems. There is an operational calculus of transforms, which applies to such networks in the same way linear transfer functions apply to linear electrical networks. How useful are these transforms to characterize behavior and to design networks? This remains to be seen.
A different view of update transducers is that they are non-homogeneous systems of first order recurrence equations over arbitrary structures. This formulation makes the subject look like first order systems of non-linear difference equations.
In case an update transducer is an automatic structure, one obtains automata decision procedures for many questions. Since communicating agent networks and distributed databases are often guided by real time finite automata, this is not uncommon. The decision methods for answer set programming of Marek-Remmel are of this kind. This suggests that appropriate logics for update transducers may be automata theoretic languages incorporating unary relation symbols for the defining domains and function symbols for the update functions.
_______________________________________________________________
Rohit Parikh
CS, Math,
Philosophy
Brooklyn College
and CUNY Grad Center
Title: Knowledge, its logic and its effect
on society
Abstract: The sixties saw the publication of
two books which started a veritable movement in
reasoning about knowledge. They
were HintikkaÕs Knowledge
and Belief and David LewisÕ Convention. Hintikka was influenced by von Wright, and Lewis by the Nobelist
(2005) Schelling. But both
works were highly original.
Starting then, reasoning about knowledge has influenced Computer
Science, Philosophy and Economics.
The celebrated TARK conferences have been devoted to this area.
While Logic
(including Complexity theory) has played a big role here, there is also a role
for Game Theory (starting with AumannÕs 1976 classic,
ÔAgreeing to disagreeÕ) and for softer developments coming from Social Science
and Animal Cognition. Knowledge
transmission is a powerful tool, used by kings to project power, by the City of
San Francisco to help public transport riders, and by the Taliban to enable
their reign of terror.
We will give a
survey of the technical developments and indicate why logicians should take a
serious look at this new way they can contribute to the well being (via
understanding) of society.
_______________________________________________________________
Michael Rathjen
Department of
Mathematics
University of
Leeds
Title: Infinitary Proof Theory and Pi-0-2
Conservation
Abstract: Hilbert envisioned the methods of
proof theory to be completely finitistic in character.
In the 1920s, Ackermann and von Neumann, in pursuit of Hilbert's Programme, were working on consistency proofs for arithmetical
systems, but already with the infusion of an infinitary
concept. Beginning in the 1950s, proof theory began to employ infinitary methods more frankly, first with the use of infinitary rules of inference (such as the omega rule) and
then with the use of infinitely long formulas. At first, these rules, formulas
and the resulting derivations were all countable, but eventually proof theory
moved on to make use of prima facie uncountably long rules of inference and/or
formulas, thence uncountably long derivations. These countably and uncountably long
derivations have been applied to treat various formal systems for parts of
analysis and set theory, by translating their finite derivations into corresponding
infinite ones of a more purely logical character. By then applying the process
of cut-elimination or other forms of normalization, the latter are transformed
into detour-free derivations whose associated ordinals give a measure of
complexity to the systems thus treated.
In the talk I will take up the question
why infinitary proof theory yields finitistic reductions. It (almost) always establishes a
conservative extension result that says that a given formal system T is a conservative
extension of a system of arithmetic plus transfinite induction on an ordinal
representation system, for Pi-0-2 sentences. Moreover, the conservative
extension statement itself is a Pi-0-2 sentence and this Pi-0-2 sentence has a
ÔreasonableÕ Skolem function.
_______________________________________________________________
Jeff Remmel
Department of
Mathematics
University of
California at San Diego
Title: Pi^0_1 Classes in Mathematics
Abstract: XXX
_______________________________________________________________
Gerald Sacks
Department
of Mathematics
Harvard
University
Title: Models of long sentences
Abstract: A straightforward construction of
models of sentences of (infinity-omega)-infinitary
logic of ordinal rank less than omega-2 under suitable conditions.
_______________________________________________________________
Andre Scedrov
Department
of Mathematics
University of
Pennsylvania
Title: Foundations of Network Security Protocol Analysis
Abstract: The design and security analysis of
protocols that use cryptographic primitives
is one of the most fundamental and challenging areas of computer
security research. Relatively succinct but subtle authentication, key exchange,
negotiation, authorization, and related protocols are the building blocks for secure
distributed systems. Protocol analysis is a successful scientific area with two
important but historically independent foundations, one based on symbolic
computation and one based on computational complexity theory. We discuss these
perspectives and the ways they relate to each other. As a case study, we
highlight joint work with Cervesato, Jaggard, Tsay, and Walstad on
the formal analysis of the Kerberos 5 authentication protocol suite.
This work discovered a serious vulnerability in the Kerberos public-key
extension and caused a Microsoft security patch for Windows 2000 and Windows XP
operating systems. The work contributed to the reformulation of the industry
standard for Kerberos public-key extension and provided security proofs of the
corrected version of the protocol, the latter jointly with Backes.
The flaw discovered is not a flaw in implementation or in cryptography, but a
protocol-level, structural flaw, which is present even when the underlying
cryptographic operations and network infrastructure operate normally. The
methodology developed in this work is applicable to a wide range of network
security
protocols. We also discuss current joint work with Blanchet on mechanized proofs
of authentication and key secrecy properties of Kerberos 5, both with and
without its public-key extension.
_______________________________________________________________
Kevin Scharp
Department of
Philosophy
The Ohio State
University
Title: Modal Semantics for Descending
Truth
Abstract: As an approach to the liar paradox,
I claim that truth is an inherently defective concept that needs to be
replaced. I suggest two
replacement concepts, ascending truth
and descending truth. In this talk, I present a theory of
ascending and descending truth (ADT) and investigate whether modal logic can
help provide a semantics for it. Virtually all the work done on
semantics for modal logics is on either relational semantics or neighborhood
semantics. However, an easy extension
of Montague's theorem shows that neither relational semantics nor neighborhood
semantics will work for ADT. I
present a general semantics for modal logics that has neighborhood semantics
and relational semantics as special cases. Since ADT is a theory of predicates instead of operators,
the standard inductive definition of satisfiability
at a world does not work. Instead,
I use transfinite revision sequences to define satisfiability
at a world for the descending truth predicate—the ascending truth predicate
is then defined in terms of descending truth and negation. Along the way, I compare and contrast
ADT with the theory of truth proposed by Feferman and
the theory of truth proposed by Friedman and Sheard.
_______________________________________________________________
Wilfried
Sieg
Department of
Philosophy
Carnegie Mellon
University
Title: Is there a proof of ChurchÕs Thesis?
Abstract. The question has been of deep interest
to Harvey Friedman, and it has been the focus of many papers ever since Alonzo
Church in [1935] suggested the ÒidentificationÓ of the informal concept of
effective calculability with GšdelÕs mathematical concept of general recursiveness.
Kleene presented in [1952] the arguments for
this thesis including a careful
discussion of TuringÕs 1936-analysis. In his [1980], Gandy argued that TuringÕs
analysis really is a proof of
ChurchÕs Thesis.
Dershowitz and Gurevich
in [2008] deny, rightly from my perspective, GandyÕs assertion. They present what they claim to be the
first Òcomplete axiomatizationÓ of computability and
argue that ChurchÕs Thesis Òprovably followsÓ from their four general
postulates. (E.g., p. 339 and p. 307). I analyze their argument and contrast it
with my proposal of axioms for computability given in [2002]. My axioms are rooted in TuringÕs
analysis and GandyÕs work.
However, there is no proof of ChurchÕs Thesis; rather, the axioms are
shown to ensure that the computations of any model can be simulated by Turing machines. That, I argue, is the best one
can do.
References
Church, A.
1935 An
unsolvable problem of elementary number theory. Preliminary
report (abstract); Bulletin of the American Mathematical Society 41, 332-333.
Dershowitz,
N. and Gurevich, Y.
2008 A natural axiomatization of computability and proof of ChurchÕs
Thesis; Bulletin of Symbolic Logic, 14 (3), 299-350.
Gandy, R.
1980 ChurchÕs Thesis and
principles for mechanisms; in: The Kleene Symposium (J. Barwise,
H.J. Keisler, and K. Kunen,
eds.), North-Holland Publishing Company, Amsterdam, 123-148.
Kleene,
S.C.
1952 Introduction to Metamathematics;
Elsevier, Groningen.
Sieg, W.
2002 Calculations
by man and machine: mathematical presentation; in: In the Scope of Logic, Methodology and Philosophy of Science,
volume one of the 11th International Congress of Logic, Methodology
and Philosophy of Science, Cracow, August 1999 (P. GŠrdenfors,
J. Wolenski and K. Kijania-Placek,
eds.), Synthese Library volume 315, Kluwer, 247-262.
Turing, A.
1936 On computable numbers,
with an application to the Entscheidungsproblem; Proceedings of the London Mathematical
Society, series 2, 42, 230-265.
_______________________________________________________________
Theodore Slaman
Department of
Mathematics
University of
California, Berkeley
Title: Borel
Determinacy and Randomness
Abstract: We will discuss joint work with
Jan Reimann in which Borel
Determinacy is invoked in an essential way to analyze a recursion theoretic
aspect of randomness.
For n a natural
number, let NCR(n) be the set of infinite binary sequences
x such that there is no (representation of a) continuous probability measure m
such that x is n-random relative to m.
We show that for all n, NCR(n) is
countable. The proof relies
heavily on Martin's proof of Borel Determinacy. Further, the use of Borel
Determinacy is essential in that this statement cannot be proven using finitely
many iterates of the power set of the reals.
The natural
transfinite extensions of these results also hold. Thus, there is a second route to proving FriedmanÕs Theorem
that Borel Determinacy makes essential use of uncountably many iterates of the power set axiom.
_______________________________________________________________
Reed Solomon
Department
of Mathematics
University
of Connecticut
Title: Reverse mathematics and group theory
Abstract: Harvey Friedman developed the program of reverse
mathematics to measure the proof theoretic strength of theorems of
ordinary mathematics by analyzing the set theoretic axioms need to prove
them. Over the past 30
years, theorems in many areas of mathematics have
been classified in this program.
This talk will focus on reverse
mathematics results in group theory and ordered group theory, covering the
work of Harvey Friedman and others as well as presenting some new
results.
_______________________________________________________________
Patrick Suppes
Stanford
University
Title: Neglect of Independence and
Randomness in the Axioms of Probability
Abstract: The classic 1933 axiomatization of Kolmogorov is
purely measure-theoretic. There is
no mention or use of the concepts of independence or randomness, which are the
most important probability concepts not shared by finite
additive measures not normed to one. But
simply fixing the sum to be one is only a convention in the context of Kolmogorov's other axioms. (Kolmogorov
does discuss in detail independence immediately after stating his axioms) Simple axioms using independence or
randomness can be added to eliminate this defect. Qualitative comparative axioms of probability have been much
investigated, and those for independence much less so. I give what I think are new qualitative
comparative axioms for randomness, and then explore, in this qualitative setting
using Padoa's principle, the independence of these
three basic concepts:
comparative probability, independence and randomness. If time permits, methods derived from ergodic theory will be used to represent just in terms of
Bernoulli processes the randomness of familiar statistical systems, such as the
randomness of three correlated
random variables, or a Markov chain.
_______________________________________________________________
Christian Tapp
Katholisch-Theologische FakultŠt
RuhruniversitŠt Bochum
Title: Absolute infinity - Between
mathematics and theology?
Abstract: The class of all ordinals, the
class of all cardinals, and the class of all sets are examples for proper
classes: assuming that they are sets leads to paradox. So they should not be
taken to be proper objects of mathematics. Nevertheless they are infinite.
Cantor called this kind of infinity Òabsolute infinityÓ. Some have held that
there is an immediate connection between this mathematical kind of infinity and
theological or philosophical conceptions of God, the absolutely infinite being.
Cantor's aleph series was said to be Òfootsteps to the throne of GodÓ, absolute
infinity was taken as a Òmetaphysischer GrenzbegriffÓ (Clayton with reference to Kant). Can
absolute infinity bridge the gap between mathematics and theology?
_______________________________________________________________
Simon Thomas
Department
of Mathematics
Rutgers
University
Title: The Friedman Embedding Theorem
Abstract: The Higman-Neumann-Neumann
Embedding Theorem states that every countable group G can be embedded into a
2-generator group K. In this talk, I will consider the question of whether
there exists a Borel choice which
has the property that isomorphic groups G are assigned isomorphic
2-generator groups K.
_______________________________________________________________
Albert Visser
Department of
Theoretical Philosophy
University of
Utrecht
Title (for the talk): Logics and Admissible Rules of
Theories
Title (for the Proceedings): The
lowest degree of local interpretability
Abstract: The logic of a theory U is the set
of principles, of a given signature, that are valid in U under all
interpretations. A rule Ôinfer C from BÕ is admissible over a theory, if every
interpretation of B in U, also is an interpretation of C. One can view logics
of theories and admissible rules as the schemes and schematic rules that can be
conservatively added to a theory.
We first discuss
the case where the interpreted signature is propositional. Note that the
interpreting theory may be, but need not be, propositional. If we just consider
classical theories and the language of propositional logic, our notions
trivialize. However, if one considers constructive interpreting theories or an
interpreted signature for modal logic,
the material becomes definitely non-trivial. I will discuss the case where we consider
interpretations of
the signature of propositional logic in a constructive theory.
If the
interpreted signature is a signature of predicate logic, lots of interesting things
happen. In the constructive case
the logics of some salient arithmetical theories are complete Pi^0_2. All theories, whether constructive or
classical, satisfy a non-trivial admissible rule, which is just a reformulation
of the Second Incompleteness Theorem.
We provide some
characterizations of admissible rules and predicate logics of classical
sequential theories. We present an example of a classical sequential theory
that has a Pi^0_2-complete logic.
_______________________________________________________________
Bruce Weide
Department of
Computer Science and Engineering
The Ohio State
University
Title: Progress on the Verified Software
Grand Challenge: The Resolve Approach
Abstract: A Ôverifying compilerÕ (a tool
that, in its purest form, would compile only
programs that it could prove correct) has long been a dream of the
software formal methods community.
Jim King apparently coined the term in his 1969 Ph.D. thesis, and 35
years later Tony Hoare proposed the development of a verifying compiler as a ÔGrand
Challenge for Computing ResearchÕ.
Visions of software verification foundations and technology that would
qualify as meeting this challenge have driven the research of the OSU
Resolve/Reusable Software Research Group for over two decades. This talk/paper will not be a survey of
the field. Rather, it will explain
to a mathematics/logic audience how our group's verifying compiler will work,
why it will be a significant advance over current practice, why reaching the
goal is still considered a ÔchallengeÕ (not just technically but also for
educators of future software engineers), and how Harvey Friedman's involvement
in this project has contributed to our progress in addressing the challenge.
_______________________________________________________________
Andreas Weiermann
Department
of Mathematics
University
of Gent
Title: Well-quasi orderings and
independence results
Abstract: Harvey Friedman has pioneered
impressive independence results (for subsystems of analysis) related to
well-quasi orderings (via so-called miniaturizations). In this talk I will
survey some of these famous results and I will describe recent developments in
the area concerning phase transitions and maximal order types.
_______________________________________________________________