Saturday, July 6, 2013

Technical resources

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."


Type theories

Automated Theorem Proving, Proof Assistants, etc.