Аннотация:
В докладе будет рассмотрена формальная арифметики на базе логики без сокращения,
т.е. логики, в которой не для всякой формулы $A$ из "$A$ или $A$" следует $A$.
Мы опишем основные свойства данной системы и поймем, почему для неё выполняется вторая теорема Гёделя о неполноте, несмотря на то, что стандартное доказательство второй теоремы Гёделя использует правило сокращения.