HoTT off the Presses!
This looks extremely cool: Homotopy Type Theory: Univalent Foundations of Mathematics from The Univalent Foundations Program Institute for Advanced Study. Free, in a variety of formats!
"The present book is intended as a first systematic exposition of the basics of univalent foundations, and a collection of examples of this new style of reasoning — but without requiring the reader to know or learn any formal logic, or to use any computer proof assistant. We believe that univalent foundations will eventually become a viable alternative to set theory as the “implicit foundation” for the unformalized mathematics done by most mathematicians."
Logical Consequence
- Etchemendy, John: The Concept of Logical Consequence. A detailed attack on Tarski's concept of logical consequence and the model theory it spawned: "[M]y claim is that Tarski's analysis is wrong, that his account of logical truth and logical consequence does not capture, or even come close to capturing, any pretheoretic conception of the logical properties...Applying the model -theoretic account of consequence, I calim, is no more reliable a technique for ferreting out the genuinely valid arguments of a language than is applying a purely syntactic definition."
- The Philosophy of Logical Consequence and Inference Special issue of Synthese Volume 187, Issue 3, August 2012
Proof-Theoretic Semantics
"Proof-Theoretic Semantics (PTS) is an alternative of model-theoretic (or truth-condition) semantics. It is based on the idea that the central notion in terms of which meanings are assigned to expressions is that of proof rather than truth. In this sense PTS is inferential rather than denotational in spirit." (P. Schroeder-Heister)- Proof-theoretic semantics from Stanford Encyclopedia of Philosophy
- Proof-Theoretic Semantics R. Kahle, P. Schroeder-Heister, editors Special issue of Synthese, 2005
- Schroeder-Heister, P. The categorical and the hypothetical: a critique of some fundamental assumptions of standard semantics (preprint) Abstract: "The hypothetical notion of consequence is normally understood as the transmission of a categorical notion from premisses to conclusion. In model-theoretic semantics this categorical notion is ‘truth’, in standard proof-theoretic semantics it is ‘canonical provability’. Three underlying dogmas, (I) the priority of the categorical over the hypothetical, (II) the transmission view of consequence, and (III) the identification of consequence and correctness of inference are criticized from an alternative view of proof-theoretic semantics. It is argued that consequence is a basic semantical concept which is directly governed by elementary reasoning principles such as definitional closure and definitional reflection, and not reduced to a categorical concept. This understanding of consequence allows in particular to deal with non-wellfounded phenomena as they arise from circular definitions."
Curry-Howard
- Curry-Howard Isomorphism (wikipedia)
- Lectures on the Curry-Howard Isomorphism (1998)
- Gallier, Jean: On the Correspondence Between Proofs and Lambda Terms
Type theories
- Hofmann, Martin: Syntax and Semantics of Dependent Types - "The main aim of this article is not so much to explain how to use dependent types to formalize constructive mathematics or to do program development and specification, but rather to introduce the reader to a tool for the metatheoretic study of dependent type theory: category-theoretic semantics."
- Schulman, Mike: In Praise of Dependent Types; From Set Theory to Type Theory
Automated Theorem Proving, Proof Assistants, etc.
- vdash
- Harrison, John: Formal Proof - Theory and Practice (PDF, AMS paper)
- Gallier, Jean: Logic for Computer Science: Foundations of Automatic Theorem Proving (free PDF)
- Coq proof assistant
- Pierce et al.: Software Foundations. Includes hands-on tutorial on Coq.
- Mondet, Sebastian: Coq programming with subsets "...intended for Coq beginners like me, i.e., people who have been learning with Software Foundations (or other) for some time and who want to program."
Misc
- AMS Special Issue on Formal Proof (Dec 2008)
- Tait, William: Truth and Proof: The Platonism of Mathematics - "The answer to the initial question of this paper, concerning the relation between truth and proof in mathematics, is that a proposition A is true when there is an object of type A and that a proof of it is the construction of such an object. That there is an object of type A is the 'fact' about, say, the system of numbers that A expresses. It is clear from this why proof is the ultimate warrant of truth... The Platonist view that truth is independent of what we know is entirely correct on this view."
-
People
- Gerhard Gentzen
- Arend Heyting
- Dag Prawitz
- Michael Dummet
- Solomon Fefferman
- Per Martin-Lof (intuitionistic type theory)
- Jean-Yves Girard - linear logic, proof nets (1986)
- Thierry Coquand & Gerard Huet
- Constructions: A higher order proof system for mechanizing mathematics (1985)
- Calculus of Constructions (1986)
- Peter Aczel
- Peter Schroeder-Heister
- Ruy de Queiroz
