Kreisel's conjecture stated that if Peano Arithmetic PA
proves A(Sn0) for
each n by a proof with ≤ k lines then PA proves
∀xA(x). It had been proved by
R. Parikh (Zbl 0269.02011) for a monadic formulation of PA
with S as the only function and predicates for addition and
multiplication. The paper under review provides a detailed treatment
in numerous special cases for the following drastic modification by
G. Kreisel (in a supplement to Zbl 0609.03019).
Suppose that π is a proof
of A(Sn0) for just one (but
large) n. Then there is an infinite
set X(Π,A) ⊆ N with proofs of
the same logical form Π π for
all A(Sm0) with m
∈ X(Π,A). The central notion in the reviewed
paper is uniform derivability of a schema (by one and the same proof
schema for all instances) instead of derivability in k
steps. Descriptions of the sets X(Π,a) are
derived from the properties of linear diophantine equations describing
the proof schema. Equivalent (with respect to the set of theorems)
formulations of PA behave differently in this respect. The ordinary
successor induction gives uniform proofs of
∃x(x+x=S2n0),
whereas the order induction schema ∀α(∀β<α
A(β) → A(α)) → ∀α
A(α) admits generalization from n sufficiently
large to A(Snx). Hence
the successor induction schema is not uniformly derivable from order
induction, while the other direction holds in the presence of finitely
many basic arithmetical axioms. A long postscript by G. Kreisel
supplements and criticizes the main body of the paper.
Proper subsystems Ps-Prop2 and
P-Prop2 of the ordinary intuitionistic propositional
calculus Prop2 considered here are negationless in the
sense that negation is not definable and all subformulas are
“motivated”:
if A1,…,An
⊦ F then there is a substitution σ such that
⊦ σ A1,… ⊦
σ An, ⊦
σ F. This is achieved by restriction on the axioms
introducing assumptions of natural deduction: Γ,A
⊦ A is an axiom only if ⊦ σ A for
some substitution σ. “Initial” σ simply
substitutes ⊤ (truth) for everything. Restricted subsystems
Ps-Prop2
and P-Prop2 are intertranslatable with
Prop2 by devices similar to (but simpler than) ones used
earlier by other authors for predicate logic and
arithmetic.
The Multiple Birkhoff Recurrence theorem by Furstenberg and Weiss in
1978 is a seminal result for the interaction between topological
dynamics and combinatorics, establishing Ramsey-type theorems through
corresponding recurrence results. However, while combinatorial proofs
often contain explicit quantitative information, topological proofs
usually do not contain realizers, bounds or similar data. E.g. for van
der Waerden's theorem—for every finite colouring of the integers
one colour contains arbitrarily long arithmetic progressions—one
may ask for a number N = N(q; k)
such that for every q-colouring of [0;N], one colour
contains a progression of length k. The combinatorial proof
contains an explicit upper bound
on N(q; k), while Furstenberg and Weiss'
topological proof does not. Thus one may ask: what is the algorithmic
content of the topological proofs of Ramsey-type theorems. We will
present an analysis of Furstenberg and Weiss' Multiple Birkhoff
Recurrence theorem which generalizes a previous analysis by Girard. We
will also discuss the use of compactness in proofs of the Multiple
Birkhoff Recurrence theorem, i.e. the concept of minimality in
topological dynamics, sketch the treatment of generalizations of the
Multiple Birkhoff Recurrence theorem, and, if time permits, survey
some related proof mining results in ergodic theory.
Modern logic was originally developed in large part in order to
provide a mathematical model of theorem-proving, a model about which
theorems could be proved. Differences between a mathematical model and
what is modeled are only to be expected, but in the case of logic,
these have sometimes provoked rather strange reactions. One
difference, in particular, has given rise to rather extravagant
philosophical claims under the label “structuralism”. A
closer look at the logic of the situation suggests a way of improving
the modeling and avoiding the extravagance.
In this talk, I extend the argument in the paper
“What is
Neologicism?” co-authored with Bernard Linsky (Bulletin
of Symbolic Logic 12(1), June 2006, 60–99). Linsky
and I argued that if the notion of reduction used by the original
logicists is weakened, a new form of neologicism emerges that can be
generally applied to arbitrary mathematical theories. In the present
talk, however, I develop positive arguments for
thinking: (1) that the notion of reduction assumed by
the early logicists is the wrong notion of reduction given their
epistemological motivations and goals; (2) that the
notion of ‘ontological reduction’ defined in the paper
“Neo-logicism?
An Ontological Reduction of Mathematics to Metaphysics”
(Erkenntnis, 53(1–2), 2000, 219–265)
allows one to attain the epistemological goals driving
logicism; (3) that when the comprehension principle for
object theory is replaced by the equipotent abstraction principle, the
resulting system is a logic, given that we accept that weak
second-order logic is part of logic; and thus (4)
logicism is true: since arbitrary mathematical theories are
ontologically reducible in the logic of object theory, mathematics is
reducible to logic. This will be a survey talk for non-experts in algebra. The
applications covered will extend from Shelah's proof of the
undecidability of the Whitehead Problem to recent algebraic theorems
proved in ZFC using set-theoretic methods. A common theme is the use
of the Singular Compactness Theorem.
We formulate the first three of Euclid's five postulates
algebraically, and in lieu of postulates 4 and 5 postulate that every
finite set of points has a centroid. We show that the variety of
models of this algebraic theory is equivalent to the category
VctQ[i] of vector spaces over the complex
rationals. We complete any such model to a continuum, i.e. a vector
space over the complex numbers, using only the geometric primitives
defined by this theory, independently of any notion of number or
metric. Various subtheories characterize the vector spaces over the
reals, over the rationals, their affine (origin-free) counterparts,
the Gaussian integers, etc.
The counterpart of abelian groups in this framework is a notion of
grove arising naturally from Euclid's first two postulates. We show
that sets and groves are algebraic in each other, giving a rare
example of a structure as algebraically primitive as sets
themselves.
This system differs from Hilbert's second-order and Tarski's
first-order axiomatizations of geometry in four principal ways: it
matches Euclid's original postulates more closely; its model theory at
least for the rationals follows Szmielew in being more algebraic than
Tarski's; each variant of the theory determines its underlying field
up to isomorphism; and it limits itself to Euler's affine fragment of
Euclidean geometry extended to the complex numbers. Most theorems in mathematics state a fact about infinitely many
objects of a certain kind, e.g. all triangles. But the diagram used
in a proof only represents one such object, and it is an issue whether
the particular representation taken is typical, i.e. does not have
features which are not shared by all the objects under consideration.
This is a frequent concern when dealing with proofs of geometric
theorems that rely to a significant extent on diagrams. In this talk
I'll bring attention to a different kind of diagram that is ubiquitous
in modern mathematics, in which there is a single infinite
configuration under consideration, and what is exhibited in the
diagram is a typical finite part of that configuration, with the
balance indicated by the use of dots (…) in some way. The
consideration of such infinite diagrams is interesting because they
enlarge the question of what makes a diagram typical. Moreover, I
shall argue that there are certain proofs in modern mathematics where
the use of such infinite diagrams is essential, i.e. it is not
possible to even follow the proof without consulting the diagram at
practically every step of the way. In fact, there are certain
theorems that can't even be understood without reference to such a
diagram. This presentation will be a review of a recent paper, "A formal system for Euclid's Elements", by J. Avigad, E. Dean, and J. Mumma. It is available electronically at
Reviews of Two Recent Papers
Proof Mining in Topological Dynamics
Putting Structuralism in Its Place
A Defense of Logicism
Some Uses of Set Theory in Algebra
Complex Linear Algebra from a Modification of Euclid's Postulates
And So On…: Reasoning with Infinite Diagrams
Avigad, Dean and Mumma's “A formal system for Euclid's Elements”
http://arxiv.org/abs/0810.4315 .
The authors give a formal system for faithfully expressing the
Euclid's proofs in Elements, books 1–4 (on plane geometry),
especially Euclid's diagram-based reasoning. The work advances the
claim that Euclid's arguments are more rigorous than modern critics
suggest. I shall review some key features of the formal system: its
language, axioms and rules; the notion of a “direct
consequence” (which is intended to capture what intuitively can
be “read off” a diagram); ways in which the formalism
adheres to and diverges from Euclid; completeness; and
implementation.