Richard Zach

Jan Krajíček posed the following problem: Is there is a generalization result in the theory of real closed fields of the form: If A is provable in length k for all n ϵ ω , then A is provable? It is argued that the answer to this question depends on the particular formulation of the “theory of real closed fields.” Four distinct formulations are investigated with respect to their generalization behavior. It is shown that there is a positive answer to Krajíček's question for 1. the axiom system RCF of Artin-Schreier with Gentzen's LK as underlying logical calculus, 2. RCF with the variant LK B of LK allowing introduction of several quantifiers of the same type in one step, 3. LK B and the first-order schemata corresponding to Dedekind cuts and the supremum principle. A negative answer is given for 4. any system containing the schema of extensionality

Quantified propositional intuitionistic logic is obtained from propositional intuitionistic logic by adding quantifiers ∀p, ∃p, where the propositional variables range over upward-closed subsets of the set of worlds in a Kripke structure. If the permitted accessibility relations are arbitrary partial orders, the resulting logic is known to be recursively isomorphic to full second-order logic (Kremer, 1997). It is shown that if the Kripke structures are restricted to trees of at height and width at most ω, the resulting logics are decidable. This provides a partial answer to a question by Kremer. The result also transfers to modal S4 and some Gödel-Dummett logics with quantifiers over propositions

The period from 1900 to 1935 was particularly fruitful and important for the development of logic and logical metatheory. This survey is organized along eight "itineraries" concentrating on historically and conceptually linked strands in this development. Itinerary I deals with the evolution of conceptions of axiomatics. Itinerary II centers on the logical work of Bertrand Russell. Itinerary III presents the development of set theory from Zermelo onward. Itinerary IV discusses the contributions of the algebra of logic tradition, in particular, Löwenheim and Skolem. Itinerary V surveys the work in logic connected to the Hilbert school, and itinerary V deals specifically with consistency proofs and metamathematics, including the incompleteness theorems. Itinerary VII traces the development of intuitionistic and many-valued logics. Itinerary VIII surveys the development of semantical notions from the early work on axiomatics up to Tarski's work on truth.

After a brief flirtation with logicism around 1917, David Hilbertproposed his own program in the foundations of mathematics in 1920 and developed it, in concert with collaborators such as Paul Bernays andWilhelm Ackermann, throughout the 1920s. The two technical pillars of the project were the development of axiomatic systems for everstronger and more comprehensive areas of mathematics, and finitisticproofs of consistency of these systems. Early advances in these areaswere made by Hilbert (and Bernays) in a series of lecture courses atthe University of Göttingen between 1917 and 1923, and notably in Ackermann's dissertation of 1924. The main innovation was theinvention of the -calculus, on which Hilbert's axiom systemswere based, and the development of the -substitution methodas a basis for consistency proofs. The paper traces the developmentof the ``simultaneous development of logic and mathematics'' throughthe -notation and provides an analysis of Ackermann'sconsistency proofs for primitive recursive arithmetic and for thefirst comprehensive mathematical system, the latter using thesubstitution method. It is striking that these proofs use transfiniteinduction not dissimilar to that used in Gentzen's later consistencyproof as well as non-primitive recursive definitions, and that thesemethods were accepted as finitistic at the time.