Dieter Probst - Concepts of Proof in Mathematics, Philosophy, and Computer Science

Concepts of Proof in Mathematics, Philosophy, and Computer Science

Ontos Mathematical Logic

Edited by

Wolfram Pohlers, Thomas Scanlon,
Ernest Schimmerling, Ralf Schindler,
Helmut Schwichtenberg

Volume 6

ISBN 978-1-5015-1080-9

e-ISBN (PDF) 978-1-5015-0262-0

e-ISBN (EPUB) 978-1-5015-0264-4

ISSN 2198-2341

Library of Congress Cataloging-in-Publication Data

A CIP catalog record for this book has been applied for at the Library of Congress.

Bibliographic information published by the Deutsche Nationalbibliothek

The Deutsche Nationalbibliothek lists this publication in the Deutsche Nationalbibliografie; detailed bibliographic data are available on the Internet at http://dnb.dnb.de.

2016 Walter de Gruyter GmbH, Berlin/Boston

www.degruyter.com

The Humboldt-Kolleg Proof held in Bern, Switzerland, from 9th to 13th September 2013 was a try to give due consideration to the depth and breadth of the time-honoured concept of proof, by gathering leading scholars from mathematics, informatics and philosophy whose studies are centered at the concept of proof. The present volume is an attempt to represent many of their approaches in print, which can briefly be summarized as follows.

In Herbrand Confluence for First-Order Proofs with -Cuts Bahareh Afshari, Stefan Hetzl and Graham E. Leigh assign to each first-order proof with cuts of complexity at most a well-behaved formal grammar of limited size; all normal forms obtained by non-erasing cut reductions result in the same Herbrand expansion.

Proof-Oriented Categorical Semantics is Marco Beninis alternative interpretation of the entity of which the first-order proposition-as-types correspondence and the associated type systems are equivalent but different presentations in distinct categories; his framework embraces standard first-order categorical semantics.

In Logic for Gray-Code Computation Ulrich Berger, Kenji Miyamoto, Helmut Schwichtenberg and Hideki Tsuiki study real number computation with Gray code from a constructive angle, to extract algorithms from proofs with inductive and coinductive definitions; their case studies are formalized in the proof assistant Minlog.

Douglas S. Bridges in The Continuum Hypothesis Implies Excluded Middle shows within the framework of Bishop-style constructive mathematics that the ContinuumHypothesis resembles the Axiom of Choice also inasmuch as it implies the Lawof Excluded Middle, and discusses a more explicit Brouwerian counterexample.

Theories of Proof-Theoretic Strength ( +1 ) by Ulrik Buchholtz, Gerhard Jger and Thomas Strahm is about a range of theories with proof-theoretic ordinal ( +1 ); it is not only that this ordinal parallels the one of predicative analysis, , but also that some of those theories are parallel to classical theories of strength .

The highlight of Thierry Coquand and Henri Lombardis Some Remarks about Normal Rings is a constructive proof that if a commutative ring R is normal, then so is the polynomial ring R [ X ]; this is based on a special technique to replace the use of minimal primes by explicit localizations in a suitable tree.

In On Sets of Premises Kosta Doen sheds light fromcategorial proof theory on the phenomenon that when collecting premises into (multi)sets rather than sequences one might have to face the unwanted consequence that any two deductions with the same premises and the same conclusions would be identified.

Hajime Ishihara and Takako Nemoto in Non-Deterministic Inductive Definitions and Fullness prove that a special form of non-deterministic inductive definition is tantamount to the principle of fullness characteristic of constructive ZermeloFraenkel set theory as a constructive version of the power set axiom.

In Cyclic Proofs for Linear Temporal Logic Ioannis Kokkinis and Thomas Studer establish weakening for annotated sequents by purely syntactical methods, and thus solve an open problem that Brnnler and Lange have brought up in the proof theory of temporal logic.

The main achievement of Roman Kuznetss paper Craig Interpolation via Hypersequents is a novel constructive method of proving the Craig interpolation property based on cut-free hypersequent calculi; he tests the method by verifying that property for the modal logic S5.

With A General View on Normal Form Theorems for ukasiewicz logic with product Serafina Lapenta and Ioana Leutean explore the connection between the PierceBirkhoff conjecture and ukasiewicz logic with product, the models of which reflect an algebraic hierarchy of lattice-ordered structures, from groups to algebras.

In Maria Emilia Maietti and Giuseppe Rosolinis Relating Quotient Completions via Categorical Logic the authors show that the elementary quotient completion of an elementary existential doctrine coincides with an exact completion when a choice rule holds in the starting existential elementary doctrine.

Roman Murawskis Some Historical, Philosophical and Methodological Remarks on Proof in Mathematics is about task and meaning of proof in mathematics, including discussions of the role of informal proofs in mathematical research practice, of the concept of formal proof, and of the distinction between provability and truth.

In Cut Elimination in Sequent Calculi with Implicit Contraction, with a conjecture on the origin of Gentzens altitude line construction Sara Negri and Jan von Plato settle the issue that standard cut elimination fails if the principal formula of a rule occurs in a premiss, and adapt this to sequent calculi with multisets and contraction.

While one objective of Hilberts Programme, finitistic consistency proofs, has been dashed by Gdels second incompleteness theorem, in Hilberts Programme and Ordinal Analysis Wolfram Pohlers argues that ordinal analysis not only helps to the other objectivethe elimination of ideal elementsbut is actually based on it.

In Aristotles Deductive Logic: a Proof-Theoretical Study Jan von Plato shows that derivations based on Aristotles rules of proof can so be transformed that the method of indirect proof is invoked at most once as a last step, which is the only way in whichas the author claimsAristotle used indirect proof.

Michael Rathjens Remarks on Barrs Theorem: Proofs in Geometric Theories gives a constructive proof of Gentzens Hauptsatz for logic which entails in a simple way the so-called Barr theorem that in geometric logic classical and intuitionistic provability coincide; also the Axiom of Choice is put into context.

Acknowledgment: First and foremost the editors of this volume would like to express their gratitude to the Alexander-von-Humboldt Foundation for offering the patronage of the Humboldt-Kolleg Proof and for generously giving financial support. Open-handed financial assistance further came from the following institutions: Burgergemeinde Bern, Deutsche Vereinigung fr Mathematische Logik und fr Grundlagenforschung der Exakten Wissenschaften, the Logic and Theory Group at the Institute of Computer Science of the University of Bern, Swiss National Science Foundation, Swiss Academy of Science, and Swiss Society for Logic and Philosophy of Science.

When co-editing this volume the second editor received individual funding by the Alexander-von-Humboldt Foundation, in the form of a Further Research Fellowship which he spent at the Munich Center for Mathematical Philosophy upon kind invitation by Hannes Leitgeb; and by the John Templeton Foundation within the project Abstract Mathematics for Actual Computation: Hilberts Program in the 21st Century.