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.
