Я, возможно, неправильно сформулировал - в этой статье рассматриваются теории с сигнатурой анализа, а я имел в виду (довольно тривиальное) утверждение, что теорему "непрерывная на отрезке функция достигает своего максимума" можно преобразовать в утверждение в сигнатуре
- "для любого множества
, такого что на нем выполнены нужные аксиомы, для любого множества
, являющегося непрерывной функцией
,
", и вывести получившееся утверждение из аксиом
. Разумеется, получившийся текст будет нечитаем и мало кому нужен.
(а утверждение "что-то там выводится в таком-то исчислении" для всех используемых на практике исчислений вообще формулируется и доказывается [если истинно] даже в арифметике)