Теория формальных систем

[djuuj]

Изучая мат. логику, формализованное исчисление высказываний, предикатов, возник такие вот вопросы. Есть так называемое "определение" формальной системы:
Формальная система определена, если:
П.1. Задан конечный алфавит (конечное множество символов).
П.2. Определена процедура построения правильных слов (формул).
П.3. Выделено множество слов, называемых аксиомами.
П.4. Задано множество правил вывода, которые позволяют из множества аксиом получать новые формулы. Правило вывода в общем случае имеет вид: A1 и A2 и ... An –> B1 и B2 и ... Bm, где Ai и Bj – формулы, «–>» читается как «влечет».
Но ведь раз это определение, то оно сформулировано в некоторой формальной системе! Порочный круг? Да ещё и в нём фигурируют термины теории множеств! Естественно возникает вопрос: а является ли аксоиматическая теория множеств формальной системой? И в терминах какой формальной системы тогда можно разъяснить, что значит непротиворечивость (доказанная! а раз доказанная, то в некоторой формальной системе) исчисления высказываний, предикатов?
Может кто-то может посоветовать литературу по теории формальных систем?

[Xaositect]

Есть понятие метатеории: У нас есть некоторая формальная система - теория, которую мы изучаем, и есть метатеория, в которой мы изучаем теорию.
Обычно, чтобы сильно не заморачиваться, в метатеории есть достаточно сильные понятия, вроде понятия множества, но иногда нужно, чтобы теория была достаточно бедной. Метатеория может даже быть той же самой, что и теория, то есть теорию иногда можно формализовать внутри ее самой. Примером такого подхода может служить доказательство теоремы Геделя о неполноте.
Теорию формальных систем тоже можно представить как формальную систему - обычно считается, что множество аксиом рекурсивно перечислимо, а правила вывода рекурсивны, так что их можно описать конструктивно в виде строк и оперируя со строками определить отношение "формула F выводима в формальной системе S". И опять же, можно изучать получившуюся формальную систему (теорию рекурсивно-перечислимых множеств) внутри ее самой.

Насчет литературы - есть фундаментальная книга Клини "Введение в метаматематику".

[djuuj]

Спасибо большое, разобрался!