Спирина, М.С. Дискретная математика

системой (теорией) Т. Строго говоря, непосредственная выводи­ мость и выводимость являются свойствами конкретной формаль­ ной системы Г, поэтому должны употребляться знаки [—г и f=r . Но в тех случаях, когда очевидно, о какой формальной системе идет речь, т.е. все выводы происходят в одной и той же формаль­ ной системе, указание на нее мы будем опускать и употреблять знаки |— и (=. Допустим, формальная система задана: выделены алфавит, множество формул, аксиомы и правила вывода. ? Как пользоваться построенной формальной системой? Во-первых, она должна быть понятной не только ее автору. Во-вторых, из нее должна сле­ довать некая конструктивная теория, в рамках которой можно делать что- то определенное. Например, мы хотим решать уравнения, формулировать и доказывать теоремы, вычислять выражения, причем не обязательно ма­ тематического характера, допустим, выводить законы генетики или социо­ логии. Очевидно, что нельзя универсально задать формальную тео­ рию. Так, определяя и объясняя ее, кроме алфавита самой теории был использован русский язык и язык теории множеств. В этом случае, когда мы вынуждены прибегать к другим знакам, их при­ дется брать из некоторой более общей теории — метатеории, пред­ метный язык которой называют метаязыком. Возникает проблема интерпретации полученных формул, пе­ ревода их на более доступный язык. Но любой перевод есть ото­ бражение слов из одного языка в другой, например английского в немецкий. Это языки над одним и тем же латинским алфавитом, но фонетическая транскрипция и лексическое значение слов раз­ личны. Итак, отображение х: F -» L называется интерпретацией формальной теории ( А , F, Р, R ) во множество содержательных высказываний метаязыка L. Метаязык должен содержать, помимо прочего, семантические характеристики высказываний, если та­ ковые имеются. В частности, мы сопоставляли истинным выска­ зываниям символ «1», а ложным — «О», т.е. эти элементы или слова «ложь», «истина» должны содержаться в метаязыке. Поскольку некоторые элементы L несут на себе семантическую характерис­ тику, это значит, что определено отображение v: L -> (истина, ложь}, которое отождествим со знакомым В - (0, 1}. Тогда автома­ тически определена суперпозиция v ° х: F -> В, ставящая в соот­ ветствие некоторым формулам их семантическую характеристику. Пусть/ € F. Тогда, если высказывание x ( f ) является истинным в смысле L (т.е. v ( jc ( / ) ) = 1), то считают, что формула/ выполняет­ ся в интерпретации х. Именно в конкретной интерпретации имеет смысл говорить об отрицании формулы. О формулах теории вообще можно судить прежде всего по ее аксиомам. 212