Верещагин Н.К., Шень А. - Языки и исчисления (1076783), страница 13
Текст из файла (страница 13)
Отметим, что добавление правила сечения не нарушает корректности, как легко проверить, и не может нарушить полноты.Задачи о поиске вывода и анализе его структуры, хотя и были одно время модными в связи с «искусственным интеллектом»,представляют большой интерес, и про них есть целая наука, в которой исчисления генценовского типа играют центральную роль. Мырассмотрели один из вариантов исчисления секвенций для классического исчисления высказываний; бывают исчисления для интуиционистских и модальных логик, для исчисления предикатов и т.
д. Исходной мотивацией для рассмотрения такого рода исчислений было58Исчисление высказываний[гл. 2]желание доказать непротиворечивость арифметики. Согласно знаменитой второй теореме Гёделя о неполноте без дополнительных аксиом этого сделать нельзя, но если принять схему аксиом для трансфинитной индукции по ординалу ε0 , это удаётся сделать, как показалГенцен.2.4. Интуиционистская пропозициональная логикаИсключим из числа аксиом закон исключённого третьего A ∨ ¬A.Полученное исчисление называют интуиционистским исчислениемвысказываний. (Обычное исчисление высказываний называют классическим, чтобы избежать путаницы при его сравнении с интуиционистским.
Вообще математические рассуждения, опирающиеся нааксиому исключённого третьего, называют «классическими», а избегающие её — «интуиционистскими».)Конечно, немедленно возникают естественные вопросы. Почемуименно эта аксиома вызывает сомнения? Вообще-то аксиом много,и можно было бы исключить любую и смотреть, что получится безнеё — но ясно, что скорее всего получится что-то странное.
Как понять, какие формулы останутся теоремами без закона исключённого третьего? Раньше у исчисления высказываний была «сверхзадача» — вывести все тавтологии и только их, а теперь?Интуиционистская логика возникла как попытка (сделанная Гейтингом) формализовать (хотя бы частично) методы рассуждений,практикуемые в «интуиционистской математике». Голландский математик Брауэр широко известен как автор классической (во всехсмыслах) теоремы Брауэра о неподвижной точке (она утверждает,что любое непрерывное отображение многомерного шара Dn в себя имеет неподвижную точку).
Но одновременно он создал целуюшколу в области оснований математики — математический интуиционизм. Отчего, спрашивал Брауэр, в теории множеств возниклипарадоксы? Можно считать, что это оттого, что мы стали рассуждать о каких-то уж очень абстрактных объектах, которые существуют лишь в нашей (порой противоречивой) фантазии, так что следуетпроявлять осторожность и не подходить к опасной черте.
Но Брауэрпошел дальше, говоря, что противоречия лишь симптом болезни, анадо устранить её причину. Причину он видел в том, что математические рассуждения и понятия утратили интуитивный смысл, инужно вернуться к основам и пересмотреть смысл самих логическихсвязок.[п. 4]Интуиционистская пропозициональная логика59Что мы имеем в виду (или должны иметь в виду), говоря о том,что мы установили, что «A или B»? Это значит, по Брауэру, что либо мы установили A, либо установили B.
Когда мы устанавливаем,что «A и B», это значит, что мы установили и A, и B. «Если A, то B»означает, что мы располагаем каким-то общим рассуждением, которое позволит нам установить B, как только кто-то установит нам A.Отрицание A означает, что мы располагаем рассуждением, котороеприводит к противоречию предположение, что A установлено. (Какс точки зрения интуиционизма, так и с классической точки зрения,¬A во всех смыслах эквивалентно A →⊥, где ⊥ — заведомо ложноеутверждение. Можно было бы вообще не использовать отрицания, аиметь константу ⊥ — это не очень привычно, но технически удобно.)Интуиционизм отвергает идею о том, что все высказывания делятся на истинные и ложные (пусть неизвестным нам образом).
Сэтой точки зрения закон исключённого третьего совершенно безоснователен: A ∨ ¬A означает, что для произвольного утверждения A мыможем установить либо A, либо его отрицание (то есть объяснить,почему A в принципе не может быть установлено) — а почему, собственно?Обычно, говоря об интуиционизме, приводят следующий примеррассуждения, неприемлемого с точки зрения интуиционизма.
Докажем, что существуют иррациональные числа α и β, для которых√ √2αβ рационально. В самом деле, рассмотрим два случая. Если2√ √2√рационально, то можно положитьα = β = 2. Если же 2 ирра√ √2√ционально, то положим α = 2и β = 2; легко проверить, чтоαβ = 2. Интуиционист скажет, что это рассуждение некорректно: доказать существование чего-то означает построить этот объект, а мытак и не построили чисел α и β, поскольку не установили, какой издвух случаев имеет место.
(Заметим в скобках,что специалисты по√ √2алгебраической теории чисел знают, что 2 иррационально и даже трансцендентно. Кроме того, не нужнобыть специалистом, чтобы√заметить, что можно положить α = 2 и β = 2 log2 3.) Этот примерможно критиковать и с другой точки зрения, говоря, что само понятие действительного числа не является интуитивно ясным и требуетобоснования.Вообще интуиция — дело тонкое: если долго рассуждать, скажем,о действительных числах, то начинает казаться, что они в каком-тосмысле существуют независимо от наших рассуждений. Именно по-60Исчисление высказываний[гл. 2]этому психологически оправдан вопрос о том, скажем, как обстоятдела с континуум-гипотезой «на самом деле»: существует ли несчётное множество действительных чисел, не равномощное всем действительным числам, или не существует?Мы не будем говорить о философских предпосылках интуиционизма подробно.
Вкратце упрощённая история вопроса такова. Брауэр наметил планы переустройства математики на интуиционистскихпринципах и отстаивал их настолько горячо, что однажды Гильбертв раздражении заметил: отменить закон исключённого третьего —это всё равно что отнять у астрономов телескоп или запретить боксёрам пользоваться кулаками. Но, продолжал он, никто не можетизгнать математиков из рая, который создал Кантор.В планы Брауэра не входила формализация интуиционистскойлогики и математики, скорее наоборот.
Тем не менее анализ принципов интуиционизма пошёл именно по этому пути, когда Гейтинг стализучать пропозициональную логику без закона исключённого третьего. Различные спорные интуиционистские принципы стали предметом изучения с точки зрения формальной логики; были построены интуиционистские варианты формальной арифметики, теориимножеств, логики предикатов, а также генценовские варианты интуиционистских систем. Были предложены различные интерпретации интуиционистской логики. Колмогоров предложил трактоватьеё как «логику задач», Клини предложил понятие «реализуемости»,использующее теорию алгоритмов для толкования формул; былипредложены топологические модели для интуиционистской логикии т.
д. В СССР знамя Брауэра подхватила школа Маркова, написав на нём, впрочем, слово «конструктивизм» вместо идеологическисомнительного «интуиционионизма» и более последовательно ограничиваясь конечными объектами. Крипке в 1960-е годы предложилнекоторую семантику (определение истинности), согласованную синтуиционистским исчислением высказываний и весьма естественную (даже странно, что её не придумали раньше); замечательнымобразом оказалось, что она в некотором смысле близка к методуфорсинга, который примерно в это же время придумал Коэн, чтобы доказать независимость аксиомы выбора и континуум-гипотезыв теории множеств.Возвращаясь к интуиционистскому исчислению высказываний,приведём несколько выводимых формул.• Чтобы понять смысл формулы (A → B) → (¬B → ¬A), вспом-[п.
4]Интуиционистская пропозициональная логика61ним, что отрицание ¬X можно толковать как (X →⊥), где ⊥ —заведомо ложное утверждение. Эта формула говорит, что еслииз A следует B, а из B следует заведомо ложное утверждение, то из A следует заведомо ложное утверждение (частныйслучай транзитивности отношения следования). Вывод её неиспользует закона исключённого третьего. В самом деле, полемме о дедукции (доказательство которой остаётся тем же идля интуиционистского исчисления высказываний) достаточнодоказать, что из (A → B) и ¬B выводится ¬A. Для этого, всвою очередь, достаточно доказать, что из (A → B), ¬B и Aвыводятся две противоречащие друг другу формулы (что очевидно: это формулы B и ¬B).• Чтобы вывести формулу (A → ¬¬A), надо показать, что изA выводится ¬¬A, для чего достаточно из A и ¬A вывестидве противоречащие друг другу формулы (что тривиально —годятся сами формулы A и ¬A).• Формула (¬¬¬A → ¬A) получается из двух предыдущих: положим B равным ¬¬A в первой из них.• Формула (¬A → ¬¬¬A), с другой стороны, есть частный случай второй формулы, так что три отрицания равносильны одному.• Коммутативность и ассоциативность операций ∧ и ∨, так жекак и два свойства дистрибутивности, не опирались на законисключённого третьего.• По-прежнему ((A ∨ B) → C) равносильно ((A → C) ∧ (B →C)) (импликации в обе стороны, связывающие эти формулы,выводимы в интуиционистском исчислении высказываний).• Взяв ⊥ в качестве C в предыдущих формулах, мы видим, чтоодин из законов Де Моргана, ¬(A ∨ B) ↔ ¬A ∧ ¬B, не опирается на закон исключённого третьего (что легко проверить инепосредственно).• Формулу ¬¬(A ∨ ¬A) сохранившийся закон Де Моргана позволяет переписать в виде ¬(¬A ∧ ¬¬A), и нужно лишь вывестииз (¬A ∧ ¬¬A) две противоположные формулы, что очевидно.62Исчисление высказываний[гл.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
