Но притом там будет разница, если взять классическую логику?
(Оффтоп)
Странно, что Вы помещаете вопрос в офтоп. Обычно это подразумевает отсутствие необходимости развития дискуссии во избежание ухода от темы, т.е. ответа Вы, вроде как, не ждёте... Несколько сбивает с толку. Всё же постараюсь ответить, стараясь не слишком далеко уходить от темы.
Разница не столько в заложенных в логику аксиомах, сколько в подходах к интерпретациям. Понятно, что с формальной точки зрения доказательство всегда базируется на некоторой аксиоматике. Вопрос в том, насколько с нашей точки зрения добавляется или убавляется убедительности доказательству в случае добавления дополнительных аксиом существования. В языке всегда можно сформулировать утверждение о существовании какого-нибудь очередного "чайника Рассела". Подход BHK-интерпретации таков, что пока оный чайник явно не предъявлен, утверждать его существование неправомерно. Подход же классической логики таков, что интерпретация обязана трактовать это утверждение либо как истинное, либо как ложное. Можно, конечно, заложить как аксиому несуществование, но в такой ситуации классический математик скорее склонен сказать, что существует всё, что он способен непротиворечиво вообразить (в смысле, что оно существует хотя бы в его воображении
). Это в полной мере относится и к существованию разного рода бесконечных множеств.
(В арифметике Пеано речь идёт только о подмножествах
, и выражаются они кодами соответствующих формул, или имелось в виду что-то другое?)
В арифметике первого порядка, строго говоря, речь идёт только о натуральных числах. Ни о каких "множествах" она вообще-то ничего сказать не может. Это выражается в том, что формула арифметики первого порядка может интерпретироваться совершенно разными множествами. Арифметика второго порядка, конечно, совсем другое дело.