Доказуемое и недоказуемое - Манин Ю.И.
Скачать (прямая ссылка):
б) Если в выражении Е есть скобки, но не существует скобочной биекции между открывающими и закрывающими скобками, то Е не является ни термом, ни формулой.
в) Пусть в Е есть скобки и скобочная биекция между ними.
(см. § 2 гл. I). Конечные последовательности элементов А суп тогда ? либо однозначно представляется в одном из девяти видов: выражения этого языка. Некоторые выражения были отмечень (^ — операция); р{Ео) (р — отношение);
как формулы или термы.
Напомним, что из определений § 2 гл. I вытекает следующее
а) любой терм языка Ь является либо константой, либо пере менной, либо представляется в виде /(Ц ..., и), где { — операцш ранга г, а /1, ..., К — термы меньшей длины;
б) любая формула языка Ь представляется либо в вид р(1 ь ..., и), где р—отношение ранга г; и, ..., К — термы мень шей длины, либо в одном из семи видов:
(Р)—ДО), (Р)~*(0), (Р)У(0),
(Р) А (<2). 1 (Р), Vх (р)> 3х (Р)>
где Р, С} — формулы меньшей длины; х — переменная.
Отсюда индукцией по длине получается такой результат: есл\ выражение Е является термом или формулой, то между множест вом П+ номеров открывающих скобок в нем и множеством П- но
26
(Е1)^(Е2); (Р,)-*(?*); (А)У(А);
(^)А(^); 1 (А); чх (Е»); н-*(А).
либо не является ни термом, ни формулой. Подразумевается, что выписанные пары скобок связаны единственной скобочной биекцией, по предположению существующей в Е: это и обеспечивает однозначность. В самом деле, вид <((Е0) получается, если первый элемент выражения есть операция, второй—скобка ( , а послед-
ний— парная ей скобка), и только в этом случае, и т. д.
Таким образом, мы свели задачу к синтаксическому анализу выражений меньшей длины Е0, Еи Е2, Е3, Это почти завершает описание алгоритма, потому что относительно Еи Е2, Е3 нужно выяснить, являются ли они формулами. Однако относительно Еа нужно выяснить, является ли это выражение соединением термов в надлежащем числе и однозначно ли это представление.
27
Ответ положителен. Следующий рецепт позволяет последова тельно отделять слева термы в соединении термов.
г) Пусть Е0 — некоторое выражение, между скобками котэрого есть скобочная биекция. Если представление Е0 в виде фЕ'о, где t — терм, существует, то оно однозначно.
Действительно, До либо однозначно представляется в одном иа видов:
хЕ'о, сЕ'о, [{Е"0)Е'о
(х — переменная, с— константа, —операция, скобки связаны единственной скобочной биекцией в ?0), либо вообще не пред ставляется в виде tE'o, где t — терм.
В случаях Е=хЕ'а или сЕ'0 это, очевидно, единственный способ отщепить терм слева. В случае Д0=/(Д"о)Д/о вопрос сводится к анализу того, является ли Е"0 соединением термов в количестве ранг /. Индукция по длине Д0 позволяет предположить, что ответ либо отрицателен, либо положителен и тогда Е"0 разлагается в со-единении термов однозначно. Лемма доказана.
Упражнение: сформулировать и доказать лемму об одно значном чтении для «бесскобочного» диалекта 3?и описанного в гл. I «Отступление о синтаксисе», п. 2а.
Вот первые индуктивные рассуждения, описывающие противопоставление свободных и связанных вхождений переменной в тер мы и формулы. Корректность следующих определений обеспечивается леммой 1.4.
1.5. Определение.
а) Всякое вхождение переменной в атомарную формулу или терм свободно.
б) Всякое вхождение переменной в ~| (Р) или в (?\)^<(Л2) №~ любая связка) свободно (соответственно связано) в точности тог да, когда свободно (соответственно связано) соответствующее вхождение в Р, или Р2.
в) Всякое вхождение переменной х в чх (Р) и дх(Р) связано Вхождения остальных переменных в ух{Р) и дх(Д) таковы же как соответствующие вхождения в Р.
Пусть дано вхождение квантора у (или д) в формулу Р. И:
определений следует, что вслед за ним в Р входит переменная и открывающая скобка. Выражение, начинающееся с этой переменной и кончающееся соответствующей закрывающей скобкой, назы вается областью действия данного (вхождения) квантора.
1.6. Определение.
Пусть дана формула Р, свободное вхождение переменной х в Р и терм и Мы говорим, что данное вхождение х не связывает Ъ в Р, если оно не лежит в области действия ни одного квантора вида д у или у у, где у — переменная, входящая в /.
28
Иными словами, после подстановки ( вместо данного вхождения х все переменные, входящие в t, останутся свободными в Р.
Чаще всего приходится подставлять терм вместо каждого из свободных вхождений данной переменной. Важно, что такая операция переводит термы в термы и формулы в формулы (индукция по длине). Если каждое свободное вхождение х в Р не связывает I, мы будем говорить просто, что х не связывает Ъ в Р.
1.7. Работать с определениями 1.5 и 1.6 мы начнем в следующем параграфе. Здесь ограничимся некоторыми интуитивными "пояснениями.
Определение 1.5 позволяет ввести важный класс замкнутых формул. По определению, это — формулы без свободных переменных (их называют еще суждениями). Интуитивный смысл понятия замкнутой формулы таков. Оно отвечает вполне определенному (в частности, в отношении истинности или ложности) высказыванию: имена неопределенных объектов теории используются только в контексте «все объекты х удовлетворяют условию ...» или «существует объект у со свойством ...». Наоборот, незамкнутая формула хег/ или д х (хег/) может быть истинной или ложной в зависимости от того, какие множества нарекаются именами х, у (для первой); у (для второй). Истинность или ложность понимаются здесь для фиксированной интерпретации языка, как это будет объяснено в § 2.
