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