Я всё ещё не понимаю: это вывод или это определение "истинности"? И причём тут равенства без переменных? Если Вы уверены в непротиворечивости аксиом и из них следует утверждение о несуществовании, то можете спокойно считать это утверждение истинным.
Вывод, конечно. А равенства без переменных (без связанных и без свободных, типа

или

) при том, что доказуемость всех тех равенств из них, которые истинны используется в этом выводе. Система аксиом может быть непротиворечива и утверждение о несуществовании натуральных решений уравнения

доказуемым в ней, но это утверждение не является истинным.
Цитата:
Я всё ещё не понимаю какой смысл Вы вкладываете в понятие истинности. Утверждение о существовании чётного нечётного совершенного числа истинно или нет?
Я не знаю, истинно это утверждение или нет, и это неважно для понимания его смысла и того, что оно либо истинно, либо ложно. Что касается смысла понятия истинности, то я вкладываю в это понятие тот же смысл, какой вкладывал Гёдель, когда утверждал, что его предложение

недоказуемо, но истинно (при условии непротиворечивости системы аксиом) и Тарский, когда утверждал, что арифметическая истина невыразима (в отличие от доказуемости, которая выразима).
Цитата:
А ЧТО проверяемо? "Равенства без переменных" типа

или

проверяемы именно путём построения доказательства (или опровержения) в аксиоматике Пеано.
Для проверки таких равенств, существует алгоритм, который не зависит от той или иной системы аксиом.
Этот алгоритм сложения и умножения в столбик учат в начальных классах.
Цитата:
Но есть высказывания арифметики, которые пока не удалось доказать или опровергнуть. Они "проверямы" или нет? Короче: Как Вы определяете проверяемость?
Я говорил о "проверяемости" "равенств без переменных" в том смысле, что существует алгоритм их проверки. У нас нет метода проверки более сложных утверждений, таких как несуществование решений диофантовых уравнений. Поэтому мы доказываем эти утверждения в той или иной системе аксиом, о которой мы верим, что она непротиворечива. Однако, не следует путать доказуемость в некоторой системе аксиом с истинностью.