First Steps towards Non-Classical Logic of Informal Provability - a podcast by MCMP Team

Rafal Urbaniak (Ghent) gives a talk at the MCMP Colloquium (29 October, 2015) titled "First Steps towards Non-Classical Logic of Informal Provability". Abstract: Mathematicians prove theorems in a semi-formal setting, providing what we'll call informal proofs.
There are various philosophical reasons not to reduce informal provability to formal provability within some appropriate axiomatic theory (see Marfori 2010, Leitgeb 2009). But the main worry is that we have a strong intuition that whatever is informally provable is true. So we seem committed to all instances of the so-called reflection schema: P(A) ->A (where P is the informal provability predicate). Yet, a sufficiently strong arithmetical theory T resulting from adding to PA (or any sufficiently strong arithmetic) all its instances for provability in T will be inconsistent. The main idea behind most of the current approaches (Shapiro 1985 Horsten 1994, Horsten1996} is to extend the language with a new informal provability predicate or operator, and include all instances of the reflection schema for it. Contradiction is avoided at the price of dropping one of the derivability conditions. Thus, various options regarding trade-offs between various principles which all seem convincing are studied. In order to overcome some of the resulting difficulties and arbitrariness we investigate the strategy which changes the underlying logic and treats informal provability as a partial notion, just like Kripke's theory of truth (Kripke 1975). Alas, no three-valued logic can do the job that K3 does for truth for informal provability. The main reason is that the value of a complex formula in those logics is always a function of the values of its components. This fails to capture the fact that, for instance, some informally provable disjunctions of mathematical claims have informally provable disjuncts, while some others don't. We develop a non-functional many-valued logic which avoids this problem and better captures our intuitions about informal provability. We describe the semantics of our logic and some of its properties. We argue that it does a better job when it comes to reasoning with informal provability predicate.

Further episodes of MCMP

Further podcasts by MCMP Team

Website of MCMP Team