Метатеорема - Metatheorem
В логике , метатеорема является утверждение о формальной системе испытанной в метаязыке . В отличие от теорем, доказываемых в рамках данной формальной системы, метатеорема доказывается в рамках метатеории и может ссылаться на концепции, которые присутствуют в метатеории, но не в теории объекта .
Формальная система определяется формальным языком и дедуктивной системой ( аксиомы и правила вывода ). Формальная система может использоваться для доказательства конкретных предложений формального языка с помощью этой системы. Однако метатеоремы доказываются извне по отношению к рассматриваемой системе, в ее метатеории. Общие метатеории, используемые в логике, - это теория множеств (особенно в теории моделей ) и примитивная рекурсивная арифметика (особенно в теории доказательств ). Вместо того, чтобы демонстрировать доказуемость конкретных предложений, метатеоремы могут показать, что каждое из широкого класса предложений может быть доказано, или показать, что определенные предложения не могут быть доказаны.
Примеры
Примеры метатеорем включают:
- Теорема дедукции для логики первого порядка говорит о том , что предложение формы φ → ф доказуемо из набора аксиом А , если и только если предложение ψ выводима из системы , чьи аксиомы состоят из ф и все аксиомы А .
- Теорема класс существования из теории множеств фон Неймана-Bernays-Гёделя утверждает , что для каждой формулы которой кванторы варьируются только над множествами, есть класс , состоящий из множеств , удовлетворяющих формуле.
- Доказательства непротиворечивости таких систем, как арифметика Пеано .
Смотрите также
Ссылки
- Джеффри Хантер (1969), Metalogic .
- Аласдер Уркхарт (2002), «Метатеория», спутник философской логики , Дейл Жакетт (ред.), Стр. 307
внешние ссылки
- Мета-теорема в энциклопедии математики
- Бариле, Маргарита. «Метатеорема» . MathWorld .