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

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

Примеры

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

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

См. также

• Метаматематика

Примечания

Ссылки

• (1969), Metalogic .
• Alasdair Urquhart (2002), "Metatheory", A companion to philosophical logic , Dale Jacquette (ed.), p. 307

Внешние ссылки

• Barile, Margherita. (англ.) на сайте Wolfram MathWorld .