Метатеорема

Метатеорема — логическое утверждение о формальной системе, доказанное на метаязыке. В отличие от теорем, доказанных в рамках данной формальной системы, метатеорема доказывается в рамках метатеории и может ссылаться на понятия, которые присутствуют в метатеории, но не в теории объектов^[англ.].^[1][2]

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

Примеры

Примеры метатеорем включают:

• Теорема дедукции для логики первого порядка гласит, что предложение вида ${\displaystyle \varphi \rightarrow \psi }$ доказуемо из набора аксиом "A" тогда и только тогда, когда предложение ${\displaystyle \psi }$ доказуемо из системы, аксиомы которой состоят из ${\displaystyle \varphi }$ и всех аксиом "A".
• Теорема о существовании классов теории множеств фон Неймана–Бернейса–Геделя гласит, что для каждой формулы, кванторы которой варьируются только по множествам, существует класс, состоящий из множеств, удовлетворяющих формуле.
• Доказательства непротиворечивости таких систем, как арифметика Пеано.

См. также

• Метаматематика
• Различие между использованием и упоминанием