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