Метатеорема

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

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