Invariance axioms for realizability

Invariance axioms for realizability

Helmut Schwichtenberg
Ludwig-Maximilians-Universität München
Date: 
2016/08/25 (Thu) 13:30 to 15:10
Place: 
JAIST, Lecture room I2
Group: 
Logic Unit
Core2Core

Kolmogorov (1932) proposed to consider mathematical formulas as problems asking for solutions. Following this idea it seems reasonable to extend arithmetical theories by adding invariance axioms, which state that every formula is equivalent to the (internal) formula stating that it has a realizer. We sketch such a theory, which in addition allows to fine-tune the computational content of proofs by decorations of the logical connectives. A soundness theorem holds.

コンタクト
ishihara`at`jaist.ac.jp