(1) определение «несуществующего» терма, т.е. такого терма
,
что формула
не выводима в рассматриваемой теории;
Это получается вроде введения новых аксиом. Не, я такого не допускаю. Я имел ввиду именно введение сокращенных записей. То есть существенно нового (формально) ничего не должно получатся.
Не-не, ни в коем случае! Никаких «новых аксиом» и ничего «существенно нового»! Иначе это уже будут не «определения». К примеру, введение терма

вовсе не предполагает какое-либо изменение аксиоматики. Мы всего лишь расширяем синтаксис новым термом

и используем его наряду со старыми термами самым обычным образом, подразумевая семантику

. При этом формула, содержащая новый терм, считается теоремой в том и только том случае, когда теоремой является ее перевод на исходный язык. В этом смысле ничего «существенно нового» не появляется. Например, формула

является теоремой, так как ее перевод имеет вид

и, разумеется, доказуем.
Кстати, работая в ZFC, бывает очень удобно перемещать аксиому экстенсиональности на уровень синтаксиса и считать формулу

(где

и

— термы) сокращением формулы

. Кое-кто так и поступает. Это действительно удобный прием, так как он приводит к существенной технической экономии (за счет упрощения сигнатуры и сокращения множеств атомарных формул, аксиом и правил вывода), тем не менее сохраняя в неизменном виде множество теорем. При таком подходе, например, формула

теоремой не является. Более того, теоремой является ее отрицание

: действительно, перевод этой формулы с учетом сокращения

имеет вид

или, что эквивалентно,

, а последнее доказуемо в ZFC.
Такой немного философский вопрос: чего же мы достигаем введением новых понятий? Неужели только лишь сокращения записи? Или в этом есть и более глубокий смысл?
Как я уже говорил, в большинстве случаев это всего лишь сокращение. Случай

— это на самом деле тоже сокращение, но не сводящееся к добавлению определимой (по Бету) константы. А вот

— это уже не просто сокращение. Это, если угодно, схема сокращений: каждая формула вида

является сокращением соответствующей формулы, получаемой из

в результате применения алгоритма перевода, раскрывающего рекурсию по сложности

. Но если отвлечься от такого рода нюансов и придать термину «сокращение» более общий смысл, — считая раскрытие сокращения алгоритмом перевода формулы с расширенного языка на исходный, — то всякое определение является сокращением. Никакого более глубоко смысла тут нет. И это хорошо, ибо согласуется с интуитивным пониманием определения как введения новой записи для какого-либо утверждения или терма. Чистой воды прагматизм и никакой философии.
AGu, а вот скажем аксиома пустого множества или аксиома бесконечности тянут на первый случай, да?
Нет, так как аксиома — это не определение. Упоминая аксиому пустого множества, Вы, возможно, имели в виду определение пустого множества, т.е. расширение синтаксиса термом

с семантикой

. Это уже определение, но оно все равно не относится к случаю (1), так как формула

является теоремой, т.е. мы вводим «существующий» терм. (Что же касается аксиомы бесконечности, то тут я даже отдаленной аналогии с определением не вижу.)