This will also be an organizational meeting of the seminar for the spring quarter. The first regular meeting of the Logic Seminar will be on Tues. April 16. Speaker, Grigori Mints on the use of proof theory in extracting the constructive content of non-constructive proofs in analysis (report of work by U. Kohlenbach on unwinding proofs in the theory of approximation). Possible topics of further reports will be discussed at the April 9 meeting.
The first meeting of the Logic Lunch this quarter will be on Friday April 12, separate announcement to follow.
Most of the existence proofs in mathematics are constructive as they stand or are easily made constructive by an expert. Proof theory provides tools for constructivization of essentially non-constructive proofs. A new constructive proof uses the data already present in the formulation of the problem as well as special features of the problem _and_ the old proof. This is illustrated by work of U. Kohlenbach on constructivization of two results: Uniqueness of L_1-approximation and asymptotics for Krasnoselski-Mann iteration for finding fixpoints of non-expansive mappings. No previous knowledge of proof theory and very modest background in analysis is assumed.
Two replacements for Frege's infamous Axiom (V) of his Basic Laws of Arithmetic are considered first. The first, "Numbers", is a particular corollary of Axiom (V) that is sufficient for Frege's development of arithmetic, but insufficient to derive Russell's paradox. The second, "New V", is a restriction on concept formation to those that are sufficiently "small". Together with the axioms of second order logic, "Numbers" and "New V" are relatively consistent with second order arithmetic and sufficient for the development of arithmetic.
Frege's Foundations of Arithmetic does not contain a formal system like the system found in the Begriffsschrift and the Basic Laws of Arithmetic. Boolos examines the presupposition that it is only the lack of formality in the Foundations that saves it from inconsistency. He proposes a system FA for capturing the content of the mathematical program in the Foundations, and claims that FA is in fact a consistent system.
The last part of the talk presents chapter 14 of Logic, Logic and Logic where Boolos discusses the origin of the contradiction in Frege.
Darko presents chapter 14 of Logic, Logic and Logic where Boolos discusses the origin of the contradiction in Frege. Audrey reviews some of further work. Ed discusses Frege, Boolos, and Logical Objects. Abstract:
In this talk, I discuss entities Frege would have called "logical objects" (extensions, numbers, truth-values, etc.), describe my attempt to rehabilitate Frege's theory for introducing such objects, and compare it with that of Boolos. I try to show that the `eta' relation that Boolos deployed on Frege's behalf is similar, if not identical, to the encoding mode of predication that underlies my theory of abstract objects. Boolos uses unrestricted comprehension over Properties and used the `eta' relation to assert the existence of logical objects under certain highly restricted conditions. By contrast, I use unrestricted comprehension over logical objects and banish formulas with encoding subformulas from comprehension over Properties.
Constructive set theory grew out of Myhill's endeavours to discover a simple formalism that relates to Bishop's constructive mathematics as $ZFC$ relates to classical Cantorian mathematics. Aczel then modified Myhill's set theory to a system which he called Constructive Zermelo-Fraenkel Set Theory ($CZF$). Two hallmarks of this theory are that it possesses a canonical interpretation in Martin-L\"of type theory ($MLTT$) and that it provides a rather powerful framework for developing mathematics constructively, making the process of formalization rather simple.
Surprisingly, many metamathematical properties of $CZF$ and related theories are not known. Is there a good (complete) characterization of the set- theoretic statements validated in $MLTT$? Does $CZF$ have the disjunction property and/or the set existence property? It turns out that the answer to the former question strongly bears on the second question and that it is closely related to a search for the strongest forms of the axiom of choice allowable in a constructive extensional set theory.
Another important axiom in this context is the so-called Regular aExtension Axioms ($REA$). It is the main tool for showing that inductive definitions give rise to sets rather than classes. In the talk I intend to relate also some new results about the meta-mathematical status of $REA$ in connection with $ZF$, $CZF$, and similar theories.
Further progress in establishing interpolation theorems for superintuitionistic and modal logics depends on finding treatment of new kinds of deductive formulations like multiple-sequent and tableau calculi. A new translation of sequents and tableaux into formulas is proposed for intuitionistic logic. It allows extension of a standard proof of the interpolation theorem to multiple succedent sequents and tableaux, closing gaps in some previous proofs. This can open way to solution of open problems.
Augmenting constructive Zermelo-Fraenkel set theory, CZF, by the regular extension axiom, REA, allows one to prove that many inductively defined classes are sets. In this talk I shall compare variants of REA and gather together results about their deductive relationships and independence on the basis of CZF and classical Zermelo-Fraenkel set theory.
Proof mining is the process of logically analyzing proofs in mathematics with the aim of obtaining new information. This talk is based on a joint paper with Ulrich Kohlenbach as a part of a case study in proof mining applied to fixed point theory. More specifically, we are concerned with the fixed point theory of directionally non-expansive self-mappings of convex sets in hyperbolic spaces.
In previous work, Kohlenbach derived an explicit quantitative version of a theorem due to Borwein, Reich and Shafrir on the asymptotic behavior of Mann iterations of non-expansive mappings of convex sets C in normed linear spaces. This quantitative version, which was obtained by a logical analysis of the ineffective proof given by Borwein, Reich and Shafrir, could be used to obtain strong uniform bounds on the asymptotic regularity of such iterations in the case of bounded C and even weaker conditions.
In this talk we present extensions of these results to hyperbolic spaces and directionally non-expansive mappings. In particular, we obtain significantly stronger and more general forms of the main results of a recent paper by W.A. Kirk with explicit bounds. As a special feature of our approach, which is based on logical analysis instead of functional analysis, no functional analytic embeddings are needed to obtain our uniformity results which contain all previously known results of this kind as special cases.