Алгебра доказуемости и разреженная топология

Лев Беклемишев

В докладе рассмотрены два класса объектов, имеющих различную природу, но неожиданным образом аналогичные по своим свойствам. С одной стороны, так называемые алгебры доказуемости, возникающие при изучении свойств формальной доказуемости в арифметических теориях. С другой стороны, топологические пространства, наделённые одной или несколькими разреженными топологиями, то есть такими, что любое непустое подмножество $X$ имеет хотя бы одну изолированную точку.

Алгебра доказуемости формальной арифметической теории $T$ представляет собой булеву алгебру Линденбаума для $T$ , расширенную оператором $D_0:L\to L$ , сопоставляющим любому предложению $A$ гёделевское предложение, выражающее непротиворечивость теории $T+A$ . Ее естественным обобщением является алгебра, в которой наряду с оператором $D_0$ рассматриваются операторы $n$ -непротиворечивости $D_n$ , выражающие истинность всех доказуемых в $T+A$ предложений с $n$ переменами кванторов.

Операторы $D_0,D_1,\dots$ могут интерпретироваться как операторы на алгебре всех подмножеств данного множества $X$ . Оказывается, что в случае, когда на алгебре множеств выполнены все тождества алгебры доказуемости, каждый из этих операторов естественным образом определяет некоторую разреженную топологию на $X$ , для которой $D_n(A)$ есть множество всех предельных точек множества $A$ .

В докладе рассмотрены свойства соответствующих политопологических пространств и их связи с вопросами из теории доказательств, в частности вопрос о полноте топологических пространств относительно системы тождеств алгебр доказуемости.

Беклемишев Лев Дмитриевич, доктор физико-математических наук, член-корреспондент РАН.

Традиционная новогодняя сессия МИАН-ПОМИ, 2009 «Логика и теоретическая информатика», г. Москва
17 декабря 2009 г.

Комментарии: 0

Похожее

Алгебры доказуемости

Лев Беклемишев

Аксиоматические системы, такие как арифметика Пеано и ее фрагменты, являются традиционными объектами изучения в математической логике. В докладе будет рассказано о сравнительно новом подходе к изучению таких систем с алгебраической точки зрения. Будут описаны алгебраические структуры, возникающие при изучении формальной доказуемости, и приведены некоторые применения этих структур к вопросу о порядках роста вычислимых функций для фрагментов арифметики и к построению простых утверждений комбинаторного характера, независимых от аксиом арифметики Пеано. Также будет рассказано о топологической точке зрения на алгебры доказуемости, которая приводит к изучению некоторого интересного класса пространств.
Математика, метаматематика и истина

Янов Ю. И.

В связи с разными точками зрения на природу математики рассматриваются вопросы о метаматематическом понятии истины и возможности убедительного доказательства истинности математических теорем.
Доказательность в математике

Юрий Ершов

Программа Гордона

Доказательность — главнейшая особенность математики, науки, представляющей образцы точности рассуждений. Но понятие доказательства долгое время не имело точного математического определения. О парадоксах в теории множеств и основаниях математики — академик РАН Юрий Ершов.
Аксиоматический метод

Беклемишев Лев

В чем заключается аксиоматический метод? Как развивалось понятие аксиомы? Кем был разработан аксиоматический метод? Какое место он занимает в математике? И какой критике подвергается этот метод? Математик Лев Беклемишев о неевклидовой геометрии, системе аксиом Гильберта и смысле в математике.
Доказуемо рекурсивные функции

Лев Беклемишев

Вычислимая функция f:N→N называется доказуемо рекурсивной в данной формальной теории T, если существует алгоритм её вычисления такой, что в T можно доказать утверждение «для любого x существует y такой, что f(x)=y». В математической логике такие функции изучаются по двум причинам. Во-первых, для данной программы нас часто интересует доказательство её корректности, в частности вопрос о том, завершает ли она работу при любых исходных данных. С другой стороны, варьируя функцию f мы можем ставить для теории T сколь угодно сложные (вплоть до невыполнимости) задачи на доказательство. Тем самым, доказуемо рекурсивные функции могут быть использованы для изучения различных формальных теорий. Такой подход приводит к наиболее впечатляющим на сегодняшний день примерам недоказуемых комбинаторных утверждений. Мы начнем с понятия машины Тьюринга и вычислимой функции. Разберемся, как формальная арифметика может говорить о вычислениях. Поймем, что для любых разумных систем аксиом T их запас доказуемо рекурсивных функций никак не может исчерпывать все вычислимые всюду определенные функции. Отсюда выведем первую теорему Гёделя о неполноте.
Доказуемость и модальная логика

Лев Беклемишев

Классическая логика высказываний исходит из предположения о том, что любые высказывания либо истинны, либо ложны. Логика доказуемости отражает более глубокую картину мира, осознанную после теорем Гёделя о неполноте: истинность высказывания, вообще говоря, не равносильна его доказуемости. Можно ли — и если да, то как — говорить на уровне логики о доказуемости или недоказуемости высказываний, наряду с их истинностью или ложностью? Программа: Логика высказываний и её модели. Модальная логика, модели Крипке. Логика Гёделя-Лёба GL. Теорема о полноте логики GL по Крипке на конечных деревьях. Формальная арифметика Пеано. Гёделева нумерация. Теорема о неподвижной точке. Формулы доказуемости и непротиворечивости. Теоремы Гёделя, Россера и Лёба. Доказуемость как модальность: арифметическая интерпретация логики GL. Замкнутые модальные формулы, последовательность Тьюринга, локальная рефлексия. Существование и единственность модально определимых неподвижных точек (теорема де Йонга).
Компьютерные доказательства

Лев Беклемишев

Какую часть математических доказательств можно поручить компьютеру? Какие существуют виды интерактивных систем поиска математических доказательств? В чем заключается теорема о четырех красках? И как она была доказана? Математик Лев Беклемишев о теории множеств, интерактивных системах и проблеме о четырех красок.
Доказательства невозможности в математической логике и теории алгоритмов

Алексей Семёнов

Попытки дать математические определения понятий формального доказательства, истинности, формализованной деятельности по инструкции привели к построению математической логики и теории алгоритмов — области математики, результаты которой сформировали и продолжают формировать основы информатики и влиять на практическое использование цифровых технологий. Важнейшие результаты данной области, наряду с указанными определениями — это результаты о невозможности, в свою очередь тесно связанные с результатами об универсальности и диагональными конструкциями.
Элементарная геометрия с точки зрения логики

Лев Беклемишев

Разные варианты выбора неопределяемых понятий. Система аксиом Тарского (по-видимому, самая простая из известных). Роль аксиом непрерывности с точки зрения различия логики первого и второго порядков. Модели и синтаксические интерпретации формальных теорий. Несколько классических интерпретаций, в том числе взаимная интерпретируемость гиперболической и евклидовой геометрии, элементарной геометрии Тарского и элементарной теории поля вещественных чисел, интерпретация теории поля вещественных чисел в арифметике натуральных чисел. Теоремы Тарского о полноте аксиоматики и о существовании алгоритма, распознающего истинность утверждений элементарной геометрии.
Куда движется математика?

Брайан Дэвис

На протяжении большей части XX столетия в «чистой» математике царило замечательное единодушие относительно того, как нужно представлять результаты. Весь предмет сводился к комплексу теорем, каждая из которых, в конечном счете, выводилась из фиксированного набора аксиом путем так называемого строгого логического доказательства. В отдельных разделах математики, таких, например, как арифметика Пеано, справедливость аксиоматики выглядела самоочевидной, однако во многих случаях аксиомы попросту очерчивали рассматриваемую область вопросов. Для математиков, если только они не выходили за рамки математики, выступая в роли философов-любителей, принципиального различия между изобретением и открытием новых концепций не было.

Далее >>>

∀ x, y, z

Алгебра доказуемости и разреженная топология

Лев Беклемишев

Теги

Похожее