Л.Я. Карпова) О НОРМАЛЬНЫХ ВЫВОДАХ В АРИФМЕТИКЕ И ПРОБЛЕМЕ ПРОТИВОРЕЧИВОСТИ – 1 В статье вводится понятие нормализации вывода для формальной арифметики (обобщающее соответствующее понятие для исчислений Правица [1]) и обрисованы подходы к доказательству нормализации и слабой нормализации. <...> Нормализация выводов позволяет доказать ряд важных свойств арифметической системы, имеющих прямое отношение к исследованию вопроса о возможной противоречивости арифметики. <...> Отметим, что в работах [2-8] исследование проблемы противоречивости было выполнено применительно к теории множеств ZFC. <...> Будем использовать формальную систему натурального вывода Правица [1] в ее интуиционистском варианте. <...> При этом термы не могут содержать переменных, а формулы не могут содержать переменных свободно (все вхождения переменных в формулу являются, таким образом, связанными, а все вхождения параметров свободными). <...> Областью действия кванторов , в формуле являются переменные, но если говорить о генетическом построении формулы, то надо иметь в виду, что в ходе построения могут делаться замены некоторых вхождений параметров на вхождения переменных. <...> Так если имеется формула A A( )a , то, применив квантор , можно получить формулу a xAx , где a Ax – псевдоформула, получаемая из формулы A в результате подстановки переменной x вместо всех вхождений параметра a (а ax Axb есть результат последовательной подстановки x вместо a и b вместо x ). <...> В системе Правица вводятся такие логические константы: пропозициональные связки &, , , кванторы , и пропозициональная константа для ложности (абсурда) (A B)&(B A ) . исключением . <...> Также определяемым является символ тождества «»: для отрицания «» является определяемым: по определению A есть формула A A B есть формула Степенью формулы называют A называют число вхождений логических констант (за ) в нее. <...> Вывод формулируется в виде дерева формул, в котором заключения правил заключения расположены <...>