Теорема Гёделя о неполноте и вторая теорема Гёделя — две теоремы математической логики о принципиальных ограничениях формальной арифметики и, как следствие, всякой формальной системы, в которой можно определить основные арифметические понятия: натуральные числа, 0, 1, сложение и умножение.
Первая теорема утверждает, что если формальная арифметика непротиворечива, то в ней существует невыводимая и неопровержимая формула.
Вторая теорема утверждает, что если формальная арифметика непротиворечива, то в ней невыводима формула, содержательно утверждающая непротиворечивость этой арифметики.
Обе эти теоремы были доказаны Куртом Гёделем в 1930 году (опубликованы в 1931) и имеют непосредственное отношение ко второй проблеме из знаменитого списка Гильберта.
Расшифровка видео
Предисловие
0:01
всем привет продолжим наш разговор о формальных система home от логики и на
0:07
этот раз я постараюсь как бы сделать такой мягкий непринужденный подход к доказательству
0:13
теорем геделя о неполноте а именно 2 тереме года ли они полноте поскольку разбор 1 уже был значит ну
0:22
начнём мы с того что дадим все необходимые определения это достаточно такой большой блок получается но тем не
0:28
менее без этого никак и первое с чем мы будем разбираться это собственно структура формальных систем
0:34
что они собой представляют значит запишем формальные системы
Формальные системы: определение
0:43
значит формальная система математическая это не который строго по строгим
0:50
правилам построенный язык без исключений ну точнее там могут быть не такие
0:55
соглашения вместо исключений вот но в целом это очень правильно построенный
1:01
язык вот кто знает французский на че там тоже есть достаточно жесткие правила и исключения довольно-таки мало несмотря
1:08
на то что выглядит очень сложным вот с английским по
1:13
крайней мере уж точно значит что такое вообще в целом формальная система или формальная теория
1:19
мы будем говорить именно формальных теориях это на самом деле просто некоторый набор
1:27
текстов такой свод как канонический с вот там какой библиотеки набор текстов и
1:33
этот набор мы можем изучать математические методами с помощью
1:38
находясь в теории множеств например очень люблю математическими методами при помощи там теории чисел каких
1:46
соотношений ну короче говоря всем всем этим арсеналом которые нам доступен
1:51
temsa у нас получается как бы две теории одну теорию мы изучаем например формально арифметику пиана а в другой
1:58
теории мы находимся изучая эту самую формально арифметику пиа ну то есть у нас есть теория есть эта теория вот про
2:05
эту теорию мы будем считать что она примерно это то же самое что зато в c
2:10
ну а соответственно формально через это все тоже может изучаться внутри как бы математической теории множеств
2:17
вот то есть выглядеть немножко так парадоксально тем не менее это действительно возможно значит поскольку
2:24
любой формализм это просто текст как например программы компьютерные да это
2:29
просто некий текст надо уметь его правильно грамотно строить вот мы
2:35
собственно говоря с этого и начнем значит и как строится любая формальная система ну во-первых задается два набора
2:42
переменных это так называемые свободные переменные
2:49
обычно их обозначают первыми буквами латинского алфавита маленький на abcd и
2:54
так далее ну кто хочет совсем уж полой стопроцентной строгости давайте считать
3:01
что это строки вида в палочка звездочка значит здесь я
3:07
использую регулярное выражение имеется ввиду что это строки вида в в палочка вы
3:12
две палочки в этой пачке так дальше и все переменные свободны и можем вот так вот записать всего ли доходящего
3:18
алфавите состоящего из группу вот но все что мы здесь получим это будет символы
3:24
нашего нового алфавита который мы ноги не реле с помощью вот этих вот выражений далее у нас есть запас связанных
3:31
переменных обычно это буквы из конца латинского алфавита x y z
3:39
вот ну и можно себе представлять что формально это x с палочками где палочек
3:46
может быть 0 1 2 3 и так дальше чтобы не использовать натуральные числа вот хотя
3:51
на самом деле поскольку мы находимся в теории множеством и натуральные числа можем пользоваться как бы вовсю
4:00
дальше мы конечно же вот пользуемся понятие множества хотя вот это вроде бы не множество но мы можем считать
4:05
опять-таки что это некий графически экономические символы которые заданы где-то там вы в кли давай плоскости
4:11
например или что то еще или у нас просто вот эти наборы это какие-то функции из
4:17
натурального ряда куда то еще но короче говоря главное понимать что вот эта штука она
4:24
очень хорошо погружается в компьютер то есть вот можно прямо буквально если нам памяти хватает до постольку поскольку но
4:31
хватает памяти мы можем вот этих переменных на генерить столько сколько мы хотим и у всех у них будет строго
4:37
однозначно прописан номера дальше ну переменах от них мало естественно самое
4:43
главное формально теория эта сигнатура сигнатура обычно состоит из трех
4:49
множеств это множество константных символов множество
4:55
предикат ных символов и множество функциональных символ
5:05
константные символ это все что обозначает константы в нашей формальной теории если это арифметика то это
5:12
простотой только 0 если теория групп ну например то символ единицы вот или там
5:18
айди например если мы рассматриваем движение плоскости это могут быть числа е и мнимая единица
5:25
если мы находимся в формализме комплексных чисел далее предикат ные символы это все что обозначает отношения
5:32
между объектами данной формальной теории формально теории можно рассматривать как какой-то текст про что то вот вот это
5:40
что-то про что этот текст мы будем называть объектами данные формальной теории а соответственно переменные
5:46
которые пробегают эту область я изучаемую область называется объектные
5:51
переменными ну вот отношения между объектами которых могут возникнуть например равенство неравенство
5:58
конгруэнтность подобия и так далее это все описывается вот этими символами а
6:04
преобразование которое мы выполняем в наш внутри нашей объектной области то
6:10
есть некие операции до когда моя нескольким предметам из области сопоставляем 1 ну как в теории групп
6:16
например мы там вводим умножения операцию умножения двух элементов получаем какой-то еще элементы из этого
6:22
же набора это вот собственно функциональные символ будет обозначать вот эти самые операции соответственно у
6:28
каждого предикат нова символа у каждого функционального символа есть такое понятие как валентность а именно это
6:34
количество аргумент ных мест куда можно подставить какие-то аргументы
6:40
аргументы соответственно это какие-то объекты которые мы в нашей теории изучаем вот либо переменные которые
6:47
пробегают ну сейчас мы как раз будем это все устроить ну давайте на примере
6:52
посмотрим пусть у нас есть арифметика пиана переменная те же самые сигнатура
6:59
выглядит так самая простая сигнатура 0 я вот эти множества без фигуры скоба буду
7:06
указывать потому что так проще но как бы опять таки с точки зрения полного
7:11
тотального формализма тут надо вот ставить фигурные скобки и перечислять там константы дальше предикат ный символ
7:18
у вас один и он имеет валентность 2 вот так это пишет далее у нас есть
7:25
функциональные символы их там три это сложение значит от двух аргументов это умножения
7:32
двух аргументов и это символ последователя унарный оператор
7:39
ну это вот операция x + 1 го которое мы уже ранее говорили когда обсуждали терему густой на
7:46
вот собственно сигнатуру арифметики пеано бывает сигнатуры даже бесконечные то есть этих вот операции можно ввести
7:53
много более того можно ввести целый континуум константы для каждой константы свою операцию вот тогда сигнатура
7:59
получается вообще несёт но мы будем оставаться в рамках самых простых теорий и значит будет считать
8:06
что сигнатура как правило конечно более того как мы видим и переменная да можно свести к конечному алфавиту что
8:13
тоже очень хорошо таким образом вот все вместе вот это называется алфавитом нашей формальной системы и в этом
8:20
алфавите также как там скажем в русском алфавите в латинском алфавите можно записывать текст и все что мы дальше
8:27
делаем это мы пишем некие текст и вот мы сейчас вот так вот можно все правильно
8:32
построенных текстов поместил в такой прямоугольничек
8:39
единственно здесь надо на самом деле ввести два прямоугольника 11 лист как бы с текстами
8:46
я положу снизу почему потому что это будут но условно
8:54
говоря вспомогательные тексты которые будут вставляться в эти тексты сейчас я поясню значит все что мы дальше строим
9:04
можно разделить на две категории это термо и формулы термы это жена
9:11
обозначения для объектов нашей теории например если мы говорим про арифметику piano то
9:17
натуральные числа натуральные числа можно задать значит либо явно то есть это 0 с от 0с от с от нуля и так далее и
9:25
так называемой numeral и а можно задать с помощью разных операций
9:30
ну типа там 0 + 10 + 1 умножить на два и так дальше получаются какие-то такие
9:36
сложные конструкции на вот которые все равно будут обозначать
9:43
натуральные числа при этом это мог быть даже функции то есть там будет меняться аргументы и зависимости от этого будет
9:49
получаться раз натуральные числа функции тоже будут являться как бы обозначениями
9:54
для наших объектов вот хотя это получается уже переменное обозначение но
10:00
тем ни менее и вот термы строится следующим образом
10:07
во-первых мы к темам относим все константы и все свободные переменные то
10:12
есть в термо включаем константы и свободные переменные
10:21
дальше мы можем комбинировать уже сгинь елены и термы но этот как бы
10:27
база индукции или база рекурсии точнее генерировать при помощи функциональных
10:32
символов каждый функциональный символ имеет такой вид это какой-то значок открывается скобка идет аргумент на
10:39
место , и так дальше то есть аргументы и места расположенная между скобками
10:45
разделенные запятой и функциональный силу в этом формализме кстати сложения и он даже не правильно записывать вот так
10:53
плюс а.б. но поскольку традиция непреодолимо вот тут как раз
11:00
начинается исключение в нашем языке то мы будем всегда это писать как a + b
11:07
подразумевая при этом внешние скобки чтобы у нас не путалась приоритетность при записи форму
11:13
вот но вообще строгов строго формально прямо совсем по правилу надо вот писать вот так
11:20
ну я думаю тут не будет возникать каких-то противоречий привет толкование
11:25
вот таких формул до их легко достаточно переделать в правильные значит все что
11:31
дальше которым относится это следующий если у нас т1 и так далее т.н. это термо
11:38
ну что термов мы обозначим следующим образом тобой т.м. сигма
11:44
вот то есть мы просто строим некая новое множество это будет множество текстов то есть нам дали алфавит теперь мы строим
11:50
текст и если вот эти наши уже теперь термы построены из нашего
11:56
множество т.м. имеется и дан какой-то функциональный symbol of
12:03
из нашей сигнатуры то тогда
12:09
говорим мы вот такая комбинация f от т1 и так далее т.н. это тоже term
12:20
при этом подразумевается что f это функциональный символ валентности н то
12:26
есть там ровно n аргумент ных место ещё это можно вот так вот записать то есть мы как бы в ну что всех функциональных
12:33
символов вырезали кусок а именно функциональные силы валентности pen
12:40
ну и соответственно вот так вот можно подставлять подставлять одно в другое мы можем там собрать формула типа не
12:47
формула термо а плюс b умножить на 0 плюс c потом от всего этого взять с и
12:55
так далее вот мы просто занимаемся тем что подставляем в
13:00
функциональные силы все в новой термы которые мы тут получаем на каждом шаге рекурсии и вот термами
13:07
являются те и только те тексты которые получены по данным правилам ничего лишнего там быть не должно
13:13
кстати каждому ты раму можно сопоставить так называемое дерево разбора тут нужно
13:19
как бы вести от самый внешний последние исполняемой операции в этом terme помещать ее в
13:26
корень вот дальше мы видим какой тут аргумент тут аргумент очевидно
13:33
сложение будет сначала вот кстати опять таки я здесь не поставил скобки
13:38
выделяющие умножения но помимо вот таких соглашений у нас есть соглашение о
13:43
приоритетах то есть умножение скажем имеет высший приоритет по отношению к сложению
13:49
тоже сама там будет логических операциях если есть соглашение приоритетах то
13:55
можно экономить на скобках скажем так вот если нет тогда уж извините нас везде писать скупки то есть вот здесь вот тоже
14:01
например поставить и тогда мы видим что у нас значит под с стоит операция плюс у
14:07
плюсика уже два аргумента соответственно есть левый правый аргумент и мы можем
14:13
посмотреть что у нас справа стоит c слева у нас стоит умножение у которого
14:20
тоже есть два аргумента справа стоит ноль слева стоит опять term сложный
14:27
операция сложения и дальше уже получаются переменная a и b свободные
14:32
переменные значит и таким образом получается вот это вот так называемо дерево разбора по которой
14:39
можно проверить правильность построенные формулы и наоборот если у нас дано некое
14:45
дерево разбора некая дерево где в листьях стоят либо переменные либо константы свободные переменные имеются
14:51
ввиду хотя позже мы увидим что там могут появляться и связанные переменные и
14:57
дальше а узлах стоят значит элементы множества функциональных символов и
15:04
количество веток которые исходят из узлов соответствует их валентности ну то
15:11
есть or насти тогда мы поэтому дерево можем совершенно правильно грамотно в с точки зрения
15:17
нашего формализм построить некий терм ну и значит да и вот термы мы поселим
15:24
поселим вот здесь на втором и листочки которые как бы
15:32
подложим под первый листочек с текстами нашей теории да пока еще это не теория это просто
15:38
формальная система и вот вторая часть текстов корпуса текстов таскать это
15:44
формулы формулы отражают как раз такие разные
15:50
зависимости между нашими объектами то есть у нас есть базовая формула или атомарная формула или атомарный предикат
15:57
правильно говорить который отвечает за равенство объектов в нашей
16:04
теории ну кстати говоря если теория содержит предикат носила равенство то и
16:09
мы всегда читаем автоматом туда присоединяются все аксиомы равенство но об этом чуть позже
16:15
но помимо этого мы можем на генерить новые отношения например мы можем определить отношение
16:22
меньше либо равно следующим способом а меньше либо равно по определению будет равно значит такой
16:30
форма не существует z а плюс z равно b правда мы еще не описали как это строить
16:37
но сейчас опишем то есть мы можем ввести новые отношения между нашими объекта
16:42
определив его через старый и тем самым у нас получится
16:48
не входящая в сигнатуру отношения между объектами и собственно все формулу
16:53
теория это в общем то либо отношения либо просто какие-то предложения например основная теорема арифметики это
16:59
предложение формализме арифметики пеано предложение этот смысл еще кто-то кому-то чудо предлагает это просто
17:07
замкнуто формула которая что-то утверждает про все числа в целом вот
17:12
осенью нет параметров ну значит что такое формулы формула также строятся рекурсивно отталкиваясь от некого
17:19
базового множество вот и подальше по некоторым правилам они
17:25
устраиваться такая бесконечная цепочка формул так в общем то тоже такое же дерево получается во-первых мы к
17:31
формулам относим давно что формул могу обозначим ф.м. сигма
17:37
во-первых мы к формулам отнесем все что получается когда он берем предикат ный
17:43
символ какой-нибудь и туда подставляем любой term то есть если п это предикат ный символ
17:52
нашей сигнатуры причем валентности pen
17:57
соответственно что-то у нас 31 т.н.
18:03
это термы которые вот построены по этим правилам
18:08
то тогда вот такая штука то есть композиция предикат нова символа с
18:15
термами является формулой
18:20
тем самым мы определили так называемые атомарные
18:25
предикаты нашей теории вот то есть это все что получается подстановкой сюда например a + b ну вот
18:34
а плюс z это атомарный предикат ой ну собственно вот а плюс z равно b это уже
18:40
это тоже атомарный протекать потому что он повод получен из равенства в которой поставлю два термо а плюс z и б правда
18:47
мы еще не знаем что этот точнее такой псевдо т.р. сейчас я поясню
18:53
об этом значит дальше если у нас есть какие-то формулы а и b
18:58
вот большими латинские буквы мы мы будем обозначать
19:04
произвольные формулы нашей формальной системы иначе это их еще можно понимать
19:10
как некие бы левски и переменные потому что формула они могут принимать значение только истинно или ложь по логическим
19:17
правилам да потому что мы автоматически что еще цепляем и исчисление высказываний вот и поэтому а и b эtom
19:24
обозначения вот эти таки футболе его значных функций формулы можно еще рассматривать как были различные функции
19:30
то есть мы им подали на вход какие-то термы а на выходе получили либо истина либо ложь если a и b это какие-то формы
19:38
а то тогда
19:43
формулами же будут и следующее выражение отрицаниям
19:50
конъюнкция а и b дизъюнкция а и b
19:55
импликация я их беру в скобки опять таки для того
20:03
чтобы когда мы будем генерить формулы 2 другую вкладывать вот по такому же принципу
20:08
чтобы нам не путаться с приоритетами но на самом деле тут тоже всегда есть
20:13
стандартные устоявшиеся нормы priority приоритизации который говорят что отрицание ведь самый высший приоритет
20:19
также как умножение например конъюнкции дизъюнкция они ну конъюнкция
20:26
следующий приоритет визируется следующий и самый славы приоритет у импликации с
20:32
тем самым можно опять таки экономить на скобках если мы принимаем эти соглашения о приоритетах
20:38
значит таким образом мы уже получаем некие простейшие формулы нашей теории
20:44
типа что можем не все можем написать типа там
20:49
a плюс b равно с
20:55
киви а плюс 0 равно d вот это будет как
21:01
раз таки совершенно правильно построенная формула ну опять таки надо брать скобочки везде
21:07
неважно истинна она или ложна это вообще форму с параметрами зависимости от того что вы вместо и а bdc подставим у нас
21:15
могут быть разные варианты ответа да либо истина либо ложь тем не менее это правильно построенная формула но это еще
21:22
не все дело в том что в формальных математических системах нам нужны кванторы кстати в языках
21:29
программирования нала кванторов как я уже говорил это цикл и разного вида
21:34
ну там все конечно поэтому там в общем то quanta но превращается в некий конечный
21:40
хотя циклы while он там до потенциально бесконечный может быть итак следующее чему мы должны научиться
21:48
это делать подстановку связанные переменной вместо свободными обычно это
21:54
записывается следующим образом если у нас имеется формула а
22:00
со свободной переменной а маленькая ну вот например как это то вот таким
22:06
символом записывают подстановку когда мы формуле а все вхождения именно
22:14
все вхождения переменной а свободной заменили на переменную x
22:20
связано то есть вот все равно что здесь я вместо а вписал везде x
22:27
но это еще не формула дело в том что
22:35
пока свободна и пока связанная переменная не замкнута квартирам это не
22:41
формула таким образом для того чтобы получить форум и вы должны это дело замкнуть так вот формулами являются для
22:48
любого x а где мы заменили x на перемену она x а
22:53
также формула существует x а где а маленькая замедлено x маленькая
23:01
единственное что здесь требуется при такой постановке это чтобы переменная x уже не было бы в формуле а потому что
23:09
например мы сделали одну замену а потом например мы здесь захотели бы б ну мы
23:14
можем вот так вот написать там для любого x неважно сейчас верна эта формула we never на мы лепса 0 икс икс
23:21
плюс b равно икс плюс 0 равно d а потом хотим еще
23:26
значит бы заменить на связанную переменную и поставить впереди какой
23:32
диктатору при существует x вот если мы бы заменим на x и поставим здесь экватор
23:38
существует получится уже не формула какая-то ерунда вот существует x такой что для любого x
23:43
да мы не понимаем как это читать это примерно то же самое что брать там интеграл
23:50
скажем от 0 до x и дальше будет функция f от x pdx это такая же по формату
23:57
формула с замкнутой перемены со связанной переменной только вместо кванторы используется знак интеграла еще
24:04
бывает знак суммы еще есть вот такой вот знак ну там типа а плюс x равно c
24:13
это тоже своего рода quandl только как бы term квант эрдал он генерит нам term
24:19
то есть какое-то число или какое-то множество они формулу вот так вот надо что надо эту замену
24:28
производить только в том случае если в формуле еще не было переменной x если она уже там было то лучше пользоваться
24:34
другую переменную пример y z или или что то еще либо выполнить замену переменной под
24:41
квантовом это позволяют аксиомы исчисления предикатов то есть например вот здесь я заменю x на y у меня будет
24:48
существует y а а заменено на y таким образом x у меня отсюда ушел и тогда я
24:54
могу добавлять новый квант где у меня войдет переменная x которая заменит там
24:59
какой-то другой b c или d поскольку атом а маленького там уже не будет и вот
25:04
формулы получается построены по трем правилам это все что получается
25:09
непосредственно подстановкой термов предикаты приятные символы далее это все
25:15
что получается логическими связками из других формул и наконец это формула
25:20
которые перед которыми ставится кванторы и тем самым значит свободные переменные
25:27
заменяются на связанные у нас появляется формула со связанными переменной для таких формул естественно существуют
25:34
аналогичное дерево разбора здесь помимо операции потому что у нас есть
25:39
термы там внутри всегда поэтому операции тоже будут но здесь также будут в узлах стоять еще и вот эти вот связки вот
25:46
унарная связка 3 бинарных связки могут стоять ну и кванторы тоже будут стоять в
25:52
этих узлах как некие новые операторы можно отдельно выделить чего оператор
25:57
замены переменных но можно считать это как одним актом действия потому что без
26:03
кванторы это уже не формула это какая-то не то формула вот ну и и наоборот да соответственно
26:11
можем построить ника дерево разбора тут накидать логические операции подставить вот тут кстати уже будет появляться
26:17
свободные связанной переменной в листьях вот но они там могут стоять тогда я
26:23
только тогда когда где-то выше в каком-то родители стоит кванта по этой переменной и собственно вся вот эта
26:28
ветка которая стоит под квантовом она является область действия данного кванта
26:34
вот хотя мы знаем теорема претворено форуме о том как в си кванторы можно вынести вперед произведя некие замены
26:40
переменных да и хочу читать всю форму без квартирная кванторы только впереди
26:46
но мы сейчас это не будем углубляться значит теперь нам надо
26:51
перейти к тому собственно года вот вот этот лист это наша формула
26:58
формулах и вот то что мы получаем в обычной
27:04
формальной математической системе всякие там теоремы рассуждения которые мы проводим все что все результаты так
27:10
сказать математические они описываются вот на этом листике номер один в котором лежат все формулы созданные внутри нашей
27:18
сигнатуры формулы бывают разные бывают формулы со свободными переменные бывают формулы без
27:25
свободных переменных так называемые замкнутые форму формулы за свободные переменными это что-то
27:31
вроде функции то есть у нее есть аргументы abcd зависимости от постановки туда чего-то каких-то других термов или
27:39
констант мы можем получить разный ответ то есть это может быть истинно да может быть ложным то что вещи либо равно b
27:45
например вот как раз та типичная форма с двумя холодным переменами
27:50
если же мы напишем вот так вот здесь еще для любых x и y и вот здесь вместо а
27:58
напишем икса вместо b напишем y у нас свободных переменных уже не будет
28:04
все они будут закрыты кванты раме получается формула так называемая
28:09
замкнутая она может быть либо всегда истинной либо всегда ложь без вариант
28:16
поэтому вот в этом куске в этом пласте таскать бесконечном
28:21
формулу можно выделить а некая некую часть которую мы назовем
28:27
связанными замкнутыми формулами замкнутые формулы
28:35
вот ну в принципе это как бы такая тут двойственность возникает а потому что из всех формул вот этих вообще всех
28:43
приписывая спереди кванторы мы будем получать замкнуто есть тут получается что как бы вот эти множества они
28:51
более широкая отображается в более узкая причем однозначным образом то есть тут как раз
28:58
работает та самая бесконечность которую мы знаем из теории множество что больше
29:03
множество можно отобразить однозначно в начни активно отобразить в меньшее
29:09
множество вот но тем не менее нам бывает полезно и формулы со свободными переменными как вот этого какое то
29:15
неравенство особенно когда мы хотим их куда-то еще внутрь подставить доп то что нельзя
29:21
что-то замкнуть контур если там уже нет свободных переменных но работать в
29:26
теории вы всегда предпочитаем замкнутыми то есть все теоремы лучше считать замкнутыми все аксиомы лучше считать
29:32
замкнутыми формулами ну почему но я надеюсь что будет понятно из дальнейшего теперь что мы делаем с
29:39
этими замкнутыми формулами значит
29:44
но вот хорошо мы создали такой вот корпус текстов огромный научились там
29:50
генерить термо подставлять их формулы там что-то понаписали вопрос какое это
29:56
отношение имеет к некой исследуемой области на 3 натуральным числам отношения появится только тогда когда мы
30:03
какие-то из этих формул объявим истинными то есть тогда мы сможем
30:08
поделить все формулы вот так вот на ну условно пополам
30:14
на формула которой являются истинными скажем
30:20
да и ложными по закону исключенного третьего все
30:26
форму они либо истина либо ложь не вот ясно что форму со свободно переменными там как бы в зависимости от поставленных
30:33
аргументов поэтому здесь вот такой пунктир прям совсем пунктир вот а вот
30:39
эти мы можем более четко поделить пополам на истинные и ложные но все
30:44
будет зависеть от того что мы вообще считаем истинной вот а равно а это
30:50
истинно или это ложь соответственно для того чтобы определиться с понятием истинности в
30:57
нашей теории но это такая на самом деле кашу псевдо
31:03
истинность у нас потом будет еще одна истинность в модели тут просьба не
31:08
путать тем не менее мы можем задать некий список форму
31:14
которые мы прям вот объявляем по закону да как по конституции объявляем некий
31:20
список формул истинными и мы его выделяем где-то здесь
31:26
таким особым цветом вот эти формулы мы говорим вот это
31:32
истинная формула почему мы не берем сразу все что нам
31:38
надо не объявляем истинными дело в том что если вы все что угодно начнем объявлять
31:45
истины мы можем получить противоречие например мы скажем что в одном месте в этом списке будет стоять а равно а
31:51
истина а в другом мы напишем они равно а та же истина тогда у нас получится просто обычное логическое противоречие с
31:59
противоречия как мы знаем вообще обследуют все что угодно и поэтому тогда мы же вообще все форума считать и
32:05
стенами и тем самым теория перестанет различать истинность и ложность вот так
32:11
так сказать как говорю воланда без тени невозможно увидеть рельеф
32:17
поэтому для того чтобы был был как бы и свет и тень нам нужно нужно определиться
32:24
выделить как-то вот как мы будем строить эти самые стены формулы и чем меньше будет вот этот базис который
32:32
мы объявляем истинной тем нам проще будет верифицировать то что мы не столкнемся с противоречием то есть базис
32:38
должен быть максимально экономной вот как требовал гиллеберда аксиоматика а должна быть непротиворечивой и чем
32:46
меньше то максимум тем это легче установить да и желательно чтоб всех всем были
32:51
независимыми это тоже важное требование потому что если они начинают как-то друг на друга влияет зависеть еще что то мы
32:57
перестаем контролировать что у нас потом производится из этих аксиом в дальнейшем мы можем случайно сузить область котором
33:05
мы делаем истины например вообще все свести противоречие мы можем случайно расширить истинность
33:11
да просто до всех форума как я говорю до этого вот поэтому лучше чтобы максим
33:17
аттика было не только непротиворечиво не что psy аксиом были друг от друга независимо это
33:23
так сказать в идеале конечно самый самый идеал как я уже
33:28
ранее говорил это такой случай когда вот этот независимый
33:34
аксиоматический боец он еще и породит все породит все формулы таким образом что
33:41
они будут либо истины и положен то есть мы в нашей теории сможем доказать любую из этих формул и либо сможем
33:47
опровергнуть любой из этих форм доказать ее отрицания и тогда у нас понятие истинности она станет так сказать
33:53
истинном у нас действительно все формулы ну замкнутые формула имеют у конечно разобьются строго пополам на истинное и
34:00
ложное сожалению мы знаем что это далеко не так потому что есть теорема которые не доказуемо в аксиоматике вот
34:08
но кстати говоря когда мы вводим модель то там есть такие так называемой теории
34:13
которые состоят из всех истинных данной модели теарин вот там мы уже не скупился
34:18
так сказать на аксиоматические базисы просто вообще все все что там истина объявляем аксиомами
34:24
вот но это такой технический момент работа с моделями и так как водится
34:31
собственно говоря вот этот вот аксиоматический базис или теория типа
34:37
теории обычно в молоке подразумевается именно список аксиом то есть вот этот вот желтый сектор аксиомы вводятся
34:44
следующим образом во-первых мы должны вспомнить о том что
34:52
у нас есть логика высказываний или исчисления высказываний и
34:57
из это и и воспользоваться ею для того чтобы получать аксиому то есть все что
35:03
истина логике естественно должно оставаться истинном и в любой
35:08
математической теории иначе у нас теряется связь между логикой математикой
35:15
это уже было бы очень странно значит аксиома
Аксиомы: логические и нелогические
35:22
по этому общему делятся на два вида бывают аксиома логически те которые мы
35:28
унаследовали из логики и бывают аксиомы не логически это те которые мы
35:34
хотим вот для данной конкретной теории задать значит логические аксиомы
35:42
они генерации следующим образом во-первых мы из логики высказываний
35:47
уберем все возможные тавтологии и подставляем туда вместо булевских
35:53
переменных вот этих вот а и b поставляем все наши формулы все замкнутые формулы
35:59
вот вот тут мы тоже не скупимся значит знает что тавтология она не выводит за
36:05
рамки истинности да то есть если он ну например вот известно тавтология а следует там
36:13
чтобы вместо мы здесь не подставили 0 или единицу мы всегда будем получать единицу это тавтология поэтому
36:20
соответственно к мы не подставили сюда функцию которые значения могут быть тоже только истинные или ложные мы тоже будем
36:26
получать истину уже неважно даже даже даже не важно с параметрами там формула без параметров никакого никакой разницы
36:34
нет это будет всегда тождественно истина например если если я напишу о меньше
36:39
либо равно бы следуют а меньше либо равно бы ни у кого не вызовет сомнений что это действительно истина вот но
36:46
значит аксиомы мы считаем только замкнутые формула поэтому мы говорим что все
36:51
что получается из тавтологии подстановкой туда замкнутых формул нашей
36:57
сигнатуры это все является аксим все относится к аксиомам
37:02
начинаю в нашей формальной системе запишем это так
37:08
примеры подстановок
37:15
в тавтологии
37:20
примеры почему потому что мы берём какую-то конкретную тавтологию которых у
37:27
нас счетное множество берем какую-то конкретную формулу замкнутую нашей сигнатуре
37:33
точнее набор формул до в зависимости от того сколько там у тавтологии переменных
37:39
подставляем их туда и получается некая новая формула которая вот по этим
37:44
правилам будет построена значит это та же формула из нашей системы и объявляем ее аксиомой понятно что их
37:52
получается счет не набора причем он строит там из двух четных наборов которые вы композицию между собой но тем
37:59
ни менее ну и вот каждый экземпляр называется примером подстановки тавтологию поэтому все это мы объявляем
38:07
аксиомы но нам этого мало потому что вот такие такого рода формулы они не
38:13
включают в себя значит кванторы поэтому мы еще вводим общем вот
38:19
за кванторов максимум имеет такой вид любого x от x
38:27
следует а у т где т
38:32
произвольный терм и второе если для какого-то termo
38:42
выполнялся at&t тогда мы говорим существует x-mode x
38:48
значит тут важно понимать что здесь имеется в виду что ты это любой term
38:55
gt давайте любой напишем другой а здесь мы напишем где т некоторые кирам
39:02
некоторые тиром ну смысла всем понятен что если мы
39:09
доказали что для ics для для любого x верно для любой объектный для любого объекта эта формула
39:16
верна то тогда можно любой term туда подставите будет верное утверждение это нам
39:24
увязывает так сказать формулы с переменными и формулы от
39:30
термов когда можно поставлять терме тем самым мы говорим что у нас действительно переменные пробегают весь ну все объекты
39:37
нашей теории объектами являются как раз termo правильно построенный термо и наоборот если мы нашли какой-то тырым
39:47
который засвидетельствовал нам формулу а таких случаях кстати называют
39:53
ну там константу re-therm то что то значение переменной при котором формула
39:59
стала истина ее называют свидетелем если мы нашли какой-то тиром который нам
40:04
засвидетельствовал истинность формулы а там и говорят что существует такое x при котором выполняется от x здесь уже term
40:11
of термо нет здесь переменная но зато у нас есть quandl при этом такие формулы
40:17
они увязывают кванторы переменная и термо причем надо сказать что вот вот
40:23
эта фраза где ты любой term она находится в нашей мета теории она не
40:29
относится к формализму которые мы изучаем и это надо всегда различать что вот есть
40:35
тексты которые лежат в нашем формализме а есть наши рассуждения наши какие-то требования которые находятся вне этого
40:43
формализма а именно в нашей теории с помощью которой мы изучаем данный формализм значит вот это вот логически
40:50
аксиома да конечно надо не забывать что во первых а это должна быть правильно построена
40:57
формула всегда туре 7 вторых здесь на самом деле стоит подстановка
41:03
то есть правильнее было бы так вот написать вместо переменной свободный а мы представляем
41:09
свободную переменную x и тогда здесь говорим мы мы должны вместо той же самой
41:16
свободной переменной а подставить конкретный терм из нашей теории
41:24
вот только тогда это будет вот прям совсем грамотно грамотно построенная
41:29
аксиома на самом деле это конечно же получается ни одна аксиома да это получается
41:35
ну для каждой формулы а в которой есть свободная переменная а маленькая мы
41:41
можем такую штуку проделать ну записать такую аксиому и конечно же для того
41:46
чтобы вот эти аксиомы тоже были замкнуты и формулами как мы хотим чтобы это все сюда помещалась мы должны сказать что
41:53
здесь стоят еще кванторы для любого b1 б.н.
42:00
где b1 б.н. это все остальные свободные
42:05
переменные формулы а то есть мы мы а уже пою зале да мы заняли а все остальные мы
42:10
просто вот так вот за нумеровали понятно делаешь и их там конечный набор и потом все это дело замкнули и я здесь
42:18
опять делаю ошибку потому что под контура может стать только
42:23
связанная перемена то есть на самом деле имеется ввиду что я все остальные вот
42:28
эти вот переменные b1 bm заменил на связанные y1 y en и вот эти уже игреки
42:35
поставил сюда но опять-таки к вопросу об исключениях языке да мы
42:41
упрощаем себе жизнь тем что сюда подписываем под кванта свободные переменные но надо держать в
42:49
голове что это все сводится к нашим правилам то есть это все можно
42:54
погрузить в тот формализм который я вам здесь описывал иначе вы это просто все не работала то
43:01
есть есть некая произвольность но произвольность в рамках правил все равно
43:07
так но на этом заканчиваются логические аксиомы и мы их наверное выделим
43:14
как-нибудь там еще
43:19
каким-то цветом вот пусть вот этот пласт
43:24
это этот этаж нижней так сказать цокольный этаж нашей теории это на все
43:30
логически аксиома мы их всегда цепляем автоматом к любой формальной системе но
43:36
к любой формальной теории когда мы делаем формально теорию вот я думаю что языках программирования есть
43:42
что-то аналогичное потому что там мы там и генерим разные тоже термы мы там
43:48
всегда что-то вычисляем вот но но там есть некие соглашения когда мы что-то
43:55
производится пусть пусть по правилам одинаковым для всех языков программирования
44:01
но может быть это явно нигде не прописано ну просто сама конструкция компьютера это предполагает скажем так
44:07
дальше собственно говоря нам надо перечислить ввести понятие не логических
44:15
axil но с ними как раз все гораздо проще не
44:23
логические аксиомы это
44:31
это просто некое подмножество вот здесь в замкнутых формулах нашей сигнатуре
44:39
это подмножество т.в. ф м 7 вот так вот обозначу как в
44:46
вещественных числах обозначают замыкает это не замыкание множество всех формул
44:52
да это просто это часть этого множества именно замкнутые формулы из нашей
44:57
сигнатуры укажем явно что это часть [музыка]
45:03
множество ф м сигма вот то есть просто берется некий список оттуда и все ну как
45:09
я говорил желательно чтобы они были независимы и желательно чтобы было как можно меньше чтобы проще было
45:14
анализировать желательно чтобы они противо не приводили противоречие чтобы как бы
45:19
любая конечная конъюнкция из них не было бы противоречием вот и вот именно не
45:26
логические аксиомы и принято называть теорией в данном формализме в данной сигнатуре например если мы вспомним
45:33
арифметику piano там у нас были такие аксиома
45:38
значит первое это
45:43
аксиомы равенство значит вот я опять буду записывать
45:49
аксиомы как незамкнутые формула хотя сам потребовал чтобы эти фуру вы были замкнуты для чего ну потому что так
45:56
просто короче вот я пишу а равно б моя ну давайте такая равно b и b
46:02
равно c отсюда следует аромат c а равно б
46:08
следует b равно а и а равно а строго говоря это не аксиома почему
46:15
потому что здесь стоят формулы со свободными переменными на самом деле нам надо было бы вместо
46:20
свободных переменных здесь подставить связаны и замкнуть это дело все квартиры
46:26
то есть вот эту аксиому последняя она бы выражалось так него икс икс равно икс
46:31
ну тут просто больше символов получается и мы опять-таки пользуемся никакими
46:36
условностями так же как с приоритетами операции скобками да и пишем это все в
46:43
виде формул за свободную перемен на самом деле подразумеваем что они замкнуты по всем своим переменном это
46:51
стандартные аксиомы равенство облагает как бы говорящий нам о том что равенство является отношением эквивалентности
46:57
ну мы помним что на самом деле равенство обоих это не просто отношение эквивалентности равенство даже но
47:04
говорить что замена равного на равная всегда приводит всегда должно сохранять истинность
47:10
формул и должен приводить к равным there мам поэтому мы от равенство еще требуем вот конкретно в арифметики пеано мы
47:17
требуем чтобы что если а равно b и b равны
47:22
все равно d то тогда выполняется следующие а плюс c
47:30
равно вы + d вот мы она б на равное заменили c
47:36
на d умножить на c равняется бы умножить на d и без at a равняется с от b
47:45
в произвольной формальной теории естественно помимо ну то есть мы должны вместо вот этих конкретных плюс умножить
47:53
с подставлять эти самые функциональные символ для всех функциональных символов это должно
47:59
работать больше того здесь переменная можно заменить на произвольные термы потому что у нас есть вот такая аксиома
48:06
поскольку на самом деле эти аксиомы замкнуты как я говорю квартирами то есть там впереди стоит квантов и от и из этих
48:13
аксиом будет следовать что любую переменную здесь можно поменять на любой term то
48:19
есть вместо а можно подставить любое сложное арифметическое выражение если оно равно b то значит равенство
48:27
сохранится и таким образом у нас получать только что называют школе тождественные преобразования
48:33
вот ну и помимо того если у нас еще есть какие-то предикаты в теории помимо
48:39
равенство то надо требовать чтобы еще и эти предикаты сохранялись сохраняли истинность при подмене равна на равны но
48:46
это так называемые общие требования к равенству в любой математической теории
48:51
более того эти аксиомы которые нам указывают как ведет себя равенство их
48:56
можно даже не относить к к аксиомам теории а считать их тоже логическими аксионы ну так около логически потому
49:03
что как только у нас сигнатуре появляется равенством и сразу автоматом считаем что
49:09
она подчиняется этим правилам то есть это отношение эквивалентности которые не приводят
49:15
к смене значение термов и формулу при замене равных на равны вот ну и наконец
49:22
основной блок аксиом именно арифметики пеано да это уже вот такие
49:28
содержательные аксиомы которые нам говорят о том как все таки связано между собой вот эти вот базовые наши предикаты
49:36
и функции ну и константы тоже это во-первых аксиому для с как я говорил
49:42
уже значит во первых из а никогда не равно нулю тут я опять
49:49
пользуюсь сокращениями опять выбросов гантер во вторых если у нас
49:55
is at a равно без от b то тогда а равно
50:00
б это вот уже антипод аксиомы равенство в обратную сторону если у нас ну какое по
50:07
сути это означает индуктивность вот этого ударного
50:12
функционального символа дальше мы вводим
50:17
рекурсивно сложение умножения а именно мы говорим что + 0 это а а плюс описать
50:25
б это с от а плюс b умножить на 0 это 0 и а умножить на sb это а
50:34
умножить на b плюс плюс а
50:39
мы с понимаем просто как бы плюс один из ответа b плюс один раскрываем скобки
50:45
получаю вот так получается такая аксиома опять-таки все замыкаем квартирами и
50:51
четвертое это аксиома индукции точнее схем аксиом опять-таки потому что
50:58
в аксиомах индукции мы получаем бесконечную серию аксиом которые
51:03
получаются из формул со свободными переменными
51:11
вот но я не буду выписывать мы это разбирали вот ваши 1 значит как выглядит индукция но главная
51:18
тоже туда подставляется формула в которой есть хотя бы одна свободная переменная вместо которая поставляется дойдет 0x x минус 1 и
51:28
потом она ещё вся замыкается по всем остальную свободно перемену она а также замыкается кванторы всеобщности
51:34
вот это получается если вот если приходится замыкать по дополнительным параметром то это получается индукцию с
51:41
параметрами но ничего тут сложного нет
51:46
собственно и вот получается такой перечень и вот можно привести пример там теория групп на при она гораздо проще
51:53
чем арифметика пиана там всего одна операция вот там есть единичка
52:00
указываются свойства это единички указываются то что операция ассоциативно что есть нейтрально что единица является
52:08
нейтральным элементом и что есть обратный элемент для каждого элемента и все
52:15
там уже нет никакой индукции там и так далее мы знаем что есть арифметики более простые например их медь как у роббинс
52:22
оно есть там еще более другие арифметики в которых вообще нет индукции тем не
52:28
менее прекрасно они себе существует что-то умеет доказывать ну кстати в качестве упражнения можете проверить что
52:36
термами арифметики пеано
52:41
первыми термальных медики piano это многочлен и от переменных и констант
52:50
значит ну точнее полиномы доп то что там разные могут быть
52:56
[музыка] [аплодисменты] ну давайте так напишем
53:01
многочлены от
53:10
constant и и
53:16
этих самых свободных переменных [музыка] ну то есть выражение типа там а в
53:23
квадрате плюс b xpaмe + c ix x быть не должно потому что мы их
53:32
только под квантовыми вводим да вот и вот так собственно не должно python топ константы и соответственно
53:37
вот до для арифметики пеано еще есть такое обозначение для numeral of во
53:42
первых что такое numeral номера это обозначение натурального числа в данном формализме что такое натуральные числа в
53:49
данном формализме у нас есть одна всего константа но зато у нас есть
53:54
оператор последователя и вот все что мы с его помощью можно генерить это обозначение натуральных чисел собственно
54:00
говоря или numeral и то есть это 0 это с от нуля скобки я выбрасываю опять же спс
Нумералы
54:08
от нуля ссс от нуля и так далее и обычно
54:15
вот эти штуки обозначают следующим образом это есть и подчеркнутая где n
54:21
это количество букв с в данном терме но просто для для упрощения записи чтобы каждый раз не
54:28
делать вот так вот где с там встречается один раз мы просто пишем от подчеркнуто
54:35
это будет обозначение numeral а то есть numeral это в нашей формальной системе
54:40
обозначения для натурального числа это еще как бы не сама натуральное число в нашими эта теория а просто его значок
54:48
вот так вот будем использовать то есть например там три подчёркнуто это с с с 0
54:55
вот так а0 подчеркнут это со мной и есть ну это уже такая конкретика про
55:01
арифметику пиана мы скоро к этому делу перейдем ну хорошо вот не логически аксиому мы
55:08
задали вот здесь на втором этаже наверно можно их как-то память еще вот
55:15
так мы постарались выбрать компактный набор
55:22
какой то их достаточно немного вот частности арифметики пеано вопроса как получить все остальные истины и так
55:28
сказать утверждение здесь в нашей теории мы же хотим чтобы помимо
55:36
аксиомы что-то новое еще узнавали о об этой предметной области которую мы описываем для этого есть правила вывода
55:44
эти правила по сути являются некой машиной которая из аксиом по строгим
Правила вывода и построение выводов
55:51
правилам производит новое истинное утверждение вот вывод хорош тем что он
55:57
сохраняет истинность если мы стартовали если мы на вход ему подали какой-то набор истинных формул
56:04
то и на выходе мы тоже получим набор истинных форму
56:10
если мы подали какую-то чушь то или на выходе . как говорил фон нейман чушь на входе чушь на выходе
56:16
это некая машина эта машина выглядит достаточно просто есть всего три правила
56:23
которые нам позволяют переходить от одних истинных форму другим общий вид
56:29
правила вывода
56:36
общие правила вывода таков нам дали несколько формул которые перечислены через запятую можно
56:44
считать что это множество да просто взять фигурной скобкой это некая множество форму то есть вот из-за формы
56:49
просто чет там взяли конечный набор формул ну и конечно
56:58
лучше считать что они замкнуты и все потому что мы стартуем от замкнутую форму хотя с другой стороны у нас есть
57:04
формула которая позволяет переходить к десантным то вот увели не аксиома постановка каких-то термов а в термах
57:10
могут содержаться свободные переменные поэтому я вот не могут появляться в принципе свободное но в целом это
57:17
выглядит так вот нам дали какой-то набор формул который считается истинным либо под искать по праву
57:23
аксиоматике либо просто потому что мы перед этим мы же его доказали
57:28
и говорят нам вот тут еще стоит формула-б которая если эти истины ту и вот эта
57:34
формула будет истинной понятное дело что у них есть какая-то внутренняя органическая связь просто так нельзя тут от балды любую
57:41
форму написать но просто в целом вот конфигурация выглядит так это некий шаг программы доказательства
57:48
иначе каким будет правила вывода во первых это модус понос
57:57
выглядит он следующим образом если мы уже доказали а и а следует б
58:06
то тогда бы то есть например
58:15
например мы доказали ну среди все у нас есть аксиома выбора да мы из аксиому
58:22
выбора вы вывели мы доказали что из аксиомы выбора следует теорема tsar bell тогда говорим мы тире моцарелла ли эти
58:29
теоремой в нашей теории потому что максим выбора является аксиомой наш теорий вот как-то так это работает
58:37
понятное дело что это та же схема то есть вместо а и b можно подставлять любые формулы желательно замкнутые вот
58:44
но в принципе ничто не мешает и не замкнутая формула здесь использовать и это это правило она работает ну как бы
58:53
без квант арно и если там сидели кванторы они так и будут сидеть если их не было то они не появятся и нужны еще
58:59
два правила которые позволяют увозить кванторы что можно будет здесь вот мы как бы
59:05
просто показали ники импликации обязывающее кванторы и постановки термов а есть еще аксиомы которые позволяют
59:12
квант ввести аксиома имеет следующий вид это так называемое правило
59:17
бернайс а если у нас есть импликация а следует б
59:24
то мы можем сказать что из а
59:30
следует для любого x б и вот тут мы пропишем явно замену
59:38
свободной переменной b на x и второе если из б
59:46
значит это не конъюнкция правил это просто два независимых правило я могу
59:52
здесь нет давайте так и сделаем напишем другие буквы чтобы не путать
59:57
если из c следует д то тогда из сцен из существует x c здесь
1:00:09
я заменяются на x следует д ну понятное дело что для любых ситуаций
1:00:14
это неприменимо а применимо это в следующих случаях есть надо указать опять на как сказать
1:00:23
входит или не входит куда либо какая-то переменная
1:00:32
так вот во первых x не должен входить ни в одну из этих форм
1:00:39
чтобы не было коллизий переменах их не входят него не в б я вот так пишу опять
1:00:46
таки имеется ввиду что я нахожусь в мета теории им не позволено все я смогу писать что угодно вот но можно это
1:00:53
переписать на языке программирования там до x не является под строкой почему не
1:00:59
просто под строкой такой которая стоит на аргумент нам вести и здесь соответственно x не входит в c и d
1:01:08
но самое главное вот эта переменная b которую мы потом поменяли на x и и не
1:01:16
должно быть в а вот здесь вот напишем что б не подлежит
1:01:21
а а вот здесь вот c не принадлежит д
1:01:27
вот это самое главное условие в правила бернайс а что это означает мы взяли
1:01:33
какую-то аксиому в ней нет переменной b но потому что
1:01:39
вообще не свободных переменных б что-то из этой аксиомы вывели с переменной b ну
1:01:44
вы хотя бы вот вот такое у или вот у вас тут появилась переменная b
1:01:51
тогда говорим мы ну раз это выявилось для любой любого значения b значит это
1:01:58
значит а можно вот так переписать что из-за следует для любого x btx вот это
1:02:03
просто обычно наши рассуждения когда мы говорим что да пусть n произвольно натуральное число поехали там что-то
1:02:09
выписывать и доказали что н всегда раскладываться по степеням простых основной теоремы их медики тогда говорим
1:02:16
мы для любого н н раскладываться по степеням просто то есть мы можем это
1:02:23
переписать в виде квартира по сути это означает в общем то определение того что
1:02:28
такое кванта если не если от переменной
1:02:33
b тут ничего не зависит это выводит у мы можем сказать что для любой байта верно то же самое здесь если мы
1:02:41
из вывели для при этом в c было переменная c of да и и не было то есть
1:02:48
мы вывели что то что значит не
1:02:55
не входи но как бы в да нет цвет который что-то зависит вот тогда говорим и но
1:03:02
раз мы при некотором цвета получили то можно сказать что существует c при котором выполняется такое следствие это
1:03:09
тоже по сути определение в общем то что такое квант орда если мы при каком-то
1:03:14
терме доказали значит можем написать существует x такой что c от x
1:03:19
ну и вот вот эти вот правило всего три модус понос и правила города со
1:03:25
позволяют нам генерить то что называется теоремами а именно ну давайте так ведем
1:03:32
определение выводам
1:03:37
в нашей теории ты даже не в теории это вообще формальным выводом называется вот
1:03:44
формальный вот это набор формул а 0 и так далее а.н.
1:03:52
вот такой ну просто некий конечный набор формул
1:03:58
где каждая из формул либо является аксиомой
1:04:04
причем сейчас не уточняем логическая геологическое какой-то аксиомой может быть у нас теория пустая и делаю вот
1:04:10
этой надстройки из не логических всем вообще нет то есть вы в чистом отчислении предикатов находимся не важно
1:04:16
у нас есть q это набора все значит либо
1:04:21
каждой из этих форм либо она является аксиомой либо оно получено из предыдущих
1:04:27
а это либо аксиома
1:04:33
либо а это
1:04:40
получено из а 0 и так далее а и минус 1 то есть из
1:04:48
предыдущих форму не обязательно из всех ну вот из из этого из-под множество
1:04:53
скажем так вот этих форм по правила вывода
1:04:59
то есть по сути мы можем было так взять либо а 0 а и минус 1
1:05:07
подчеркнуто а это вот так хотя здесь лучше было бы вся там
1:05:14
существует подмножество вот в этом наборе формул но просто правила вывода таковой что мы можем тут дописать любое
1:05:21
количество формул на самом деле и она сохраняется при этом все равно если
1:05:27
только конечно эти форму не будет противоречить предыдущем но поскольку они тоже выведены из из аксиом да то как
1:05:34
бы мы считаем что все непротиворечиво по крайней в той степени в которой аксиоматика непротиворечиво вот и
1:05:41
соответственно если у нас имеется вывод
1:05:47
вывод у нас отправляется от некоего борьба за во множество форума который мы
1:05:53
назвали аксиомами
1:05:59
то мы можем ввести такое отношение на между формулами и множествами форму если у нас
1:06:07
есть некое подмножество ты можешь считать его аксиоматика и можем просто каким-то подмножеством
1:06:13
значит в этом сам в замкнутых формулах да и если есть
1:06:20
формула а которая получена в результате вот этого вывода если
1:06:26
существует вывод а0 а.н. такой что а.н. это а
1:06:35
а все вот эти а 0 ну все вот эти формулы
1:06:40
то либо логически аксиома либо форму из набора т
1:06:46
либо получено поправила воды тогда мы пишем ты выводит а
1:06:54
вот тут по через такое отношение между набором формул и одной формой и вот это
1:07:00
отношение что пора но это как раз и показывает то что у нас имеет место вот такой вот паз правильно построили то
1:07:06
есть по правилам выводы мы это все получили значит если мы в этом выводе
1:07:12
вообще не использовали формулы множество ты не логические аксиомы точнее не использовали по сути ты была пустым
1:07:19
тогда мы просто говорим что а вы вадима имеется ввиду что среди аксиом были
1:07:25
только аксиом исчисления предикатов вот ну то есть те самые примеру
1:07:31
подстановок и значит 2 аксиомы с квартирами тогда мы упрощаем себе жизнь здесь
1:07:38
ничего не пишем потому что потом мы обычно подразумеваем какие-то предложения которые все-таки лежат вне
1:07:45
вот этого первого базового этажа который у нас вообще всегда есть тем самым а это тоже своего рода
1:07:51
сокращения ну и соответственно если ты эта теория то есть вот например там список аксиом
1:07:57
арифметики пеано там и говорил что вы арифметики пеано выводим а формула а потом что мы можем у нас этот значок он
1:08:05
относится как бы их сигнатуре и к на более аксиом арифметики пеано и мы можем сказать нам что в про вадима
1:08:12
и вот формула а это например будет основная теорема арифметики
1:08:17
это означает что существует такая цепочка она может состоять там деньгами из миллиона шагов вот но это конечная и
1:08:25
строго проверяемая на каждом шаге цепочка переходов от исходных формул к к
1:08:33
каждому каждом следующей формуле на этом шаге общем-то доказательства компьютерная
1:08:39
которая сейчас активно развиваются в мире они как раз вот основаны на исчисление высказываний правда не на
1:08:45
гилберта всколыхнуть мы описали гилберт орска исчисление высказываний обычно используются другие счисления типа там
1:08:51
sea queen циального ли что еще они просто получаются более экономные по вычислениям а так в принципе
1:08:56
если бы у нас был более шустрый компьютер мы могли бы и гербер царское исчисление высказываний тоже
1:09:01
использовать для получения теорем и сами математики именно гибель the screen to всегда и пользуются дкд когда доказывает
1:09:07
теорема знать что можно сказать про это отношение
1:09:13
выводимости но обычно говорят что а это теорема если ты эта теория то есть если
1:09:21
мы решили что наш набор формул это теория
1:09:27
что это теория да ну то есть она имеет какой-то сакральный смысл типа арифметики пеано elizade ft тогда мы
1:09:34
говорим что эта теорема ну то есть такая вот связка между словами теория и теорема
1:09:41
ну этого отношения есть главное свойство которое называется теоремой дедукции
Теорема о дедукции
1:09:52
она выглядит так если из множества формул т выводим а импликация наследует
1:09:58
б то точнее тогда и только тогда когда из вот такого множества форму
1:10:06
выводим а формула-б но предполагается что а и b замкнутой
1:10:12
формулы чтобы тут не косячить с определением аксиоматике вот хотя в принципе если там от
1:10:20
подстановки в свободный белье ничего не зависит то можно считать что и значит не только за то и формула говорит она то
1:10:27
что по сути доказать импликацию в системе аксиом то это все равно что в расширенной системе аксиом доказать
1:10:34
формулу бы опять таки пример со всем и выбора да если ты это у нас теория ztf
1:10:41
стандартная а это аксиома выбора об это теорема сумела
1:10:49
дата мы говорим что взятых верно импликация и за из аксиомы выбора
1:10:54
следуйте msr белом на самом деле город но сейчас не об этом то в теории z fc
1:11:00
вот это уже получается за твц теорема carmela является действительно
1:11:07
теоремой то есть она вот доказуемо в теории сытых c и это тогда и только тогда и здесь надо обратить внимание
1:11:14
выделю красной что вот эта эквиваленте я это
1:11:21
запись на уровне метаязык а то есть это не значок из нашей форме нашего формализма
1:11:29
формализме находится только вот эти вот две части а то что их связывает это уже утверждение нашей вышестоящий теории с
1:11:36
которой мы наблюдаем за вот этим вот массивом текстах состоящим из формул вот
1:11:41
это надо всегда четко отслеживать когда вы работаете см от лойко с формальными системами что нельзя забывать где уж где
1:11:49
у вас текст из изучаемой фарма не системы а где у вас значки обычные
1:11:54
математические значки означающее какие-то логические выводы на уровне это теории ну и под конец несколько
1:12:02
определений значит мы говорим что формула а не зависит от
Независимость формул, непротиворечивость и полнота теории
1:12:11
теории т а не зависит
1:12:17
если в теории т нельзя вывести а и нельзя вывести отрицание or и
1:12:27
кстати когда в ты выводится отрицание а да то есть не а является теоремой то
1:12:34
говорят что а провяжем а но это естественно такой такая
1:12:39
технология вот когда не доказуемо и неопровержимо то называется независимой от теории т
1:12:47
противоположный вариант этой ситуации это когда vt можно вывести а и можно вывести не
1:12:56
тогда у нас все плохо файл у нас получается что в теории т выводим на противоречия сигареты называется
1:13:03
противоречивый соответственно не противоречивая теория
1:13:10
date of которой ложь вывести нельзя по определению не противоречивая теория
1:13:15
обозначается конты но это такой получается как бы унарный предикат на множество теорий да мы уже
1:13:23
как бы опять находимся сейчас в мета языке и говорим что-то про свойство к
1:13:28
разных формальных теорий вот но строго говоря совместно с теорией то именно вот и вот
1:13:35
это вот обозначение заяца совместности орет и означает что у теории ты есть модель но мы чуть позже продемонстрируем
1:13:43
значит теорем которая покажется очень тест наличие моделей и непротиворечивость это одно и то же до
1:13:50
теорема геделя поэтому непротиворечивую теорию можно вот так вот обозначает что она совместно
1:13:59
ну и наконец теория называется полной теория полна как где-нибудь давайте
1:14:07
здесь напишем
1:14:15
теория полна если в ней любая замкнутая формула это ее же собственной сигнатуры
1:14:21
либо доказуемо либо а про режима
1:14:27
полная из для любой замкнутой формула
1:14:33
сигнатуры как сигма т выводит а
1:14:39
или ты выводит не а то есть вот все что мы тут можем
1:14:47
понастроить выводы из вот этого нашего блока аксиома не ведут к истинным формулам
1:14:54
причем из них можно выводить формулу с параметрами до всего вот той самой аксиома
1:15:02
получается что мы в полной теории мы по таким образом получим все истинные формулы и больше
1:15:09
того все ложные мы получим как их отрицание то есть вот переход сюда получается с помощью отрицания
1:15:17
ровно пополам просто разделим все формулы либо истинные либо ложны и
1:15:23
ну кроме формул с параметров с параметрами где параметры являются существенными конечно же то есть вот там
1:15:29
меньше либо равно это вообще не не может быть таскать недоказуемы и неопровержимое просто потому что здесь в
1:15:36
зависимости от параметров меняется истинность поэтому всегда лучше конечно всегда говорить о замкнутых формулах в
1:15:42
данном случае более того если у нас формула не из нашей сигнатуры например мы тут
1:15:47
использовали какой-то символ которого нет сигнатуре может оказаться что она не выводим а потому что мы это символ не
1:15:53
определили в этой теории тогда этот это не считается неполнотой теории потому
1:15:59
что какая-то залетная формула у нас образовалось вот так что полнота обязательно определять и замкнуты
1:16:05
формулу той же самой сигнатуры в которой задано такси амати к этой теории ну и
1:16:12
примеры полных теорий приведем как мы знаем арифметика пиана непала
1:16:19
например теорема густым является независимой а вот
1:16:25
потом мы построим еще один пример независимой формула а полные теории
1:16:36
ну во первых это элементарная геометрия тарского
1:16:45
вот элементарно geometry тарского хороша тем что она полностью описана в языке первого порядка там всего
1:16:51
11 axium она не сильно даже проще ночам аксиоматика piano
1:16:57
выглядит там никакой индукции нет вот она является полной то есть любая
1:17:03
формула в этой геометрии она либо доказуемо либо про режима любая замкнутая формула второе это теория алгебраически
1:17:11
замкнутых полей характеристики 0 греческие замкнутые
1:17:17
поля характеристики 0 стандартные примеры того что комплексных
1:17:23
чисел с операциями сложить умножить вот его речи сказал означает что любой многочлен имеет корень характеристика 0
1:17:32
означает что но нельзя получить как конечную сумму единиц в этой теории но ну там есть эквивалентно еще определение
1:17:38
можете посмотреть третье это вещественно замкнутая
1:17:44
вещественно замкнутые линейно упорядоченное [музыка]
1:17:50
поля тоже характеристики ноль значит существенно замкнутость означает
1:17:56
что любой многочлен нечетной степени имеет корень линейного порядочность
1:18:03
означает что операции поля согласованы с порядком ну и опять характеристика 0 то что 0 не получать как сумма единиц
1:18:11
вот типичный пример р значит с операциям плюс умножить и
1:18:17
порядком кого-то здесь у нас c с операции вы плюс
1:18:23
умножить а и там еще константа на заводить 01 здесь тоже соответственно 0 и 1
1:18:30
константы а и еще такой пример эта теория плотных
1:18:36
линейных порядков без 1 последних элементов линейные порядке
1:18:44
плотные без минимума и максимума
1:18:52
типично представитель вот и насколько я помню вообще все эти теории они
1:18:57
эквивалентны элементарные ковалентную вот этой теории на читку с порядком
1:19:08
тут очень важно что он очень плотно это когда между любыми элементами найдет с 3 и нет минимума максиму это тоже типа
1:19:16
плотности только там между бесконечностью и любым числом всегда найдется еще какой-то
1:19:22
вот ну вот такие незатейливая теории многих
1:19:28
иногда почуют смущаешь почему там по алгебре очки за три поля характеристики 0 это полна теории что можно любую
1:19:34
замкнутую форму либо доказать либо опровергнуть но тем не менее это так и
1:19:40
дальше мы уже перейдем к понятию модели
1:19:45
здесь вот уже появились у нас обозначения для моделей но в общем собственно говоря пора к этому
1:19:51
переходить так поговорим теперь о моделях формальных теорий значит предположим что
Модели формальных теорий, интерпретация термов и формул
1:20:00
у нас есть некое множество м.а. и
1:20:05
мы на этом множестве и можем рассматривать разные отношения
1:20:10
функции можем так условно обозначить пусть у нас f пусть p это
1:20:17
множество всех отношений на м
1:20:23
отношения на и напоминаю это подмножество в прямом произведение м на себя несколько раз
1:20:29
a&f красиво и это у нас будет множество всех
1:20:35
функций на м опять таки даже давайте
1:20:40
скажем что это не функции и операции сразу оговоримся
1:20:47
операции то есть это функция от нескольких аргументов пробегающих множество м и принимающих значение во
1:20:54
множестве м то есть отношение имеют вид вот такой это подмножество м.н. а
1:20:59
функция имеет вид из ммм где n это какое-то натуральное число если n равно
1:21:06
0 эту функцию можно считать константой значит и давайте теперь вспомним что у нас есть
1:21:13
сигнатура в которой у нас имеются константы
1:21:20
предикат ные символы и функциональная символы и
1:21:26
пусть у нас есть некоторая функция люк которая
1:21:32
задана на вот этих трех множествах то есть ее область определения объединение этих трех множеств и она работает там
1:21:40
следующим образом значит множество всех констант
1:21:46
сигнатуры сигма то есть значков каких-то для констан она переводит в сама
1:21:51
множество м то есть константам символом ставить соответствие какие-то элементы множества
1:21:57
м далее множество предикат ных символов она
1:22:04
переводит в.п. ну то есть в множество всех отношений
1:22:10
причем сохранением валентности обязательно то есть если я вот здесь вот поставлю н то есть возьму только
1:22:17
притекает ные символы валентности н то и здесь я беру соответственно тоже предикат ный символы валентности pen
1:22:23
точно также можно определить как мы все это определяли дальше ну и наконец все
1:22:30
функциональные символы она переводит ставите в соответствии какие-то функции из но что f красиво точно также
1:22:37
сохранением валентности то есть какое количество аргументов у этого функционального символа такое же
1:22:44
количество аргументов функции которая ему соответствует
1:22:49
тогда говорим мы вот эта функция называется интерпретацией нашей
1:22:56
сигнатуры в множестве м то есть определение такое получается ну
1:23:03
это интерпретация сигнатуры сигма на множестве м
1:23:14
ну далее мы можем взять области определения вот этого отображения сразу
1:23:19
же обозначить то есть скажем область все значения да вот
1:23:25
та которая принимает мир на предикат ных символах и тоже какие-то предикаты то
1:23:31
есть отношения на множестве м-мы это множество обозначим то есть образ
1:23:37
пред м ну и соответственно
1:23:43
функциональное символы переходят у множества funk м вот то есть короче говоря у нас
1:23:51
имеется некое соответствие не обязательно взаимно однозначное но как бы вот мы значит что-то поставили в
1:23:57
соответствии тогда у нас возникает на множестве м некая структура
1:24:02
математическая а конкретно алгебраическая структура
1:24:08
потому что это у нас имеется множество с отношениями и
1:24:14
функциями а точнее даже операциями вот то есть у нас возникает некая
1:24:20
алгебраическая структура мы ее обозначаем м красивая и мы говорим что вот эта вот н красивая есть не что иное
1:24:27
как модель сигнатуры сигма
1:24:34
модель сигнатуры сигма ну конечно же просто промоделировать вот
1:24:40
эти символы отобразить в какое-то множество это ничего не значит с этим надо что-то увидеть дальше делать им и
1:24:46
дальше это делаем а именно мы знаем что каждый term и каждая
1:24:53
формула сигнатуру заданной всегда туре сигма они имеют некая дерево разбора то есть мы знаем как они устроены строятся
1:25:00
через базовые вот эти вот понятия ну и соответственно мы можем все тоже
1:25:05
самое проделать уже теперь в данном героической структуре просто повторив выглядят как бы на дерево разбора
1:25:11
какой-то формулы re-therm а то есть например был на stand in a + b
1:25:18
сигнатуре соответственно мы можем взять и написать
1:25:24
сложение в какой-то модели если она у нас там за например сложению в сигнатуре
1:25:30
сигма даже может так вот явно написать пусть ему соответствует какая-то функция
1:25:37
от двух переменных ну например умножение действительных чисел
1:25:43
почему бы нет тогда соответственно вот этому дерьму будет соответствовать
1:25:49
умножение она б ясный момент здесь надо еще сказать о том что у нас сигнатуре
1:25:55
были переменные вот я напоминаю у нас были значит свободные переменные
1:26:00
abcd там и так далее и зам на связанные переменной x y z который мы еще
1:26:08
обозначали там с индексами x0 и x1 x2 и так далее свободно его 0 1 и так далее
1:26:14
их тоже надо сопоставить переменным переменном же тоже в модели м и вот
1:26:22
сопоставление переменных тут обычно делается так сопоставляет один в один то
1:26:27
есть если было переменная of сигнатуре сигма то и в модели мы тоже берем в
1:26:33
интерпретации мы берем соответственно переменная с теми же обозначениями но конечно смысл них при этом другой почему
1:26:41
потому что здесь это были просто значки для обозначения переменных а здесь это
1:26:47
переменные уже так сказать в теории множеств которые имеют ограниченную область
1:26:53
действия вот тут надо как бы принципиальную разницу понять в том что если у нас было в сигнатуре сигма
1:27:00
переменная а мы поставили в соответствии некоторую переменную а скажем так м которая
1:27:09
сигнатура в модели м находится имеется в виду что это переменная имеет
1:27:17
право принимать значения только из множества м то есть всякий раз когда мы
1:27:22
рассматриваем формулу с интерпретациями переменных мы должны помнить о том что эти
1:27:29
переменные не могут выходить за рамки множество pen поскольку мы это все погружаем на самом деле как бы формализм
1:27:36
теории множеств да а в теории множеств есть только один вид переменных эта переменная пролегающий все множество
1:27:42
вообще и тут надо не путать что вот это вот эта переменная она имеет как бы другой сорт что или другой тип но тем
1:27:48
кто хорошо знаком с языками программирования и понимаю да что есть разные сорта или типы переменных есть
1:27:55
там целочисленные булевских текстовые так далее вот и тут мы как бы получается обзаводимся новым типа переменных в
1:28:02
нашей метод теории что это означает это означает что когда мы пишем какие-то кванторы по этим
1:28:08
переменам новых например для любого а и а это интерпретация переменной а то мы
1:28:16
должны его заменить на самом деле на квартир для любого а из м по сути в этом и есть разница только
1:28:23
опять таки я здесь написал свободную переменного по хорошему надо было бы написать
1:28:29
связано переменная вот а для свободных тоже соответственно
1:28:34
мы должны понимать что свободы только поэм бегают у нас ну это такое достаточно тонко отличие просто надо
1:28:41
всегда держать в голове это записывать можно в принципе также как мы в исходную сигнатуре сигма все это дело
1:28:47
пишем вот таким образом имея интерпретацию
1:28:55
переменных и всех базовых наших констант предикат ных символов функциональных
1:29:00
символов мы можем проинтерпретировать любой тиром и формулу нашей теории ну
1:29:06
например что мы делаем с фирмами пусть у нас есть
1:29:11
какие-то термы т1 и так далее т.н. это термы
1:29:20
заданной всегда туре сигма и пусть мы уже построили для них интерпретацию в
1:29:26
модели м значит мы вот так вот напишем что у нас задано интерпретация
1:29:32
в модели тем когда мы подчеркиваем где мы их
1:29:37
интерпретируем и вот значок этой модели ставим как бы на место степени вот тогда
1:29:44
да и пусть у нас имеется некий функциональный символ
1:29:53
заданный в сигнатуре сигма и мы его про интерпретировали какой-то функцией в
1:29:59
модели м то есть у нас есть интерпретация для этих термов у нас есть интерпретация для функционального
1:30:05
символа пев соответственно комп тогда кому тогда мы говорим что композиция
1:30:10
фмрт 1-м и так далее т м м
1:30:15
это ничто иное как интерпретация
1:30:22
интерпретация derma-e под т1
1:30:27
т.н. вот короче говоря о просто следуя
1:30:32
рекурсивный правилам которые задают нам термы и формул и мы точно так же строим интерпретации для этих самых
1:30:39
термов и форму отправляясь от базовой интерпретации
1:30:45
для форму соответственно все ровно то же самое включая
1:30:51
формулы с квартирами единственное что как я говорил там когда у нас идет кванта попеременной то переменная должна
1:30:57
быть должна прибегать строго множество м и не выходить как бы за его пределы вот
1:31:03
ну например если мы давайте уже построим интерпретацию арифметики пеано
1:31:09
я напоминаю что в пиала у нас сигнатура выглядит так
1:31:15
там у нас есть символ 0 константный там у нас есть отношение равенство 2
1:31:23
бинарных операции сложения умножения и 1 унарная операция которая называется последовательно и
1:31:29
вот а далее нам нужно эту сигнатуру проинтерпретировать в некой на некотором
1:31:37
множестве м естественным образом мы берем то ту интерпретацию натуральных
1:31:43
чисел которую мы в теории множеств знаем да в классическом варианте а именно мы в качестве м
1:31:49
берем орден all омега 1 бесконечно arden all дальше значит нулю мы поставим
1:31:57
соответствие пустое множество отношению равенство в арифметике ну тут
1:32:04
правильно опять-таки писать вот такой по мы ставим соответствие равенство в теории множеств
1:32:11
сложению впо мы ставим соответствие сложения ордена
1:32:17
love суженая естественно на arden ала миго умножение в по мы ставим соответствие
1:32:26
умножение ордена love ну и вот этой функции унарный последовательно мы
1:32:33
ставим соответствие вот такую функцию которая у нас была при когда мы
1:32:38
рассматривали оргинал и альфа объединить с точкой альфа которая как мы выяснили потом это ровно
1:32:45
то же самое что альфа плюс ординарный + 1 где 1 это фигурные скобки
1:32:52
0 ну то есть следующий за рулем орден all ну короче говоря мы производим простые
1:32:59
решение вещи нулю ставим соответствие 0 равенство равенство сложению сложения и
1:33:04
умножения умножения и + 1 ставим соответственно + 1 по сути вот так и в итоге мы получаем то что называется
1:33:11
стандартной моделью то есть множество
1:33:18
омега у нас является носителем модели
1:33:23
равенство это равенство плюс это плюс умножения это умножение и с это с ну вот
1:33:30
вот вот тот самый альфа объединиться альфа с точкой альфа
1:33:36
то есть конкретная совершенно алгебраическую структуру определенно она ардена ли омега причем именно та самая
1:33:43
которую мы изучали когда рассматривали кирпич кардиналов собственно говоря и вот все вместе это называется
1:33:50
стандартной моделью и является интерпретацией арифметики пеано ну можно
1:33:55
проверить до что это тут действительно ведь этим бинарные операции это бинарное
1:34:00
отношение это ударная операция все все у нас на месте более того
1:34:06
соответственно мы можем еще и аксиомы этой теории нашей pianta же проверить что и выполняются стандартной модели но
1:34:13
об этом чуть позже значит поскольку мы умеем не только базовые символы но и все формулы
1:34:20
интерпретировать в нашей модели мы вот тоже вот так будем обозначать звуков крем
1:34:31
если у нас есть какой-то term из множества термов сигнатуры сигма
1:34:39
там ему ставим соответствие term вот такой который является некоторой
1:34:46
конструкции собранной из переменных и функций уже в модели м как это делается
1:34:52
я вот только что на предыдущем шаге показывал соответственно если у нас есть какая-то формула а и
1:34:58
сигнатура сигма это может быть формула с параметрами кстати необязательно замкнутая там и есть ставим соответствие
1:35:05
формулу а со значком м и вот это будет уже формула которая по сути записано в
1:35:12
общем-то на языке эта теория то есть на языке теории множеств вот но с некоторыми ограничениями самое главное
1:35:17
ограничение заключается в том что переменная пробегает только множество м то есть у нас выделен особый класс
1:35:24
переменных ну и значит помимо логических связок и
1:35:29
кванторов там используются атомарные предикаты и атомарные функциональные символы и они и и только
1:35:36
они ничего лишнего там быть него там не может быть значка объединение множества мне может быть значка принадлежности вот
1:35:44
что там что не может быть power set какого-нибудь то есть множество всех подмножеств и тогда я то
1:35:50
есть весь этот арсенал теории множеств который на самом деле можно было бы в этой модели применить мы не используем
1:35:58
мы его оставляем за кадром потому что когда мы работаем в интерпретации мы можем пользоваться только значками из
1:36:04
сигнатуры сигма а точнее их интерпретациями в этой сигнатуре вот
1:36:10
ну например термы
1:36:16
формальной теории пиана в этой модели в стандартной модели это просто напросто некий многочлена потому что у нас
1:36:24
разрешены только операции сложения и умножения они позволяют только соответственно складывать какие-то простейшие
1:36:31
конструкции друг на друга умножать вот ну многократно умножение одного и того же это просто по определению степень
1:36:37
поэтому получается что все термы некоторые заодно в арифметики пеано здесь это какие-то многочлены которые
1:36:45
заданы соответственно в стандартной модели
1:36:51
так ну и вот определившись с терминами так сказать мы можем дальше пойти таком
1:36:59
направлении
1:37:05
про формулы которые мы про интерпретировали
1:37:10
и сигнатуры в нашей модели мы можем говорить о том истинно не или ложное в этой модели уже с точки зрения теории
1:37:17
множеств то есть ну с точки зрения мета теории ну например мы взяли какую-то формулу из арифметики пеано
1:37:26
ну скажем простейшая формула 0 меньше чем с от 0
1:37:32
эта формула не так 0 не равно давайте пока что неравенство оставим в покое
1:37:40
но не равно из от 0 это кстати одна из аксиом арифметики пеано это формула
1:37:48
правильно построена формула в нашей сигнатуре у нас есть константа у нас есть ударный удар и функциональный
1:37:54
символ вот соответственно ей соответствует формула
1:37:59
вот мы и так запишем а это вот такая формула тогда а в стандартной модели
1:38:05
это формула пустое множество не равно пустое множество объединить с такой
1:38:14
штукой ну как видим она действительно истинно стандартной модели это следует
1:38:20
вот это следует уже из аксиом теории множеств да я кстати говорил что мы не используем значок объединения но
1:38:26
поскольку мы с про интерпретировали именно вот так то в данном контексте можно использовать значок объединения но
1:38:33
лучше вообще сразу от него избавиться используя здесь alpha + 1 как сумму
1:38:38
ордена love вот тогда нам не придётся оговариваться где это значок можно ставить окей нельзя
1:38:43
вот но так сказать в базовых символах мы это все определили и мы видим что действительно вот эта формула истинна в
1:38:51
нашей арифметики пеано и ее интерпретация истинно в стандартной модели так вот
1:38:58
главное определение которое мы здесь видим это так называемый двойной штопор мы
Истинные в модели формулы
1:39:05
говорим что в модели м тут кстати ли чаще всего пишут сам носитель модели
1:39:11
множество м но чисто логически правильно было бы писать именно вот это вот
1:39:16
обозначение для модели вот такой двойной штопор обозначает что
1:39:22
формула а истина в данной модели мы здесь не
1:39:28
оговариваем есть ли у а свободной переменной или нет поэтому когда вот так пишем мы это означает что
1:39:35
при любых постановках вместо свободных переменных каких-то элементов но что м она будет
1:39:41
истина то есть это как бы как логическая функция тождественно равна единице на
1:39:47
множестве вот ну чаще всего это конечно запись относится к замкнутым формулам то
1:39:53
есть просто она может быть либо истина либо ложно и вот эта запись обозначает что формула а а даже
1:40:00
часто даже вот это не пишут обозначения тут получается такая такое смешанное
1:40:07
обозначение формула берется и сигнатуры а модель это модели мы говорим что эта
1:40:12
формула истинна в этой модели имеется в виду конечно что в модели истинно интерпретация этой формулы именно вот
1:40:20
такая ну и соответственно если какой-то набор формул
1:40:26
вот мы взяли вот эти наши формулы сигнатуры сигма мы их про
1:40:33
интерпретировали можем вот так вот написать да это все
1:40:38
интерпретации формулу из множества т но
1:40:43
и мы говорим что множество формул ты сигнатура сигма истинно в модели м если
1:40:52
для любой формулы а из нашего т в модели м истинно
1:41:00
формула а вот просто такое расширение этого определения двойной штопор
1:41:06
значит опять таки возвращаясь к формулам у
1:41:12
которых есть свободная переменная может оказаться так что какая-то формула определенная в нашей сигнатуре вот мы и
1:41:19
про интерпретировали в нашу модель и оказалось что при каких-то значениях переменных оно истинно а при каких то
1:41:25
оно ложно если она хотя бы при каком-то значении аргумента истинно
1:41:32
модели and a говорят что формула выполнимо в данной модели ну а если
1:41:38
говорят что просто формула выполнимо это означает что есть какая-то модель в которой она выполнима и наконец
1:41:45
формула является тождественно ложной а то есть вообще не выполнимой да если ее
1:41:55
отрицание выполнимо хоть в какой-то модели вот но это такая обычная условная
1:42:00
терминология связывающая так сказать понятие истинности им
1:42:05
для ну для какие-то случаев в конкретных и так теперь у нас получается имеется
1:42:12
двойной что парах и одинарный штопор напоминаю одинарные штопор означает что
1:42:17
что то выводим а в теории независимо от того какая там он есть или нет
1:42:22
интерпретация в этой теории то есть мы вот имеем некоторую сигнатуру имеют
1:42:28
некоторую теорию и в этой парочки у нас есть отношения штопор который означает
1:42:35
что из какого-то набора формул вадима такая-то формула проста по правилам
1:42:40
логики безотносительно привязки к какой-то общий конкретной интерпретации с другой
1:42:45
стороны если мы к нашей сигнатуре удачно привязали некоторую модель
1:42:51
в этой модели мы можем говорить об истинности или ложности формул об
1:42:57
этой самой сигнатуры вот вот эти два что пора у нас появляются между ними есть
1:43:04
некое таинство то эстафеты сказать взаимосвязь да еще надо сказать что поскольку мы вот этот что пар двойное
1:43:11
определили именно как истинность у нас действует закон исключённого третьего соответственно всякая формула в данной
1:43:18
модели она может быть либо истина либо ложно третьего не дано и вот ложность
1:43:25
как бы истинность отрицания формула обычно обозначают просто перечёркивая этого штопора то есть здесь не возникает
1:43:32
такой тройственная ситуации что бывает формулы которые истины бывают форму которые ложно а бывают формула которые
1:43:39
ни то ни сё нет в модели всегда мы предполагаем что форума либо истина либо ложно и поэтому это отношение она
1:43:46
получается как бы более сильным чем отношении выводимости
1:43:51
ну и теперь собственно говоря нам нужно установить некую связь между вот этими
1:43:58
стопорами а именно я приведу ряд теорем о моделях в которых мы вот
1:44:06
кое-что об этом скажем но перво-наперво конечно же у нас есть
1:44:15
теорема о том что если что-то выводим а в теории а
1:44:21
теория имеет модель то теоремы этой теории они обязаны быть истинными в
1:44:26
данной модели ну иначе получился получать какой-то абсурд ну а стадо выводилось никак не коррелирует с
1:44:33
понятием истинности в модель поэтому есть такая теорема о корректности
Теорема о корректности исчисления предикатов
1:44:40
о корректности отчисления предикатов она
1:44:45
выглядит следующим образом пусть m это модель теории т да я забыл сказать что если мы взяли
1:44:54
какую-то сигнатуру взяли набор формул замкнутых то есть ну например axiom очку
1:45:00
теорий тему взяли и эти все аксиомы оказались истины в модели в данной модели то мы говорим что
1:45:07
это модель является моделью нашей теории т частности вот это самая такая
1:45:14
стандартная модель мы знаем что они выполняются все аксиомы арифметики пеано которые ранее выписывал а значит
1:45:22
стандартная модель это действительно модель арифметики пеано первого порядка так вот
1:45:27
пусть у нас модель это пусть м эта модель теорий т и кроме того в
1:45:34
теории т доказуемо некоторая формула а тогда говорим мы
1:45:42
в модели м будет истинной формула а вот тут мы видим как раз
1:45:49
согласование выводимости и истинности из выводимости следует истинность
1:45:56
ну доказывать и теорема не буду потому что у нас очень тут еще много предстоит
1:46:03
теорем всяких разных но коротко суть в том что мы здесь будем пользоваться
1:46:10
например можно воспользоваться теоремой а дедукция а также разбором этой формулы
1:46:16
по по ее этому самому по дереву дерево разбора то
1:46:21
есть мы действуем индукция по сложности формула и отталкиваясь от базовых
1:46:28
предикатов и вот axium соответственно да мы доказываем что если формула выводим а то
1:46:35
она будет обязательно истина в этой модели верно ли обратно и возникает сразу же вопрос вот обратно естественно
1:46:43
неверно точнее верно не всегда почему потому что мы прекрасно знаем что если мы возьмем например теорему гостей на
1:46:49
она будет у нас стандартной модели истинно но при этом она не доказуемо в
1:46:56
арифметики пеано потому что когда мы доказывали терем густые до стандартные модели она формулируется как раз
1:47:02
стандартной модели мы вышли за пределы стандартной модели вот тут мы как раз использовали такой как бы читерский
1:47:08
прием да не то чтобы доказать эту теорему мы взяли продолжили нашу стандартную модель за кардинал омега
1:47:16
использовали такие понятия как подмножество вполне упорядоченность которых нет не можешь быть в арифметики
1:47:24
пеано и использовал этот расширенный аппарат мы доказали теорему good стрельна поэтому
1:47:31
она в этой модели истина но к сожалению она не доказуемо вот что подчеркивает
1:47:36
свою не палату арифметики пеано дальше отсюда следует например следующие
1:47:43
следствие один если теория имеет модель то она непротиворечиво
1:47:51
если существует модель теории
1:48:05
ттт непротиворечиво
1:48:11
ну почему так доказывается от противного предположим что ты противоречиво противоречивость означает что в ты
1:48:19
выводим а противоречия доказательство от противного получается
1:48:28
пусть в.т. выводим а ложь тогда по предыдущей теореме получается что в
1:48:34
модели м истинно ложь но тогда у нас сама модель получается противоречивой а
1:48:40
мы когда работаем в какой-то мета теории а точнее в теории множеств мы предполагаем что конечно же не пустое
1:48:47
множество она не может быть противоречивым вот если бы мы взяли в качестве моделей пустое множество но мы
1:48:52
договорились что мы не берем пустое множество количество моделей тогда да в пустом носите все что угодно мой можно
1:48:57
отыскать считать истинным потому что там ничего нет но существование моделью теории имеется
1:49:04
ввиду конечно же не пустая не пустой носитель модели вот они в не пустом
1:49:09
носите не может быть истинной сложная формула это тогда получается
1:49:14
противоречие уже в самой мета теория в теории за твц но мы предполагаем что теория z fc
1:49:20
непротиворечиво просто потому что она является воплощением наших как бы
1:49:25
способов рассуждений да потому что она оно по сути является воплощением того как мы что-либо
1:49:33
конструируем и доказываем в математике то есть противоречивое за тв по сути отменяет нам на всю математику ну
1:49:41
покрайней мере значительную часть с другой стороны
1:49:46
есть теории у которых модели очень простые то есть они ограничиваются конечными множествами ztf точнее
1:49:53
наследство на конечным деле тем те которым не требуется к бесконечности вот и в этом случае можно не ссылаться
1:50:00
непротиворечивости время что ссылаться на что-то более понятное ну например если взять теорию групп что у нас там у
1:50:07
нас там очень простая сигнатура там всего лишь операция умножения и
1:50:12
равенства и значит ряд простейших аксиом это
1:50:18
ассоциативность этой операции это аксиома единиц максимум обратного элемент и если мы в качестве модели
1:50:26
теории групп вот давайте так вот теория групп отзовем грп значит моделью теории
1:50:33
групп является любое одноэлементные множество какое угодно вот возьмите какой карандаш
1:50:41
назовем это буквой а и то есть 1 элемент на множество
1:50:48
она будет над моделью теории групп простейших группа да и состоящее из
1:50:53
нового элемента соответственно тогда получается что теория групп непротиворечиво если только непротиворечиво существовании нашего
1:50:59
карандаша и такие уже совсем даже можно сказать не математическое
1:51:05
рассуждение тем не менее на таких как для конечных рожь в случае существании конечных моделей всего вообще очень
1:51:12
просто и не вызывает никаких вопросов плане непротиворечивости вот но в общем случае до имеется ввиду что если мы
1:51:20
нашли какую-то модель там это мы предполагаем что это какое-то множество это множество находится в нашей мета теории и мы всегда изучая формальные
1:51:28
системы предполагаем что уж нас томит а теории она обязательно непротиворечиво иначе просто не о чем говорить
1:51:34
еще одно следствие которое можно отсюда извлечь это собственно говоря о прощении теоремы
1:51:42
в обратную сторону то есть поправила контр позиции мы можем заключить что
1:51:52
если у нас тэм модель теории т и
1:51:58
какая-то формула не выводим а в теории т
1:52:03
то тогда эта формула должна быть ложной в нашей модели ну просто очевидно потому
1:52:13
что если она так только конечно же наоборот
1:52:20
конечно же наоборот
1:52:25
если у нас какая-то формула ложно в модели то тогда говорим и что она в этой
1:52:33
теории не выводим а вот этой теоремы можно сказать
1:52:40
воспользовались еще тогда когда доказывали независимость пятого постулата ну допустим у нас теория т эта
1:52:46
геометрия так называемая
1:52:52
абсолютная геометрия то есть геометрия без пятого постулата без пустота лобачевского то есть первые четыре
1:52:58
постулата только формализованные виде аксиоматике тарского вот а это пятый постулат например тогда
1:53:07
мы берем модель абсолютной геометрия в которой пятый постулат ложен например
1:53:12
модель пуанкаре или модель клей на beltrami вот строим эту модель
1:53:18
оказывается что пятый постулат там не выполняются и тогда мы говорим что тогда
1:53:24
в нашей абсолютной геометрия пятый постулат не доказуемо
1:53:29
тоже самое относится к отрицанию пятого постулата форме
1:53:35
лобачевского да то что значит существует бесконечно много параллельных кривых
1:53:41
проходящих через одну и ту же точку параллельных данной кривой тоже мы можем
1:53:47
взять в качестве моделей обычная плоскость r-квадрат там выполняется пятый постулат соответственно не
1:53:53
выполняется аксиома лобачевского соответственно все малого часто не будет выводим а из
1:53:59
абсолютной геометрии таким образом получается что и пятый постулат и его отрицание форме лобачевского эта формула
1:54:06
минуты с co2 аксиомы которые не зависят от абсолютной геометрии с помощью метода
1:54:12
моделей мы показываем независимость некоторых форму от аксиоматике достаточно просто предъявить конкретные
1:54:19
модели ну и теперь собственно говоря то о чем я
1:54:25
ранее говорил о так называемой понятие совместности
1:54:31
теории и о том что это ровно то же самое что
1:54:37
непротиворечивость мы можем еще раз по определению сказать что теория совместно
1:54:46
consisted если существует модель в которой оно истинно
1:54:55
ну и мы знаем да что если вот собственно вот по этой теореме написано что если
1:55:01
теория совместно то есть имеет модель тогда она непротиворечиво вот вследствие
1:55:07
один из теорема оказывается верно и обратное это ничто иное как теорема геделя упал
Теорема Гёделя о полноте
1:55:14
на те так называемая полнота в том смысле что
1:55:21
просто эти понятия эквивалентны есть несколько вариантов этой теоремой там
1:55:26
немножко по-другому формулируются через другие понятия ну вот один из вариантов я привожу теорема году я полноте
1:55:33
формулируется так если теория непротиворечиво
1:55:42
если ты непротиворечиво
1:55:48
то она имеет модель то существует модель теории ты
1:55:55
снова обращаю внимание на то что вот это вот существует я пишу в нашей мета теории они в каком-либо формализме то
1:56:02
есть по хорошим я продолжим вот слова и писать на мне просто лень вот и таким образом вместе вот эта
1:56:08
теорема вместе со следствием один говорят нам о том что по сути совместность теория и июня
1:56:16
противоречивость это одно и то же поэтому непротиворечивость очень часто и
1:56:21
обозначаются именно как consisted доказывается эта теорема теорема очень
1:56:29
интересным способом то есть что здесь требуется взяли какой-то непротиворечивую теорию надо построить
1:56:35
ее модель в качестве моделей берут берется не что иное как сами символы сигнатуры
1:56:41
вот мы считаем некими объектами нашей мета теории
1:56:48
вот а значит это какие-то множество раз это множество то мы можем на этом можете
1:56:54
взять учет смоделировать ну и далее там идут сложные рассуждения там по по индукции и так далее в общем интересно
1:57:01
теорема советую всем ее изучить и еще одна теорема о моделях которая нам в
1:57:08
принципе не понадобится но достаточно интересная эта теорема лювин game as кулёма на
Теорема Лёвенгейма-Сколема
1:57:14
самом деле это две теоремы сейчас поясню почему теорема
1:57:23
верна гейма с кулёма значит в русской традиции
1:57:29
пишутся колемана самом деле это фамилия читается как с cullen по-моему датский
1:57:35
математик в принципе сюда можно еще отнести
1:57:45
ну да значит а формулируется следующим образом и
1:57:50
причем я формулирую в общем виде если
1:57:56
теория t имеет бесконечную модель
1:58:04
бесконечную модель то она имеет модель любой бесконечной
1:58:09
мощности то она
1:58:15
имеет модель
1:58:21
любой бесконечной
1:58:29
мощности ну например вот наша стандартной арифметика пиана
1:58:37
она имеет ее стандартная модель это орден all омега это счетный ординат на
1:58:44
самом деле как оказывается можно предъявить и например континуальной модель химически пиана или там как у
1:58:51
супер континуальная модель арифметики пеано благодаря этой теоремы теореме и
1:58:56
наоборот если у нас есть какая-то континуальная модель например модель геометрии это плоскости р квадрат
1:59:03
понятно что ты континуум мы можем ее заменить на счетную модель вот-вот
1:59:10
обычно когда говорят теорема любим game as кулёма имеют ввиду теорема о понижения мощности то есть если теория
1:59:16
ты иметь какую-то бесконечную модель то она обязательно будет иметь и счетную модель вот на вторая теорема это как раз
1:59:24
теорема о повышения мощности если теория имеет какой-то бесконечную модель то она имеет модель любой большей мощности и
1:59:31
так далее ну простейшие примеры я вот так что про арифметику piano сказал да у нас есть еще так называемо теория от f0
1:59:40
это теория алгебраически замкнутых полей
1:59:46
характеристики 0 которая по сути является теорией комплексных чисел
1:59:51
значит с константами 01 операциями плюс умножить вот
1:59:58
понятное дело что вот это я написал алгебраическую структуру которая строится через р квадрат обычное
2:00:06
определение комплексных чисел через существенное вот там мимо единичка водится и так далее
2:00:11
это естественная модель является континуальной но у нее есть
2:00:17
вполне себе хорошо знакома всем модель счетное а именно алгебраические числа комплексные алгебраические числа
2:00:27
это счетное множество и она является моделью алгебраически замкнутых power
2:00:32
характеристики 0 вот если говорить о геометрия евклида например то стандартная моделью для
2:00:40
геометрии евклида является плоскости р квадрат заодно и через вещественные числа но если мы возьмем и
2:00:49
все координаты плоскости будем брать из множества алгебраических чисел то есть
2:00:55
алгебраических вещественных чисел то есть мы отсюда переходим к множеству пар икс игрек
2:01:03
где x и y оба во-первых вещественные во вторых
2:01:09
алгебраические то мы получим счет на множество и это
2:01:15
счет на но что будет являться счетную моделью для
2:01:20
элементарной геометрии ну такие разные интересные вещи да можно
2:01:26
может возникнуть вопрос о том а как же быть с формальной теории за твц с теории множеств как так в не может быть некая
2:01:33
счетная маршрутная модель действительно счетная моделью строится вполне себе
2:01:39
понятным образом дело в том что там получается так что вот эти все понятия
2:01:45
степенного множество континуум и так далее они редуцируются некоторым образом то есть по сути у нас
2:01:52
какие-то множество вообще выпадают из этой модели и все что мы там строим и строим неким
2:01:58
конструктивным образом дамы строю множество всех подмножеств но в этом множество всех подмножеств много чего как бы нет я потому что мы их
2:02:05
конструктивно указать не можем у нас там есть только конструктивные элементы и поэтому получается что модель
2:02:14
удовлетворяет аксиомам ctf но при этом оно счетная
2:02:20
соответственно отсюда как бы вроде бы получается
2:02:26
непротиворечивость зато в цену делов точно доказывается внутри самой за твц более того можно строить модели
2:02:33
да и и причем эти модели они строятся в более сильной
2:02:39
аксиоматике мы знаем что в самой аксиоматике за 3цет оказать непротиворечивость ее самой же
2:02:44
невозможно собственно это и есть строителем году я неполноте который мы идем вот но если мы
2:02:50
зато все усилим например добавим туда аксиому строго недостижимого кардинального числа
2:02:56
это аксиома позволяет нам построить некий универсум ztf который
2:03:02
смоделировать на все ок самочку ztf тем самым мы в более сильной теории в расширенной уметь доказывать
2:03:08
непротиворечивость исходной теории что конечно ну или с таким порочным кругом в
2:03:13
общем-то да или бессмысленно больше того и непротиворечивость самой добавление
2:03:19
самой аксиома и сайт тоже можно пробовать доказать если добавить туда еще какие-то более сильные аксиома
2:03:25
и так дальше вот
2:03:30
ну в основном до вас но все это дело с моделирования сводится к обычным предъявлением моделей в стандартной
2:03:37
математики следующее что мы хотим здесь понять это так сказать
2:03:45
понятие определим асти или представим остине которых отношении функций в
2:03:50
модели мы вот мы когда строили интерпретацию нашей сигнатуры вот это
2:03:56
вот мы делали следующую операцию мы от сигнатуры переходили к не которому
2:04:03
множеству и интерпретировали наши значки сигнатуры в
2:04:08
каком-то конкретном носите в теории множеств может возникнуть вопрос об обратные
2:04:14
операции а что если мы значит в нашей модели в стандартный
2:04:21
например даже если брать арифметику пиана стандартная модель физики пиана мы взяли и чего-то определили какое-то
2:04:27
отношение какую-то функцию и мы хотим понять а можно ли
2:04:33
это отношение и функцию записать в нашей сигнатуре в исходной
2:04:41
ну для начала мы ведем следующее понятие пусть у нас есть модель
2:04:49
модель сигнатура сигма мы
2:04:54
возьмем и множество всех констант сигнатуры добавим все элементы множества
2:05:00
н то есть мы вот переопределим так сказать константы
2:05:06
сигма определим как константы сигма
2:05:12
объединить с множеством темп и вот эти элементы но что мы объявим
2:05:19
значками для новых констант которые сами себя и будут обозначать полученная сигнатура обозначается как
2:05:26
сигма вот тема и называется расширенной сигнатуры мы ее расширились за счет
2:05:32
добавления туда новых значков для константа например можно брать скажем
2:05:38
там чего вещественных полей сейчас на золотых полей вот у них есть модели
2:05:44
стандартную модель р мы можем туда присоединить константы всех действительных чисел и тем самым за
2:05:49
будет такая гигантская уже сигнатура континуальная значит сразу хочу сказать что в случае
2:05:56
со стандартной моделью арифметики пеано в принципе это делать не обязательно потому что если мы возьмем
2:06:07
натуральные числа из омега вот мы берем вены за мега им будет соответствовать на
2:06:12
самом деле вот такая вот конструкция в нашей сигнатуре в стандартной
2:06:18
сигнатуре в не расширенной сигнатуре арифметики пеано где с повторяется и нас я ранее уже говорил что мы такие вот
2:06:26
штуки будем обозначать н подчеркнутая и называть номер алами так вот в общем-то
2:06:32
сигма от стандартной модели расширения сигма
2:06:37
на стандартную модель это просто теория в которой
2:06:44
в качестве констант константы в этой расширенной сигнатуре
2:06:50
это просто все numeral и ну 0 подчеркнуто это со мной потому что
2:06:58
он у нас уже есть а все остальные это вот вот такие штуки на самом деле случае арифметики натуральных чисел и
2:07:05
стандарт и расширение за счет константой стандартной модели в принципе можно даже сигнатуру и не расширять потому что там
2:07:11
у нас уже введены вот такие по определению значки мы просто можем их каждый раз заменять на такую конструкцию
2:07:17
и тем самым сводить все к исходной сигнатуре для вещественных чисел понятное дело это не пройдет потому что
2:07:23
там просто символов не хватит на все эти вещи ну и теперь возвращаемся к нашему
2:07:28
вопросу о том что вот допустим у нас есть какой-то предикат а вернее отношения из
2:07:34
на множестве м произвольная да
Выразимость предикатов и функций в сигнатуре
2:07:41
верно ли что
2:07:46
есть некоторая формула а из нашей сигнатуры пусть будет расширенная
2:07:54
сигнатура запасом так сказать значит
2:08:01
такая что а.м. это и есть наш п то есть
2:08:08
как бы интерпретации этой формулы является прийти к т ну точнее областью истинности
2:08:15
конечно про я не говорить область истинности формулы вот это interpreter интерпретации
2:08:20
формула является предикат п но общий ответ конечно же нет потому что если м это бесконечное множество пусть даже это
2:08:26
счетное множество да как в случае натуральных чисел вот этих всех подмножеств их континуум но что
2:08:33
подмножеств натуральных чисел даже если мы только унарный предиката рассматриваем континуум а всех формул в
2:08:40
нашей сигнатуре даже пусть и расширенные сигнатур бесконечно с защитным чехол констант вода их всех формул их счетный
2:08:47
набор понятное дело что всех фору умер от а со всех формулах и сигнатуры просто не хватит на то чтобы выразить все
2:08:54
предикаты которые мы можем определить пользуясь средствами теории множеств то есть
2:09:01
нашими то теории в модели кем то есть есть очень много почти все предикаты
2:09:07
которые можем задать средствами внешней теория неопределимое в нашей сигнатуре
2:09:12
вот но поэтому имеет смысл ввести такое определение
2:09:18
мы говорим что предикат
2:09:24
определим или как еще говорят выразим
2:09:29
определим или выразим в вот такой расширенная сигнатуре
2:09:39
или иногда еще говорят в паре сигнатура сигма и модели м вот если
2:09:48
существует формула а из множества форму нашей сигнатуры
2:09:56
расширенной сигнатуры такая что произвольный вектор значит для любых для
2:10:03
любого вектора давайте так любых переменных
2:10:10
c1 цнс м вектор и набор c 1 ц н
2:10:19
принадлежит нашему предикату п тогда я только тогда когда
2:10:26
истина вот это вот формула а у
2:10:32
давайте подчеркнем что и что мы работаем с интерпретацией форму и а в которой мы
2:10:37
соответственно вместо свободных переменных
2:10:43
1-ой он подставили вот эти вот константы
2:10:49
сейчас вот так напишем подставили наши вот эти константы то
2:10:56
есть мы что хотим сказать что мы взяли какой-то предикат нашли формулу и
2:11:03
оказалось что если мы в эту формулу подставляем наши константы и сэм произвольные то формула будет истина
2:11:09
тогда я только тогда когда этот вектор попадает в это в этот наш предикат в отношении п и тем самым получается что
2:11:16
это формула интерпретируют вернее выражает как раз таки да интерпретации это действие из
2:11:22
сигнатуры в модель вырази масть это наоборот итак атомы из модели в сигнатуру попадаем вот эта формула
2:11:29
выражает нам данный предикат здесь вот есть некая тонкость значит если я говорю
2:11:34
о формуле а со значком м то это интерпретация формула в нашей модели то
2:11:40
есть эта формула уже как бы переведенная на язык модели тогда вот подчеркивать не
2:11:46
надо потому что здесь просто вместо свободных
2:11:51
переменных ну кстати сегодня перемену тогда должны быть тоже помечены значком м вот вместо свободных переменных
2:11:58
подставляются конкретные элементы множества м а если мы говорим как мы
2:12:05
договаривались ранее что мы будем писать истинно формула а которая не интерпретация а сама формула а в
2:12:11
исходной сигнатуре тогда свободная переменная это действительно свободная переменная сигнатура сигма а
2:12:17
вот константы которые мы вместо них подставляем это уже их так сказать
2:12:23
numeral и ну то есть это представление этих констант в расширенные нашей сигнатуре вот эти вот штуки
2:12:30
либо так пишем либо по другому ну и в паре с этим идет естественно мы
2:12:37
определим от функции какой-либо вот у нас везде есть какая-то функция из
2:12:43
множества м м то есть функция от n аргументов действующий оуен ну то есть
2:12:49
операция до задано на т.н. она определима или выразимо
2:12:54
в сигма у т.м. если
2:12:59
для любых c1 сны
2:13:05
скажем так б да если существует
2:13:10
если существует формула а от переменных 1 а н а а
2:13:19
здесь на было написать формула а от переменных 11 если есть такая формула
2:13:25
что для любых констант значит c и b из множества м
2:13:31
имеет место ну в общем практически та же самая напоминаю что функция это на самом деле просто некий вид отношений просто
2:13:38
на множество m в степени n + 1 и мы это просто переписываем для случая функций f
2:13:44
от c1 c2 равно б
2:13:50
тогда я только тогда когда в истинно вот это вот а
2:13:59
где мы вместо 1 хашиг подставляем наши церки
2:14:07
вместо свободной переменной а подставляем нашу константу b ну естественно тут надо
2:14:14
поставить номер алла вот то есть
2:14:19
тогда мы говорим что вот эта функция может быть задано некой формулы в нашей расширенной сигнатуре
2:14:26
расширенная сигнатуре сигма от м вот простейший пример связки значит
2:14:34
рифме кипиа на со стандартной моделью может быть таким а
2:14:39
именно многочлен какой-нибудь ну например
2:14:45
значит на стандартной модели на лиге мы можем задать такой многочленов от
2:14:51
значит у нас тут используется давайте и for a равняется
2:14:59
там 3a квадрат плюс 5 а + 1 ну обычная
2:15:06
вполне себе парабола который мы задаем на натуральных числах аа пробегает натуральные числа понятное дело
2:15:14
вопрос можно ли эту функцию выразите в исходной сигнатуре арифметики
2:15:22
пеано даже не взять на в расширенной с номером как я уже говорил там это в принципе все равно но ответ да конечно
2:15:29
можно потому что можем написать такую формулу
2:15:35
тут у нас было а один ну давайте формула будет такой вот абэ
2:15:43
следующего вида b равно 3 значит 3 это ты подчеркнутая то есть
2:15:53
мы как вот мы пользуемся расширенный сигнатуры но можно иметь ввиду что просто вот на эти три иски от нуля можно
2:15:59
заменить дальше мы умножаем на а потом еще раз на
2:16:06
потом и к этому всему прибавляем 5 подчеркнутая умноженная на а и потом мы
2:16:12
прибавляем 1 подчёркнуто вот собственно формула которая будет
2:16:17
выражать нам эту функцию в исходной сигнатуре пиана ну точнее это
2:16:22
расширенная сигнатуре арестом и все подчеркнутые заменим на ссс от нуля то тогда даже прием формулу в расширенной
2:16:29
сигнатуре это так сказать позитивный пример когда мы какую-то функцию смогли ну собственно
2:16:36
любой вообще многочлен от натуральных чисел он выразил в
2:16:41
исходной сигнатуре арифметики пеано а если мы например хотим на множестве в
2:16:48
нашей модели определить такое отношение то есть здесь была функция теперь возьмем отношение а меньше либо равно b
2:16:54
будет ли он выразил в арифметики пеано ведь там нет отношений и меньше либо
2:17:00
равно ответ да будет и формула будет такой out a b
2:17:07
существует z плюс z равно бы
2:17:12
поскольку у нас числа неотрицательные все то соответственно здесь вот вот это получается очень хорошо интерпретируется
2:17:20
да и можно доказать именно доказать что значит если мы эту формулу
2:17:27
проинтерпретируем в стандартную модель то окажется что эта формула ровно-ровно
2:17:33
задает вот это вот отношение меньше либо равно то есть это опять-таки позитивный пример
2:17:39
но смотрите если мы теперь возьмем скажи мне арифметику пиана а
2:17:45
обычную аддитивных группу по сложению до бесконечно у нее моделью будет например
2:17:51
z с операции + вот и мы рассмотрим поскольку группа по
2:17:59
сложению там есть только операция сложения больше там ничего нет ну равенство еще может добавить да еще
2:18:05
равенство берем стандартную модель и такой теории
2:18:10
это просто целые числа в целых числах мы тоже можем определить вот этот предикат а меньше либо равно бы
2:18:17
возникает вопрос а можно ли вот в такой сигнатуре задать отношении а меньше либо равно b ответ нет нельзя и
2:18:25
и значит доказывается это с помощью автоматизмов вот я сейчас это не хочу углубляться там если коротко суть
2:18:32
следующем мы когда строим какую-то модель мы можем построить еще одну модель еще
2:18:37
одно много разных моделей и говорить о выходом орфизма поскольку это алгебраические структуры то изоморфизм
2:18:44
структуру это просто сопоставление операции отношений так что одна в другую переходят один в один вот так вот если
2:18:52
мы возьмем скажем построим изоморфизм точнее автоматизм
2:18:59
этой модели на себя которые каждому из будет ставить соответствие минус x
2:19:04
то мы заметим что неравенство а меньше либо равно б она превратится в
2:19:11
неравенство в обратное то есть а меньших оборону б она перейдёт в минус b меньше
2:19:16
либо равно минус а то есть короче говоря если бы мы переносили
2:19:24
таскать ну изоморфизм короче говоря не сохраняет отношении неравенство of the more фильм на этой модели потому что
2:19:31
были в таком порядке стали в порядке наоборот вот а это и тогда а если мы
2:19:38
что-то интерпретируем в какой-то модели а потом применяем автоматизм то что у
2:19:43
нас это можно доказать что при после применения автоматизма и вообще любого изоморфизма интерпретация сохраняется а
2:19:50
тут получится что мы нарушили интерпретацию и то есть если бы меньше либо равно можно было определить в
2:19:57
исходной сигнатуре z плюс равно то неравенство обязана была бы
2:20:04
сохраняться при интерпретациях и при применении изоморфизм of она и сохраняется таким образом для обычных
2:20:10
аддитивных групп ввести отношении меньше либо равно невозможно в их сигнатуре вот
2:20:20
но как только мы добавляем
2:20:25
сюда операцию умножения то есть теперь мы рассмотрим уже не группа а кольца
2:20:31
бесконечные оказывается уже что отношение меньше либо равно можно в этой сигнатуре
2:20:36
определить почему можно определить потому что а меньше либо равно будет
2:20:42
выражаться похожий формулой только чуть посложнее z1 за 2 c-3 за 4 такие что а
2:20:52
плюс z 1 квадрат плюс за 2 квадратах релизе 3 квадрат везет 4 квадрат
2:20:59
равно b почему потому что мы знаем что любое неотрицательное число представляется в
2:21:06
виде суммы как не более четырех квадратов это теорема по моему лежандра а
2:21:12
значит как только у нас появилось уважение мы можем ввести вот эти вот степени
2:21:18
из их помощью уже задать вот это вот а меньше либо равно бы вот такая тонкая
2:21:26
грань между до между группами и кольцами когда мы хотим чего-то в них определять
2:21:31
то есть кольца они более выразительно скажем так они но больше гораздо больше могут выражать про свои объекты которые
2:21:38
они описывают ну и последнее определение которое я здесь там в этом блоке это
2:21:46
представимо сть функции в теории то есть мало того что мы сказали о том что что
2:21:53
то мы умеем выражать в языке формальном языке сигнатуре сигма но у нас же еще
2:21:59
может быть теория вот пусть у нас м это модель теория т всегда туре сигма
2:22:10
сигнатура сигма мы скажем что функция f по определению
2:22:17
функция f а точнее операция на множестве м выразим
2:22:25
представила
2:22:30
представим а в теории т
2:22:37
теории т если ну во-первых она естественно там
2:22:44
выразимо должна быть и выразимо
2:22:49
в сигма от м то есть она должна иметь свою формулу
2:22:56
которую она там представляется кстати мы обычно будем вот так писать формула а
2:23:03
с индексом f женщин когда мы писали интерпретацию мы ставили там а со
2:23:10
значком м это означало что мы формула перегрина язык модели м тут наоборот мы взяли функцию f и нашли соответствующие
2:23:16
формулу в сигнатуре вот и второе самое главное требование в
2:23:24
теории ты должна быть доказуемо теорема такого вида
2:23:31
что а нет не совсем так
2:23:39
для любых а и b таких что f это
2:23:48
равно бы вот это второй пункт для любых а и бы
2:23:53
таких что и фото равно b то есть принадлежащих графику функции f должно быть выполнено следующие в теории т
2:24:00
должна быть доказуемо теорема если f от
2:24:05
то вы тут уже мы берём вот эту вот форму если а.ф.
2:24:12
вот numeral а b и
2:24:19
a f от x
2:24:25
[музыка] то тогда x это номер all.by
2:24:32
ну и конечно я как всегда забыл здесь поставить quantum x
2:24:38
что говорит эта теорема эта теорема говорит о том что данная формула задает функцию да потому
2:24:46
что при аргументе а мы должны получать всегда одно и то же значение если a и b
2:24:53
удовлетворяют этой формуле они удовлетворят потому что а.ф. это функция
2:24:59
эта формула которая определяет нашу функцию вот это из 1 пункта следует то
2:25:04
какую бы мы переменную не взяли вместо значения функции да она обязана совпасть
2:25:11
с номера lamb то есть ну что и говорит в общем-то об
2:25:16
однозначности отображения которое задает нашу функцию а ну конечно можем сказать так мы и так знаем что она однозначно
2:25:22
потому что эта функция ну по определению исходная функция суть в том что мы
2:25:29
должны уметь это доказывать в теории т в нашем с формализме сима ты а еще лучше
2:25:36
вообще в исходном в форме формализме сигма то есть здесь
2:25:41
более сильное получается требование за счет того что должен мы должны уметь предъявлять именно доказательство этого
2:25:48
факта в самом формализме в теории т ну понятное дело что
2:25:54
представим от функции это более сильное свойства все представили функция не обязательно выразим и тут просто это в
2:26:00
определении зашито иногда дают немножко другие определения это можно доказать что всякая представимо функция будет
2:26:06
обязательно выразим ой но без этого никак потому что как иначе доказать такую теорему вот и
2:26:12
и значит что можно сказать например
2:26:18
если брать функцию быстрей на которую мы ранее говорили дату для нее можно взяв
2:26:24
конкретные числа а и b вот эту теорему доказать что это действительно функция
2:26:30
то есть она во-первых выразимо а во-вторых можно про ее доказать что эта функция
2:26:38
но доказать что она для любого стартового числа то есть поставить кванта по аргументу и доказать что она
2:26:44
будет когда-нибудь что что она будет вычислено на этом аргументе вот это уже мы не можем в
2:26:50
теории пьян ну собственно теперь мы будем двигаться дальше переходить к понятию вычислимости и как все это будет
2:26:57
связано с тем что мы здесь ввели первую очередь применить на конечно к к стандартной модели так идем теперь
2:27:04
собственно говоря понятие перечислим их и разрешим их множеств и перед этим еще я повторю
2:27:12
понятие вычислимости что такое вычисли масть но у нас когда мы рассматривали тире тире могут стейна было такое
2:27:19
понятие частично рекурсивная функция эта функция напоминаю которой построена
2:27:24
при помощи некоторого списка базовых функций по сути совпадающих с функциями
2:27:31
описываемыми функциональными символами арифметики пеано в стандартными ну там еще проекции
2:27:37
были добавлены затем любая композиция функции частично
2:27:43
рекурсивных является частичной рекурсивной значит далее обычная неограниченная рекурсия приводит
2:27:52
но не выводят из этого класса и так называемый оператор также оставляет функции в данном классе отчиму вот такой
2:27:58
что такое частично рекурсивные функции но сейчас я не буду вдаваться формальности и в общем виде можно себе
2:28:06
представлять так что частично рекурсивная функция эта функция которую можно вычислить на обычном компьютере ну
2:28:14
или на машине тьюринга при помощи некоторого конечного алгоритма то есть на вход подается
2:28:19
одно или несколько натуральных чисел на выходе получается какой-то натуральное
2:28:24
число за конечное число шагов либо программа зацикливается да мы говорим что для данного входа эта
2:28:31
функция не определена поэтому у нас функции частичными называют выше для каких-то входов она определена на каких-то не определена ну
2:28:39
и соответственно а сюда же вот даб даб ухе у нас есть такая функция
2:28:46
с к аргументами на самом деле к этим же функциям взаимно
2:28:51
однозначно сводится функций которые работают с разными другими видами да нокдауна пример со строками вот есть
2:28:59
у нас строки а мы сейчас как раз занимались построением формальной теории которая представляет собой не что иное как просто список текстов некоторых вот
2:29:06
есть руки или тексты их можно тоже эффективно за нумеровать некоторых некоторым образом поскольку у нас есть
2:29:12
нет некоторая фарид причем мы даже говорили что вы арифметики пеано можно отделаться конечным алфавитом
2:29:19
поэтому все очень хорошо все строки можно очень хорошо закодировать по сути это ну аналог
2:29:26
таблица ски или там unicode в обычных компьютерах да когда есть таблица
2:29:32
символов им сопоставлены конкретные числа там например шестнадцатеричной системе счисления их можно записать ну и
2:29:39
дальше любой текст соответствует а просто какое-то огромное число и вот таким манером действуя мы можем
2:29:45
тоже самое говорить про текста то есть какой-то алгоритм которых которого на вход мы подаем 1 или много текстов
2:29:53
код с ними что-то делает и за конечное число шагов выдает результат результата может быть или число например длина
2:29:59
этого текста или снова текст например конкатенация этих текстов вот и все это
2:30:05
сводится вот к таким функциям от натурального аргумента с натуральным значением соответственно если он на входном тексте зацикливаются то тоже у
2:30:13
нас получается что ответ не определен поэтому мы не будем делать различие между
2:30:19
частично рекурсивные функциями определенных для натуральных чисел и для текстов заданных в каком-то
2:30:25
фиксированном алфавите можно даже говорить о четных алфавитах но я более
2:30:30
чем счетных здесь уже не получится говорить вот но в принципе мы всегда будем подразумевать арифметику пиана и
2:30:36
конечный альфа и так что все еще проще значит эквивалентное понятие для
Вычислимые функции
2:30:43
частичных рекурсией это вычислим и и вот то есть мы можем говорить о том что у
2:30:48
нас функция вычислим а то же самое это означает что есть
2:30:54
алгоритм который вычисляет то есть она вычисляется на машине тьюринга или на машине паста или алгоритмом маркова или
2:31:02
в конце концов просто на любом произвольном компьютере для которого мы не делаем ограничение по памяти
2:31:08
соответственно и так ну вот более-менее мы вспомнили что
2:31:15
такое вычислимое функция и теперь введем понятие собственно говоря
Перечислимость и разрешимость множеств
2:31:21
перечислим их и разрешим их множеств мы будем говорить что множество м
2:31:28
перечислим а если
2:31:35
так называемая по характеристическая функция этого множества обозначается вот так вычислим а
2:31:44
ну и можно так написать принадлежит через что такое полу характеристическая
2:31:50
функция эта функция которая
2:31:56
значит пусть тут какой-то икс икс это может быть или число или набор чисел
2:32:02
вектор если м это так сказать многомерное поднос туда подмножество в н степени к к из теста конечная значит эта
2:32:10
функция равна единице я если x принадлежит им и не
2:32:18
определена иначе вместо единицы можно стоять в принципе
2:32:25
любой константу иногда пишут 0 иногда пишут просто какую-то константу но в общем получается так что эта функция
2:32:32
получается тождественная функция она всегда равна одному и тому же значению но определена на строго на множестве им
2:32:39
за его пределами она не определена и если она вот вычислим а то есть есть алгоритм который умеет вычислять на
2:32:44
множество м то мы говорим о том что множество м перечислим а эквивалентные значит определение для
2:32:52
перечислим их множеств такие например множество перечислим а если она является
2:32:58
областью значений некоторых вычислим ее функции ну тут правда предполагать тогда что
2:33:05
функция может действовать не только в одномерное н-но в какой-то многомерное хотя опять-таки мы не только тексты
2:33:11
умеем кодировать натуральными числами но и все конечные инки натуральных чисел мы
2:33:17
тоже можем закодировать причем эффективно некое с помощью некой вычисления функции перед умирать все
2:33:23
натуральными числами и там используются значит и диагонально нумерация кантора который а
2:33:30
потом у теплице руется на много измерений и потом еще обобщается на для произвольного к
2:33:36
тоже сейчас не будем это вдаваться в общем есть способ вот произвольных от
2:33:41
кортежей произвольной длины из натуральных чисел перейти просто к натуральным числам соответственно мы
2:33:46
вообще можем всегда говорить о вычислим их функциях как о функциях из нвм и все ну принципе можем дальше так и
2:33:54
действовать значит но что им перечислим а если она является областью значений вычислимое функции
2:34:00
если она является областью определения вычислимое функция и более того функция вычислим а если она
2:34:08
если ее график то есть подмножество в прямом произведение н а н соответственно
2:34:14
тоже перечислим причем это критерий то есть вам в той и другой стороны действует короче говоря купили
2:34:21
численности есть несколько таких достаточно понятных определений что 5 по
2:34:26
моему которой все между собой эквивалентно ну вот это самое простое главное она легко обобщается если мы
2:34:31
теперь рассмотрим так называемую характеристической у функцию множество м которая равна единице если из
2:34:39
принадлежит им и 0 если x не принадлежит им
2:34:44
вот то есть она уже всюду определено она тотальная и а на 2 единицы равна именно
2:34:51
на множестве такая функция характеристическая функция но что м и вот если такая функция
2:34:57
вычислим а да то есть она для любого входа как прилежащего м так и не подлежащего м выдает обязательно ответ
2:35:05
причем ответ который отделяет элементы м.н. тогда мы говорим что множество x
2:35:11
вот в этом случае множество м разрешима
2:35:19
нужно сказать что вообще термин разрешимость он такой достаточно перегруженной в мад логики и в разных ее
2:35:25
разделах используется для разных целей вот поэтому надо всегда иметь ввиду некий контекста если мы говорим о
2:35:31
множество натуральных чисел разрешилась означает ровно вот это некий алгоритм который умеет про каждое число
2:35:38
сказать нам принадлежит ли она множество м или не принадлежит той за конечное число шагов мы это можем выяснить
2:35:45
значит главный результат здесь наверное эта теорема клине
Теорема Клини о существовании перечислимого неразрешимого множества
2:35:54
теорема клине которое нам говорит о том что существует
2:36:02
перечислим а и неразрешимое множество существует множество к
2:36:10
перечислим а я и неразрешима
2:36:17
доказывать в эту деревню будем можно только образно заметить что например его
2:36:22
можно построить до постройки у мужа многими способами но один из способов например такой давайте рассмотрим все
2:36:29
машины тьюринга которая принимает на вход натуральное число и соответственно
2:36:35
выдают в ответ тоже натуральное число но не всегда иногда не зацикливаться да то есть машины тьюринга которые реализуют
2:36:42
частично рекурсивные функции заданной она может натуральных чисел и соответственно за с натуральными
2:36:48
значениями мы эти машины тьюринга можем все эффективно перенумеровать то есть
2:36:54
можно построить алгоритм которые нумеруют машину тьюринга потому что машины эти машины тьюринга задаются все
2:37:01
в некоем конечном алфавите соответственно можно пираты рн умирать этот алфавит затем передозировать
2:37:07
программы всех этих машин и тем самым перенумеровать все машины ну и дальше
2:37:12
возникает такой естественный вопрос да допустим у нас есть машина тьюринга какая то м у нее есть какой-то номер pen
2:37:21
мы этот номер н ей подаем ей же самый подаем на вход то есть вот она сама на
2:37:27
своем номере может либо зациклиться то есть ничего не выдать не когда-либо вы
2:37:32
дать какой-то ответ то есть ну то есть вычислить результат и дальше можем взять
2:37:39
множество всех номеров машин тьюринг которые зацикливаются на собственном но
2:37:45
мире ну вот вот такой но что будет как раз перечислил но не разрешил ну и вот
2:37:51
таких вот вариантов с таким подходом типа теорема кантора да не существует
2:37:57
много которые дают реализацию такого множества то есть нет никаких сомнений в том что
2:38:03
такое что действительно существует и достаточно убедительно что еще хорошо
2:38:10
вычислимыми функциями это их такая очень тесная связь с иерархия форму которую я
2:38:17
тоже приводил ранее в разговоре о теореме goods train а я напоминаю у нас строила следующая
2:38:24
иерархия формул у нас были так называемые дельта 0 формулы
2:38:29
это формул которая содержит только ограниченные кванторы или вообще не
2:38:34
содержат кванторов ограниченный кванторы это квартира такого вида для любого x меньше т и там меньше либо равно и
Иерархия формул
2:38:41
соответственно существует x меньше либо равный т вот если формулу
2:38:48
можно переписать так что в них будут только такие кванторы ну или вообще не будет кванторов тогда мы говорим что эта
2:38:55
формула с ограниченными квартирами или ограниченная формула или дельта 0 формула эти формулы хороши тем что их
2:39:02
истинность проверяется конечном алгоритма да то есть мы можем вот здесь вот запустить цикл который там от 0 до
2:39:09
ты пройдет и проверить истинность формулы стоящей внутрь и а поскольку внутри тоже стоит да это 0 формула то
2:39:15
соответственно какое-то конечное количество вложенных циклов будет и рано или поздно программа выдаст ответ
2:39:21
истинна эта формула или ложно ноту тем хороши эти собственно говоря дать тоннель формула ну и дальше у нас было
2:39:29
понятие сигма 1 и p1 форму сигма 1 и 1 все вместе это называлось
2:39:37
дельта 1 и дальше мы вот расширяли определяются они так если у нас есть
2:39:43
какая-то дельта формула дельта 0 формула то тогда формула вида для любого x
2:39:49
дельта и существует x дельта это как раз и есть формулы значит для любого x эта
2:39:56
формула вида p1 а существует x это формула вида сигма 1
2:40:05
то есть когда мы к ограниченной формы впереди представляем кванта
2:40:10
существования который может быть квартирам по нескольким переменным просто однотипные однотипно серия
2:40:16
кванторов скажем так стоит экватор существование перед этой формулой то это
2:40:21
нечто иное когда это один формула в частности если переменная x не входит в нашу формулу дельта вот эту дельта 0 то
2:40:28
она получается эффективной то есть что она тудей что нет не важно результат не зависит потому что ее нет
2:40:34
просто в формуле дельт этим самым и дельта 0 формулы вкладываем в класс
2:40:40
сигма 1 то есть classic мадина вот такой захватывает сигма 0 а дельта 0 ну и
2:40:45
соответственно и 1 класс содержит себя дельта 0 и все вместе это дельта 1 и
2:40:50
точно так же мы расширяем меняя навешивая кванторы то есть перед здесь
2:40:56
мы можем существует поставить потом опять для любого потом опять существует вот сколько таких перемен таков индексу
2:41:02
соответствующего класса вот но нас будет интересовать только класс сигма 1 формул и оказывается он хорош следующим
2:41:10
свойством а именно такая теорема
Теорема о сигма1-определимости вычислимых функций в арифметике
2:41:19
теорема о сигма 1 определим асти
2:41:26
терял говорит следующее что какова бы ни была вычислимое функция f
2:41:35
найдется такая формула существует формула а.ф. из
2:41:42
соответственно формализма арифметики пеано
2:41:47
то есть мы берем формулы сигма арифметики пеано
2:41:53
значит найдется такая формула которая обладает следующими свойствами
2:41:58
во первых это сигма 1 формула то есть имеет вид
2:42:04
квартиры существования неограниченны а потом ограниченная формула и второе эта
2:42:10
форма а является определением нашей функции в формализме арифметики пеано
2:42:16
вот напоминаю определение значит что что значит что это формула является
2:42:22
определением этой самой функции это значит что для любого
2:42:27
ну там давайте напишем как вектор набора параметров c и
2:42:32
соответственно числа a и f c
2:42:38
равно а просто чтобы их было ну как бы от нескольких аргументов да мы тут пишем
2:42:44
вектор то есть на самом деле это просто c1 , c2 и так далее , c&c к то
2:42:50
выполняется вот это равенство тогда я только тогда когда в нашей
2:42:55
стандартные модели истинно выражение
2:43:01
формула а.ф. с поставленными вместо туда переменными
2:43:09
давайте c здесь c напишем и и а
2:43:17
единственное когда мы говорим про формулу записано в языке арифметики пеано то мы должны вместо настоящей
2:43:22
натуральных чисел подставлять туда он умирало до то есть правильно здесь надо подчеркивать эти обозначения натуральных
2:43:30
чисел имея в виду что мы все настоящие натуральные числа заменяем
2:43:35
напором вот этих с от с от с от с от нуля чтобы получилось правильно построена
2:43:41
значит в в языке пиана формула atv ну тут конечно совсем правильно был взят
2:43:49
что аиф эта формула от аргументов скажем
2:43:56
b1 и так далее bkt и какого то
2:44:03
что у нас там б показать подмену этих переменных b1
2:44:10
заменяем на т1 numeral богатый заменяем на цикад и numeral б замена
2:44:16
он умирал дело в том что здесь то это переменные именно в формализме а здесь
2:44:23
это конкретные числа которые мы задали снаружи от нашей теории пиана мы вот
2:44:29
здесь вот вот вот эта часть формулы она находится вне формализма арифметики пеано это формула записано в нашем мета
2:44:37
языке то есть ну считайте в тюрьме за твц вот в который мы выбрали какие-то
2:44:43
натуральные числа произвольные отсюда уже подставили их вымирала вот то есть
2:44:49
это уже получается формула без переменных в общем там могут быть еще какие перемены но они получаются
2:44:54
фиктивные то есть получается в принципе как бы де-факто это некая замкнутая формула но
2:45:01
вот так то есть получается что всякая всякая вычислим а я функция ну или
2:45:06
соответственно вычислим и какой-то алгоритм можно представить или записать некоторые сигма 1 формулой на языке
2:45:11
арифметики пеано значит в частности что можно понять из
2:45:20
этой теоремы частности я напоминаю что если мы возьмем функцию будет стейна это вот
2:45:26
такая функция от x равно y я здесь опять
2:45:32
допускаю вольности пользуюсь иначе связанными переменными но просто так привычнее на самом деле можно и нужно
2:45:39
иметь ввиду что здесь опять такие переменные должны быть типа об этом которые свободны значит функция густые
2:45:46
на в точке x равна y если последовательность будет стейна начавшись с числа x за y шагов достигнет
2:45:54
нуля мы как раз разговаривай теореме густой на говорили о том что тотальность этой функции как
2:46:01
раз эквивалентно самый тебя и бегут stain on так вот оказывается что
2:46:08
вот эта функция а значит и сама терема густой на
2:46:15
записывается на языке арифметики пеано то есть когда мы говорили о том что теорема густой на не формализуется не
2:46:23
нет недоказуемо в арифметики пеано конечно же надо было для пущей строгостью обязательно сказать что она
2:46:30
во-первых формулируется в этом языке и во-вторых она там недоказуемо то что
2:46:36
если какая-то теорема не формулируется на языке этой формальной теории то говорить о по ее доказуемо стиле
2:46:41
недоказуемо стью просто бессмысленно поэтому конечно надо было бы еще доказать что она на самом деле в этом
2:46:49
языке определима и вот из этой теоремы как раз и следует что поскольку эта функция у
2:46:56
нас является вычислим ай да мы можем предъявить конкретно алгоритм как она вычисляется в каждой фиксированной точке
2:47:02
x то соответственно эту функцию можно переписать с помощью
2:47:08
некоторые формулы языке которая покажет нам зависимость между их суммы игреком вот а утверждение соответственно та
2:47:15
формула будет сигма 1 вот а утверждение о тотальности функции же то есть теорема
2:47:21
густой на она уже будет формулы пе-2 почему потому что вот есть какая-то
2:47:27
формула же которая является сигма 1 это формула
2:47:32
переписывает фактически данное уравнение на языке арифметики пеано а утверждение
2:47:37
о тотальности она имеет такой вид для любого x же x y ну точнее для любого их
2:47:44
существует y такой сюжет икс игрек это утверждение тотальности и мы видим что вот если это у нас было сигма 1 формула
2:47:52
добавление кванта существования впереди класс формул не меняют это тоже будет
2:47:57
сигма 1 формула есть вот эта сигма 1 вот это сигма 1 а как только мы навесили
2:48:04
quandl существования кванторы всеобщности впереди вот это уже получит получилось пе-2 формула ну и вот
2:48:11
получается такой интересный момент что значит если мы выбрасываем кванторы
2:48:16
всеобщности впереди мы имеем сигма 1 формулу 1 сигма 1 форму мы можем для каждого конкретного числа ну точнее пары
2:48:24
чисел x и y в архетипе она доказать что и сузить будет равенство если мы взяли
2:48:31
уже заведомо зная что при таком-то x мы за столько-то шагов дойдем до нуля то есть заранее зная как бы результат то
2:48:38
теорема мы можем предъявить доказательства внутри арифметики пеано этого самого уравнения этого равенства
2:48:45
как только мы говорим что это верно для любого x
2:48:50
то есть добавляем сюда кванторы у нас сразу же никакого доказательства нет внутри смете
2:48:57
кипиа на всему той самой теорема которую мы обсуждали ранее так ну и теперь
2:49:05
да еще несколько слов о связи тип типов формул и соответственно арифметики пеано
2:49:12
оказывается что арифметика пиана относительно этих формул обладает относиться класса форму обладает такими
2:49:19
интересными свойствами вот как я говорил длительную формулы это
2:49:26
формула которые в общем то ну так сказать разрешимы то есть получается что мы всегда можем проверить истина надежно
2:49:33
на любом в ходе алгоритма который который зашит в эту форму так вот есть
2:49:39
такая теорема о дельта 0 полноте
Теорема о дельта0-разрешимости арифметики
2:49:47
вот или а дельта 0 разрешимости почему я скобках пишу
2:49:53
потому что опять всплывает слова разрешилась но относятся она уже к формулам и вот это как раз тот самый
2:50:00
момент когда термин перегружен поэтому давайте говорить а дельта 0 полноте потому что это понятно дело в том что
2:50:07
для дельта 0 форму имеет место такое свойство какова бы ни
2:50:13
была формула дык то класса дельта 0 вот опять я тут вольности допуская
2:50:20
потому что то было бы описать словами для любой формула а потому что это не формализм ну для краткости будем так
2:50:27
писательница какова бы ни была формула дельта из класса дельта 0
2:50:33
эта формула истинна да конечно же замкнут это как как обычно поставим черточку сверху обозначая замкнутую
2:50:40
форму то есть форму без переменных от которых может зависеть его значение то есть там могут быть какие-то
2:50:46
свободные переменные но они эффективны по ним можно квартир поставить и ничего
2:50:52
не случится при этом правда тоже перестанет падать tom ford так вот какова бы ни была замкнутая
2:50:58
дельта 0 формула она из и на в нашей стандартной модели
2:51:04
тогда и только тогда когда она
2:51:11
выводим а в арифметики пеано и более того
2:51:17
эта формула ложно стандартной модели
2:51:23
тогда и только тогда когда вы вадима ее отрицание в арифметики
2:51:30
пеано тут мы наблюдаем полную гармонию да если бы мы наш формальный язык ограничивали
2:51:37
только дельта 0 формулами то есть только ограниченными кванты раме то у нас
2:51:42
теория оказалась бы полный потому что всякая формула понятно по закону исключённого третьего на либо истина
2:51:48
либо ложно а по этой теореме получается что она тогда будет либо доказуемо либо провяжем а вот поэтому и
2:51:55
теорема как как бы у дельта 0 полноте вот для формул а границе с ограниченными
2:52:01
квартирами полнота теория имеет место быть но у нас теория более
2:52:08
так сказать разнообразная чем только теория с ограниченными квартирами
2:52:15
поэтому все не так хорошо становится когда мы переходим на следующий уровень
2:52:20
а именно уровень сигма 1 формул для сигма 1 формул
2:52:25
есть тоже теорема она тоже называется теоремой о полноте а
Теорема о сигма1-полноте арифметики
2:52:32
сигма 1 полноте а
2:52:38
вот да конечно имеется виду арифметика пьяна
2:52:43
и тут и тут и она звучит так какова бы ни была формула
2:52:48
сигма класса сигма 1 естественно замкнутая
2:52:54
значит для сигма 1 формулы истинность стандартной модели
2:53:01
эквивалентно выводимости ее в арифметики пеано
2:53:10
надо сказать что в принципе морефей купе она здесь можно ослабить до некой слабенько теории типа арифметики
2:53:16
робинсона q или там элементарной арифметики убрать вообще оттуда индукцию то есть
2:53:22
сделать ее ну очень простой но тем не менее все таки это будет арифметика с
2:53:28
бесконечным рядом натуральных чисел и там все равно это все будет работать но
2:53:33
мы как бы тоже выйти деталей углубляться сейчас не будем мы видим что отличие 2
2:53:39
теорема от 1 в том что мы про отрицание ничего не говорим то есть да мы говорим
2:53:44
что если формула истинна то она доказуемо сигма 1 формула ну если она
2:53:51
доказуемо то она истина это уже следует из теорему о корректности исчисления предикатов то есть тут на самом деле существенно часть это именно слева
2:53:58
направо а вот если оно ложно то и факт что мы найдем доказательства ложности ну
2:54:06
доказательства вот это отрицание сигма в арифметики пеано на самом деле часто и
2:54:12
не найдем потому что а федька пьяна как мы знаем не полна вот в частности здесь
2:54:18
работает вот то что я говорю про теорему густой надо значит для если мы возьмем замкнутую сигма 1 формулу а
2:54:26
саму форму возьмем из теорема good стейна чтобы ее сделать замкнуты вот эту формулу надо вместо x и y подставить
2:54:33
какие-то конкретные числа например там 5 и 10 туда подставляем и
2:54:38
оказывается что она будет истинной в стандартной модели то есть просто как бы
2:54:43
в математике и мы и более того в арифметики пеано можем доказать что это формула будет верно при
2:54:53
подстановке туда через чисел 5 и 10 но из следствий из предыдущей теоремы которые я стёр вот оно здесь внизу было
2:55:00
напишем следствие такое
2:55:08
если у нас имеется перечислим эй предикат то есть пусть p
2:55:15
это подмножество степени k и это перечисленное подмножество
2:55:22
перечисленное подмножество тогда
2:55:33
этот самый предикат он во первых представим в арифметики пеано
2:55:41
то есть существует формула а такая что
2:55:48
для любых чисел c1 цкп от и
2:55:55
п фото принадлежит c давайте так лектор напишем подлежит б
2:56:03
тогда я только тогда когда в стандартной модели истинно формула вот это вот а
2:56:11
pc1 ck ну и как обычно подчеркивает выбирала
2:56:16
то есть ну это просто повторение того что это дело все у нас определима и
2:56:24
поскольку перечисленный предикат задается вычисленной функцией
2:56:31
отсюда следует что его можно задать с помощью сигма 1 формулы а
2:56:37
значит для него выполняется вот та самая теорема о сигма 1 полноте то есть помимо
2:56:43
того что у нас перечислим эй предикат представим значит в арифметики пеано
2:56:50
получается еще и то что в стандартной модели вот это вот условия
2:56:57
равносильно тому что формально арифметики пеано можно вывести вот эту
2:57:04
вот нашу формулу
2:57:12
то есть как мы видим как только мы ограничиваем область деятельности нашей
2:57:17
только вычислимыми всякими там этими под множествами функциями и так далее то есть перечислил множествами счастливые
2:57:22
функциями у нас все становится довольно таки прикольно интересно потому что это
2:57:29
всё выражается сигма 1 формулами и
2:57:34
более того истинность становится эквивалентно доказуемо sti ну правда про
2:57:40
оправе жилось мы тут ничего не говорим да памятуя о том что это это верно будет
2:57:45
только для дельта 0 формул в частности из этого следствия можно
2:57:50
извлечь еще одно следствие о том что у нас если к это множество коли не то есть
2:57:57
перечисленное неразрешимое множество то мы можем поставить ему соответствия некий предикат назовем его
2:58:05
но пусть будет а к т от переменной а
2:58:12
который будет из тени на конкретном умирали тогда я только тогда в
2:58:18
конкретном на конкретно натуральном числе тогда и только тогда когда в по можно доказать эту самую истинность
2:58:26
вот этого предиката на конкретном умирали если мы туда умирал подставляя у нас получается замкнутая формула
2:58:32
соответственно будет истинность ну то есть получается что для любого перечислимого нас что в том
2:58:38
числе для множества клиник которые перечислены неразрешима можно указать
2:58:44
некий предикат этот предикат будет сигма 1 формулой потому что перечислим во
2:58:49
множество соответствует вычислимое функции то есть какой-то алгоритм вычисляет соответственно будет какая-то
2:58:54
сигма 1 формула 1 сигма 1 формулу нас выполняется вот это по сути мы получаем что для любого числа из множества к
2:59:03
перечислимого не так напишем любого а а
2:59:11
принадлежит к тогда я только тогда когда вы арифметики
2:59:17
пеано выводим а а к от номера ла а вот такая интересная штука ну и теперь
2:59:25
мы этим воспользуемся для того чтобы по ходу дела на пути к 2 дереве году я
2:59:31
неполноте доказать 1 утеря мы гадали о неполноте так называемый синтаксический вариант но для
2:59:38
этого нам понадобится еще одно определение сожалению здесь получается очень много
2:59:43
определений на фоне полного отсутствия доказательств у теорем который я привожу вот но иначе
2:59:52
бы это заняло там не знаете в целых 7 стр теперь мы вспоминаем о том что у нас
2:59:58
о чем говорили в самом начале что всякий текст мы можем закодировать
3:00:04
каким-то натуральным числом вот и соответственно говорить о том что
3:00:11
там множество каких-то текстов может быть вычислим а да то есть вот мы взяли
3:00:16
какой-то текст вспоминаем нашу картинку у нас тут формулы и термы это все какие-то тексты
3:00:25
правильно построенная значит среди формулу мы выделяем
3:00:30
какой-то базис которую мы называли не логическими аксиомами нашей теории
3:00:36
причем речь может идти любой вообще формальной теории далеко не обязательно это будет арифметическая теория вот то
3:00:43
есть и мы говорим о том что вот эти тексты их можно каким-то образом правильно за
3:00:50
нумеровать если у нас скажем так алфавит и сигнатура позволяют придумать алгоритм
3:00:58
который будет их перенумеровать в частности для арифметики пеано для теории множеств формальные это все
3:01:04
работает там и и вот так вот такие теория мы выделяем в некоторый класс
3:01:09
который мы называем эффективно axe мотивируем и насчет формальная теория называется эффективно
3:01:15
axio мотивируя моя если
3:01:24
если множество аксиом этой теории перечислим
3:01:31
а если это x перечислим а
3:01:36
я напоминаю что вообще-то мы через ты обозначали и теорию и список аксиом то
3:01:43
есть тут можно было другое обозначение водить а просто если ты перечислим а вот
3:01:48
но так сказать для ясности я ввёл разные обозначения
3:01:57
вот что значит перечислим и множество axium но представим себе что мы вспомним
3:02:02
этот список аксиом арифметики пеано это несколько строчек каких-то из текста
3:02:07
которые мы построили по определенным правилам лишь поскольку мы задали конкретные правила формула строения и
3:02:14
термос и термос троение мы можем указать конкретный алгоритм для меня постройки
3:02:20
этих этих самых аксиом раз у нас есть алгоритм более того мы
3:02:25
знаем что есть так называемое дерево разбора мы тут тут рисовали значит когда мы формулу можем для форма указать
3:02:32
дерево конечно дерево там в листьях стоят переменная вот соответственно
3:02:37
дальше мы говорим что вот нам дали какой-то текст и просят ответить аксиома
3:02:43
это или нет то есть является ли этот текст одним из текстов аксиому нашей
3:02:48
теории тогда мы пытаемся это текст разобрать то есть перейти к дерево разбора
3:02:54
смотрим как он устроен если все хорошо там и рано или поздно это все разберем и
3:03:01
увидим что этот текст действительно совпадает с одной из аксиом ну с точностью до может быть каких то перри
3:03:06
обозначений там это сейчас неважно можно вообще в принципе да говорить о том что нам далее текст она просто сравнить
3:03:14
содержится ли этот текст в списки текстов аксиомы или нет ну там правда доставляет трудности соответственно схем
3:03:21
аксиом индукции потому что она определяется таким как виртуальным
3:03:26
параметрам которым является произвольная форма нашего языка вот тут как раз и потребуется значит дерево разбора чтобы
3:03:33
понять действительно ли это аксиома индукции в которую подставлена какая-то правильно построена формула со своим
3:03:40
деревом разбора вот но в принципе понятно что такое алгоритм написать можно которых будет проверять является
3:03:47
ли предложенный текст какой-то из этих аксиом то есть axiom pro сложение и
3:03:53
умножение про 0 и соответственно всем индукции тут есть одна тонкость если
3:03:58
этот текст который нам дали действительно является аксиомой то мы вернем положительный ответ за какой-то
3:04:04
конечное время мы это все разберем разложим по деревьям так сказать и увидим как эта формула устроено и увидим
3:04:11
что она подпадает под наш список аксиом если же это какой-то произвольный текст
3:04:16
может быть вообще не формула может быть формул но не аксиома то не исключено что
3:04:21
мы можем зациклиться потому что ну там какая-то будет ерунда мы не сможем
3:04:27
правильно разобрать это дерево может быть просто скобкой и будет какой-то закрыта и и тому подобное вот и тогда
3:04:33
наш алгоритм даст сбой и не сможет ответить на вопрос аксиома это или нет тут точнее получать так что если эта
3:04:40
аксиома дон скажет да а если это не аксиома то он ничего не скажет
3:04:45
это есть тот самый случай полу характеристической функции то есть для
3:04:51
элементов множества а x мы даем положительный ответ возвращаем единицу а
3:04:56
для всех остальных мы ничего не возвращаем вот соответственно
3:05:02
более того там можно немножко подправить да если вдруг случайно окажется что мы можем какие-то формулы разобрать это же
3:05:10
как-то и дать про них ответ что нет это не аксиома то в этом случае можем
3:05:15
доработать наш алгоритм и зациклить его если мы получили ответ что это точно не аксиома можем тоже зациклить чтобы уж
3:05:22
точно знать что у нас не зацикливаться только на аксиомах таким образом получается что вот если
3:05:32
если вот такая ситуация возможна то у нас множество axiom ну что ты чего текстов перечисли мая ну и в таком
3:05:39
случае мы говорит что теория эффективно ароматизируем например зад овцы пиана
3:05:45
элементарная арифметика вот еще там ряд теорий там элементарная
3:05:51
геометрия теория героически замкнутых полей характеристики но ли они все эффективно ароматизируем
3:05:58
то есть беря произвольную такую хорошо построенную формальную теорию в конечной
3:06:04
или счетной сигнатуре с конечным или счетным алфавитом мы скорее всего наткнемся именно на теорию которая будет
3:06:10
эффективно axe мотивируем а это как бы не исключение из правила скорее очень сильно и правила
3:06:16
так вот да и я напоминаю у нас до этого была свойства о том что в арифметики пеано
3:06:24
замкнуто сигма 1 формула обладает тем свойством что она истинна в
3:06:30
стандартной модели тогда и только тогда когда она доказуемо в арифметики пеано давайте это свойство немножко обобщив
3:06:36
пусть у нас есть какая-то произвольная теория т и у нее есть модель
3:06:42
в этой теории т соответственно в ее формализме мы тоже можем рассматривать сигма 1 формулы и мы скажем что теория
3:06:49
ты сигма 1 корректно сигма 1 корректно то есть это
3:06:54
определение если для любой сигма 1 формулы замкнутой
3:07:01
естественно ее истинность в данной модели в которой у нас истину теория т
3:07:08
эквивалентно выводимости этой формулы в этой теории то есть мы
3:07:16
просто обобщаем ту теорему которую мы знаем про арифметику пиана на произвольные теории имеющие модель то есть непротиворечивое
3:07:25
да и на соответственно аппарат вот этих сигма 1 форму которую мы в их формализме
3:07:30
создаем и говорим что теория фильма один корректно если выполняется вот такая к валентность в частности теория пиана
3:07:36
теория за торцы они сигма 1 корректно и эффективно axe мотивируем и вот теперь можем сформулировать то что называется
3:07:44
синтаксический вариант 1 теорема геделя о неполноте пока еще 1 1
Первая теорема Гёделя о неполноте (синтаксический вариант)
3:07:50
теорема геделя о неполноте
3:07:56
синтаксический вариант почему синтаксически потому что это
3:08:03
теория где теорема формулируется на уровне операции с текстами по сути с
3:08:08
текстами вот этими которые представляют собой формулы и термо и так мы говорим что если у нас теория т
3:08:16
непротиворечиво
3:08:21
далее эффективно акция мотивируем а
3:08:28
сигма 1 корректно
3:08:34
сигма 1 корректно и самое главное умеет интерпретировать арифметику пиана
3:08:41
но вот так напишем содержит в себе арифметику peanut
3:08:48
что что имеется в виду то есть t это может быть какая-то арифметика более
3:08:53
сильная чем арифметика пиана или эта теория в которой можно
3:08:59
определить натуральные числа и там будут выполнять то есть внутри которые можно построить модель в которой будет
3:09:05
выполняться арифметика пиана например теория за твц мы знаем что там есть модель omega намеки выполняются все
3:09:12
аксиом пеано если там правильно сопоставить значит сигнатуре какие-то определенные предикаты ну вот короче
3:09:18
говоря федька пиана погружается как бы в эту теорию в эти теории можно интерпретировать арифметику пиана тогда
3:09:25
теория ты не полна тогда ты не
3:09:32
полна то есть существует какая-то формула которая не зависит от t не ее
3:09:38
саму ее отрицание доказать невозможно ну можно еще пару слов сказать о том что
3:09:43
здесь на самом деле не обязательно требовать чтобы погружалась именно счете к piano как я уже говорил во всех наших
3:09:50
рассуждениях здесь в принципе проходит самая самая простая элементарная арифметика даже без индукции этого
3:09:56
вполне достаточно чтобы реализовать весь этот аппарат который мы здесь используем ну и вот давайте я пока жук как это дело
3:10:04
доказывается естественно доказывается тащу от
3:10:10
противного и с использованием всех этих понятий которые мы тут велик самом деле
3:10:17
в общем то несложно вот главное просто не запутаться и так
3:10:24
доказательства предположим что теория таки полна
3:10:31
пусть ты полна напоминаю что значит полна это значит
3:10:38
что мы можем взять произвольную форму в языке этой теории замкнутую форму и окажется что или сама эта формула или ее
3:10:46
отрицание выводим а то есть там не может быть там нет расхождений от этого зазора
3:10:51
между доказуемо стью и истинностью так хорошо тогда давайте возьмем
3:10:58
поскольку мы в теории т умеем интерпретировать натуральные числа давайте возьмем множество к которой
3:11:06
множество клине перечисли мая и неразрешима и
3:11:15
соответственно раз у нас в теорию ты погружаются вся
3:11:20
вот эта вот арифметика натуральных чисел то есть там можно задавать соответственно и
3:11:26
сигма 1 формула из арифметики пеано вот то мы можем сделать следующий мы возьмем
3:11:33
формулу а которое именно определяет наше множество к в
3:11:41
данной теории ты вот ну мы как это сделаем мы сначала выберем множество кого арифметики пеано мы знаем что в
3:11:47
арифметики пеано есть такая формула которая определяет нам данный предикат это вот множество калине вот но
3:11:54
поскольку мы умеем как бы язык арифметики пеано погружать в язык теории т то мы можем переписать эту формулу на
3:12:01
языке теории т соответственно получится что у нас вот это вот перечислим а неразрешимое множество к она будет
3:12:08
определим а в языке теории т то есть тут все как бы законно получается эта формула будет вот из такого формализма
3:12:18
ну там сигма от сигнал эта формула причем замкнутая формула языка в
3:12:26
сигнатуре теорий т и эта формула обладает тем свойством что для любого числа n и
3:12:33
значит это он принадлежит множеству к причем это это мы сейчас в мета теории пишем тогда я только тогда когда теория
3:12:41
ты умеет доказывать а к большое от numeral а.н. опять-таки под номером n мы
3:12:48
подразумеваем интерпретацию умирала в теории т вот ну там чтобы совсем не
3:12:55
путаться давайте считать что ты это просто арифметика пиа надо чтобы проще было воспринимать на самом деле это все
3:13:02
проходит для более широкой теория вот то есть это у нас следует из того что
3:13:08
соответственно множество к перечислим а вот в силу тех
3:13:14
кто того средство которое мы выше рассматривали а теперь давайте соответственно посмотрим на
3:13:23
какой-нибудь элемент который не принадлежит множеству к пусть число m не принадлежит к это мы
3:13:33
пишем в нашей мета теории что тогда давайте рассмотрим формулу
3:13:40
давайте посмотрим вот на такую формулу вот эту же самую формулу подставим в ней
3:13:48
он умирал этого числа m это какая-то замкнуто формула в языке нашей теории т
3:13:55
что мы знаем про такую формулу поскольку теория ты полна по предположению то мы
3:14:02
можем либо у нас есть либо доказательства эту форму либо опровержение есть два варианта ты
3:14:09
доказывая takata вот м или ты или ты опровергает а катая от gm
3:14:21
ну первый вариант собственно говоря
3:14:27
приводит противоречию
3:14:34
почему потому что если бы вот этот вариант был верен то тогда пользуясь сигма 1 полнотой
3:14:42
нашей теории ты вот точнее сигма 1 корректностью нашей теории т вот это вот это свойство
3:14:48
напоминаю следует из сигма 1 корректности теорий ты тогда у нас получится что
3:14:53
но элемент вот этот м натуральное число n должно тоже принадлежать множеству к
3:15:04
это следствие сигма 1 корректности я напоминаю но тогда у нас получается что с одной
3:15:10
стороны им принадлежит к раз-другой странами мне принадлежит к возникает противоречие уже так сказать на уровне
3:15:16
нашей мета теорий то есть обычно математике мы такое отвергаем и тогда говорим что ну остается да вот
3:15:23
этот вариант что т ну существуют доказательства отрицания акад м теперь
3:15:29
давайте подумаем что такое доказательства доказательства я напоминаю это цепочка конечно из формул
3:15:37
где каждая формула либо является аксиомой теории т либо выводимые из предыдущих по правилам вывода которые мы
3:15:44
знаем это два правила бар вайса бернайс а и модус помнится собственно говоря ну
3:15:50
тогда мы можем предъявить алгоритм который нам
3:15:57
покажет что вот это число m значит точнее покажет что вот эта
3:16:04
формула будет соответственно ложно пока тотем будет
3:16:10
ложников вот отсюда следует что существует алгоритм который
3:16:16
показывает что а катая от м
3:16:21
ложно вот вот тут как раз начинает работать та
3:16:27
самая эффективная axio мотивируем as теории т значит сам вывод это конечное
3:16:34
число шагов которые нам демонстрирует просто как алгоритмическая машина как машина тьюринга демонстрирует что из
3:16:40
аксиом следует вот это этот факт сложности формула окато от м причем
3:16:47
можем это все дело переложить на интерпретацию то есть на некую модель в которой у нас чудном модель теорий т а
3:16:54
вот эти вылеты существует потому что мы предположили что теория то и непротиворечиво
3:17:00
следовательно в этой модели мы можем проинтерпретировать вот эту форму и она будет ложной причем у нас есть алгоритм
3:17:07
который это доказывает но алгоритм опирается на аксиома и вот тут начинает работать свойства фиктивная
3:17:12
xi мотивированности то есть мы про эту формулу можем мы с этой формулы можем
3:17:18
проделать следующее мы ее разберем по нашему дереву мы посмотрим не только
3:17:25
саму форму но и все дерева вывода все что предшествует fashion связывает эту фуру с аксиомами и
3:17:31
получается что мы про каждую конкретную формулу для конкретного номера laem где
3:17:37
им не принадлежит к сможем с помощью этого алгоритма и того что у нас есть
3:17:42
алгоритм распознавания axium показать что число m
3:17:48
делает эту форму ложный то есть им не принадлежит к таким образом комбинируя
3:17:54
вот эту как бы алгоритмическую структуру аксиом то есть эффективного xi мотивированность с тем
3:18:00
что сам вывод который значит определять определим по герберту тоже является алгоритмом мы в
3:18:08
итоге предъявляем некий алгоритм который нам скажет что
3:18:14
если им не принадлежит к то туда соответствующая формула будет
3:18:19
ложной короче говоря получается что мы можем предъявить алгоритм который
3:18:25
на элементах вне к тоже за конечное число шагов скажет нам
3:18:33
что это это число не принадлежит к вот здесь еще раз работают два факта эффективная xi матизе новость теории
3:18:40
тыыы полнота то есть возможность доказать отрицание формула а коты ну тогда
3:18:48
получается что мы про элемента и на умеем говорить что они являются элементами н с помощью алгоритма сигма 1
3:18:55
формулу можно рассмотреть как алгоритм так а про соответственно
3:19:02
элементы вне как мы тоже с помощью вот такой конструкции никого конечно вывод
3:19:08
тоже умеем говорить что они не являются элементами к то есть короче говоря как про к так и про дополнение к но штука мы
3:19:16
можем точно указать является или значит элемент ну указать что их элемента
3:19:22
действительно vk или действительно вне к вот тут надо ещё вспомним теорему
3:19:27
которую я забыл упомянуть это теорема критерии поста
3:19:37
который говорит следующее что произвольное множество м разрешима
3:19:44
тогда и только тогда когда является перед счастливыми она сама и его дополнение м и его дополнение
3:19:56
перечислим а но именно это мы здесь и демонстрируем оказывается что и к и дополнение к
3:20:04
являются перечисленными потому что мы указали алгоритм который на новый
3:20:09
элемент вне к для всякого натурального числа говорит что это число действительно не принадлежит к то есть
3:20:16
мы строим такую полу характеристическая функция для дополнения к ну и таким
3:20:22
образом до а то что для элементов к у нас перечислим а это следует просто из того
3:20:28
что мы к так выбрали это перечислено множество таким образом получается что и к и дополнение к оба перечислим и значит
3:20:35
party время поста к будет разрешима и вот мы к финальному противоречил
3:20:41
приходим с тем что к мы выбрали как неразрешимое множество и все это за счет
3:20:47
в общем-то полноты и и эффективная схема teaser у и мастики варите таким образом наше предположение star
3:20:54
товара ложно то есть теория т неполна и мы получаем результат который называется
3:21:00
первая теорема геделя о неполноте причем в синтаксической форме да потому что мы здесь работала чисто с
3:21:06
нумерую мастью с перечисли мастью неких текстов изображающих нам нашу формальную
3:21:11
теорию так ну и теперь да ну и конечно
3:21:18
следствия из этой теоремы следствия
3:21:25
теоремы о неполноте
3:21:31
арифметика пи она неполна и теория ф неполна
3:21:39
ну арифметика пи она неполна потому что содержит в себе репите купе она там у
3:21:45
нас было такое условие что теория должна содержать себе арифметику вот сама себе содержит она эффективна axe мотивируем
3:21:51
потому что она задается в конечном алфавите вот иначе по строгим правилам формула
3:21:57
строения и значит она сигма 1 корректно в силу той
3:22:03
теоремы о сигма 1 полноте которую я приводил до этого ну и теория множеств
3:22:09
почему не полна потому что в теории множеств можно определить собственно говоря все арифметику пиана то есть там
3:22:15
тоже можно задать вот этот множество калия и так дальше ну вот оно естественно эффективно ок симпатизировал
3:22:21
потому что задается в конечном алфавите вот значит алгоритм построения всех как
3:22:27
проверки текста на то что он является аксиомой там тоже очевидным образом из
3:22:32
аксиоматике за 3 видно ну и значит
3:22:39
сигма 1 корректность для арифметических формул ну наверно надо было подчеркнуть
3:22:44
что сигма 1 корректности в теории т она требуется именно для арифметических
3:22:49
форму то есть если мы арифметику погрузили в нашу теорию дальше мы только в этом куске и работаем вот в том куски
3:22:56
нашей внешней теории в которые в которой мы нашли арифметику ну вот и соответственно сигма 1 форму только
3:23:02
арифметически запев естественно сигма 1 корректно потому что там в чистом виде арифметика
3:23:07
пиана формализуется ну ну и соответственно по этой теореме за tf тоже не полна
3:23:13
так ну и теперь мы можем перейти к
3:23:19
собственно достижению нашего главного результата а именно к доказательству 2
3:23:26
теорема геделя о неполноте
3:23:32
теперь мы немножко разовьем тему вот этой вот эффективная axe мотивированности когда мы говорили что
3:23:39
все вот эти наши тексты термов формул все это можно неким эффективным образом
3:23:45
за нумеровать то есть предъявить алгоритм который их нумирует и
3:23:52
здесь мы тоже кратенько совершенно пробежимся по идеям которое заложено в основе этой
3:23:59
теоремы этой нумерации и сейчас я коротко опишу что вообще такое
3:24:05
представляет собой так называемая нумерация геделя
Гёделева нумерация формл в форме Куайна
3:24:19
тут давайте опять вспомним о том как у нас строится формальная система у нас
3:24:25
есть сигнатура в которой есть константы
3:24:30
есть предикат ные символы и есть функциональные символы а
3:24:37
также у нас есть переменные которые можно задать с помощью конечного алфавита я напоминаю мы задавали как в
3:24:44
палочка со звездочкой и x палочку со звездочкой и
3:24:50
предполагаем что у нас сигнатура конечная то есть конечно число констант
3:24:56
конечное число предикатов у которых у каждого из не конечное число аргумент
3:25:01
ных мест и конечно чеснок число функциональных символов тоже с конечным числом аргументов то есть все у нас в
3:25:08
принципе такое совершенно абсолютно конечно ну и давайте ещё вспомним о том что когда мы записываем какие-то формулы
3:25:15
мы там ставим скобки запятые вот у нас есть значки связок
3:25:21
логических это отрицания конъюнкция дизъюнкция импликация кванторы и
3:25:28
еще у нас есть значок вывода вот собственно
3:25:34
список всех значков которые мы выучили за это время ну кроме значка там истинности в модели это в общем-то весь
3:25:41
арсенал с помощью которого мы чего-то рассказываем про нашу формализм да то есть мы задаем there мы задаем формулы и
3:25:49
потом говорим значит выделяем из этих формул axiomatic у и строим какие-то
3:25:55
выводы из аксиом получаем теорема собственно говоря теоремы и так называем анти теорема то есть имеем такой корпус
3:26:02
текстов которые можем неким образом перенумеровать ну давайте скажем о том
3:26:08
как примерно это все происходит пусть у нас есть какая-то произвольно
3:26:16
фото давайте сначала сделать следующим и как в компьютере скажем что давайте мы все вот эти символы
3:26:22
пронумеруем числами натуральными числами от
3:26:28
так только не от 0 а от единицы тот редкий случай когда надо чтобы и
3:26:34
натурально честно начинались единиц на чм и вот эти все символы которые у нас есть программирую числами 12 и так далее
3:26:41
и до некоего числа п минус 1 где по это простое число ну
3:26:47
может быть мы дописали не дойдем подойдем там то п минус 10 например в общем короче говоря мы знаем да что я
3:26:55
просто чисел бесконечно много поэтому сколько бы здесь не было символов конечно набор мы всегда можем найти
3:27:00
простое число которое больше чем количество этих символов вот и говорим что вот мы все наши числа в том
3:27:09
числе да я забыл что здесь указать скобки и запятую мы все это пили нумеровали то есть мы
3:27:16
сделали таблицу котировки как вот таблица ютв 16 например да в компьютере
3:27:24
что можем тогда сделать мы можем произвольную форму
3:27:30
записать как число причем пустой текст у вас будет соответствовать так вот
3:27:35
напишем пустой текст будет соответствовать числу 0 но соответственно если тут есть какой-то
3:27:41
текст со своими числами со своими этими самыми
3:27:47
цифрами вот эти вот числа которые мы все пронумеровали мы будем называть цифрами
3:27:52
тогда произвольным текстом 1 и так далее а катая
3:27:58
мы можем пронумеровать числом которая будет записываться но примерно
3:28:05
так значит это будет давайте там значит c 1 + c 2 на п с так
3:28:15
далее плюс c катая на p в степени k минус 1
3:28:22
где соответственно c1 это цифра соответствующие букве a1c 2 эта цифра
3:28:30
соответствующая символа два и так далее можем это сделать можем вот получается
3:28:37
какой-то код соответственно всякий текст представляет с таким ну
3:28:44
каким то натуральным числом то есть по сути это разложение да по основанию b
3:28:50
понятно что не всякому числу соответствует какой-то текст то есть тут у нас появляется что-то вроде перечислим
3:28:56
асти но неразрешимости вот или скажем так мы можем взять произвольное число но
3:29:03
если мы его переведем в текст может скорее всего получится какая-то ерунда то есть там не закрытые скобки там
3:29:10
неправильно стоят квартиры с экспериментами еще чего-то в общем достаточно мало чисел натуральных будет
3:29:17
таких которые соответствуют правильно построенную формула чаще всего это как какая-то ерунда тем не менее мы говорим
3:29:25
что у нас существует совершенно понятный конкретный алгоритм который нам кодируют тексты
3:29:30
но этот алгоритм это вычислим а я функция следовательно мы можем
3:29:37
определить в арифметики пеано сигма 1 формулу значит взять такую фору if i’m at end
3:29:46
от от от одной свободной переменной r которая является сигма 1
3:29:51
формулой нашего языка но мы тут про пиана говорим на самом деле опять таки
3:29:57
можно это все немножко обобщать эта формула будет иметь следующие смысл
3:30:04
значит оно истинно тогда я только тогда когда число n это кот
3:30:12
формулы из
3:30:17
ф.м. в нашей сигнатуре
3:30:22
ну опять таки да за счет вычислимости можно такую формулу ввести вот и получается что как бы есть
3:30:31
алгоритм который по числу распознают формула этой линии формула тоже самое можно придумать и протерм а то есть
3:30:37
можно ввести соответственно формулу которые мы зовем т.м. вот н
3:30:45
которая означает что н есть кот какого-то термо на эти вот так напишем н
3:30:52
код термо ну далее мы на этом не останавливаемся и
3:31:00
мы говорим что мы можем помимо годов форму задать еще и код
3:31:10
последовательности форму вот у нас есть какая-то последовательность формулы 1 и так далее а k-тое они это все формулы
3:31:18
мы можем неким специальным образом
3:31:24
закодировать и последовательности для этого нам надо будет добавить сюда какой-нибудь еще спит символ
3:31:30
поскольку мы выбрали простое число достаточно большим то какой то номер у
3:31:35
него будет та же который будет меньше чем п и мы будем говорить так что давайте мы
3:31:41
последовательность формулу сканка тонируем в один большой текст в
3:31:46
котором мы это все разделим значком решетки вот так вот
3:31:53
тем самым мы поскольку это символ который не используется в нашем формализме построения формул мы явно
3:31:59
укажем где у нас что эта последовательность формулы и где формула начинается и заканчивается
3:32:05
мы ему тоже можем поставить соответствие какое-то число опять-таки c1 и так далее
3:32:11
c там какой то вес на p в степени с
3:32:18
лед и более того мы можем предъявить формулу сигма 1 причем формулу от n
3:32:25
смысл которая будет сводиться к следующему число n является кодом
3:32:30
последовательности форму н это кот
3:32:36
последовательности формул все абсолютно прозрачно аналогично
3:32:42
просто представляйте себе что вы на компьютере вот это дело пытаетесь запрограммировать вот самое главное
3:32:49
самое сложное здесь это вот вам дали какое-то число и вам надо его разобрать вот так то есть надо по степеням по его
3:32:57
разложить посмотреть на цифры и попытаться восстановить себя дерево разбора если получилось то и то то и то
3:33:04
то мы даем положительно ответствуй да и он действительно является последовательностью форму вот ну
3:33:11
соответственно дальше процесс развивается и мы говорим что мы еще вводим
3:33:16
формулу ax spinn несложно догадаться что эта формула будет нам нумеровать а все аксиомы если
3:33:25
мы считаем что наша теория т теория т эффективно axio мотивируем как
3:33:31
раз тот самый случай который чаще всего и встречается там и
3:33:36
про любой текст ну а любой текст нашем понимании здесь это просто произвольно натуральное число можем сказать что этот
3:33:45
текст с кодом n является какой-то из аксиом нашей теории т.е. это формула
3:33:51
будет обозначать что н есть кот
3:33:57
аксиомы
3:34:06
ну и последнее как бы штрих к портрету здесь
3:34:14
это самое главное формула которую мы определим это форму от
3:34:19
aten которая нам скажет что н это не просто
3:34:26
последовательность форму а это доказательство какой-то теоремы
3:34:39
не какой-то теорема что это доказательство
3:34:44
не догадаться существует доказательство до
3:34:49
что ну давайте прям так и напишем что в теории т выводим а формула имеющая номер н я вот так вот напишу в
3:34:57
кавычках значит что мы здесь хотим сказать нам
3:35:05
дали какой-то номер н мы запустили вот эту вот проверку оказалось что он кодирует формулу после
3:35:13
этого мы переходим к следующему этапу программы защиты значит притекать про и
3:35:18
проверяем а существует ли доказательства этой формулы в теории т пускаем цикл по всем
3:35:26
натуральным числам и проверяем является ли текущее число в этом цикле какой-то
3:35:32
последовательностью формул если у кей то переходит следующему этапу проверяем является ли эта последовательность
3:35:40
доказательством а доказательства проверять следующим образом мы смотрим являются ли эти формулы аксиомами для
3:35:46
этого у нас есть предикат и второе что мы проверяем можно ли получить если это не аксиома можно ли получить следующую
3:35:53
формулу по правил вывода из каких-то предыдущих форму то есть тут надо еще
3:35:58
выполнить проверку на то что с помощью модус потенции правила по
3:36:04
найса из аксиом и получается эта формула понятное дело это тоже все
3:36:09
алгоритмический проверяется ну не то чтобы просто но и сложно и в конце
3:36:15
концов если мы все это по успешно завершили а если они успешно завершают что за конечное число шагов естественно
3:36:21
то мы выдаем ответ да формула с номером n является
3:36:27
доказуемое ну и т.е. является теоремой теории т в других случаях когда она не является
3:36:34
номером теории теоремы теории ты у нас просто алгоритм зацикливается то есть
3:36:39
это получается некая сигма 1 формула вот это все это на это все 7 1 формулой
3:36:47
которые значит на кодах теорем за конечное число шагов
3:36:54
выдают положительный ответ она не кодах теорем зацикливаются
3:36:59
таким образом у нас есть некий предикат который представляет нам нумерацию
3:37:06
теорем нашей теории т ну или скажем так арифметики пеано для простоты
3:37:13
хорошо вот запомним этот факт что мы научились нумеровать теоремы скажем так – нить
3:37:20
перечисляете теорема собственном и этот факт уже даже использовали в предыдущей теореме о неполноте в синтаксической
3:37:27
форме когда я говорил что вот давайте предположим что умеем доказывать отрицание формула к тогда отсюда следует
3:37:35
что у нас есть алгоритм которые нумеруют нам вот это вот доказательство поскольку
3:37:41
аксиомы тоже надеру ему то у нас просто имеется логарифмический проверенный факт того
3:37:47
что эта теорема вот мы это использовать так вот если детально говорит то использовали мы вот что-то вроде этого
3:37:52
то есть такую вот нумерацию всех теорем нашей теории здесь работают эффективно
3:37:58
axe мотивируем из теории и то что все это задается рекурсивными
3:38:05
функциями потому что это сигма 1 формула ну и соответственно это все представимо
3:38:12
в нашей теории т и там еще применяется сигма 1 корректности или значительно
3:38:17
один полнота арифметики пеано а вот главный результат вот этих наших всех
3:38:23
упражнений с текстами построить вот эту вот форму вот н
3:38:29
теперь мы должны обратиться к еще одному факту
3:38:37
мат логике так называемой ли мя диагонали зации она же теорема
Теорема о неподвижной точке
3:38:42
неподвижной точке вот вообще надо сказать что неподвижная точка такой достаточно
3:38:50
мощный архетип математике потому что неподвижной точке есть и в мад логики и
3:38:56
в топологии и если значит официальных уравнениях в общем много где они есть и
3:39:04
дают много чего хорошего достаточно свой 3 ребра ура например или там
3:39:09
какой-нибудь устойчиво решение дюфур а вот в мад лайки тоже есть свои теорема неподвижной точке
3:39:16
крема по неподвижной точке
3:39:21
теорема это формулируется следующим образом
3:39:28
пусть а вот а
3:39:34
это какая-то формула от одного аргумента в нашей теории т ну то есть каком-то там
3:39:41
формализме причем мы считаем что даже если там еще
3:39:48
какие-то свободные переменные то они эффективно от того что вы в них что-то там подставляем это
3:39:53
результат формула не меняется но проще считать что просто одна свободная переменная
3:40:00
тогда и это вы все говорим про теории который
3:40:06
естественно эффективно ароматизируем и там ну то есть вот с который может искать работать при помощи
3:40:12
частично рекурсивных функций то есть вы ваще алгоритмов тогда существует
3:40:19
формула ты та которая является замкнутой
3:40:32
такая что в нашей теории т вот которая
3:40:37
вот этой сигнатуре соответственно мы можем вывести следующий факт
3:40:43
формул от это эквивалентно формуле а в которую вместо а
3:40:52
подставили номер формулы тета вот тут надо чтобы совсем вас не
3:41:00
запугать пояснить что это такое значит
3:41:07
вот все что я стёр надо вспомнить и
3:41:13
понять что коль скоро дана некая формула ты-то у нее есть номер но только что и
3:41:20
всех сумели перенумеровать причем достаточно просто даст по степеням простого числа взяли и записали
3:41:28
разложение мы берем formulated а это какой то текст мы его преобразуем в
3:41:34
число число ну назовём не знаю там такое c как кот formulated а давайте
3:41:42
цвет это назовем вот так это натуральное число эти вместо вот этой формулы а
3:41:49
возьмем просто по определению положим что это будет отрицание
3:41:56
то есть а от а заявляет нам что формула
3:42:01
с номером а не доказуемо в арифметике то есть нет нельзя найти
3:42:08
доказательства этой самой арифметики но такая формула воспользовавшись теорема неподвижной
3:42:14
точки на ё неподвижную точку от этой формулы и обозначим ее буквой же значит
3:42:20
пусть же такого что она эквивалентна отрицанию
3:42:27
на номере же тут как раз
3:42:33
получаем неподвижная точка что как бы не формально это это вот формула за
3:42:38
является сама сама формула же заявляет она говорит я и доказуемо то есть такой
3:42:45
аналог по парадокса лжеца формула же говорит меня нельзя доказать вот так
3:42:51
ну и теперь давайте посмотрим на теорему геделя о неполноте первую как
3:42:58
она формулируется она формулируется так что если теория непротиворечиво
3:43:05
ну точнее поскольку речь и слабо арифметики давайте сразу прям так вот и напишем
3:43:11
если риф митька пьян и непротиворечиво то тогда тогда она неполна то есть
3:43:22
существует формула же которая из нашей вот этой вот арифметики пеано
3:43:31
такая что в piano нельзя ни доказать же
3:43:36
ни опровергнуть же чем хороша эта формулировка мы явным образом указываем
3:43:42
как нам найти эту формулу же которая не доказуемо и неопровержимо то есть нам надо уметь построить формулу про найти и
3:43:50
неподвижную точку и вот это неподвижная точка она и будет собственно говоря вот этой независимой формулой теперь почему
3:43:58
так ну давайте посмотрим значит на варианты какие тут могут быть
3:44:06
ну во-первых предположим что формула же доказуемо в арифметики пеано
3:44:12
первый вариант пусть про выводит формулу же что это значит это значит что по
3:44:22
выводит формулу не же я вот уголки здесь теперь буду опускать
3:44:29
и номера лада чтобы было более прозрачная вот эта запись не
3:44:35
обремененная всякими символа но естественно предполагать что здесь натуральное число подставлена а не сама формула вот ну и что мы тогда получаем
3:44:43
тогда мы получаем что в по мы можем доказать что формула же
3:44:49
недоказуемо но мы тогда получаем явное противоречие
3:44:55
с тем что мы ее доказать с одной стороны силу вот этого перехода мы до умеем
3:45:00
доказывать вот это с другой стороне поскольку в plo доказуемо же то отсюда следует что вообще-то впо
3:45:10
доказуемо про же ну правда тут надо прибегнуть еще к так
3:45:17
называемой тереме либо о том что мы должны уметь переходить от жека пмж то
3:45:24
есть если доказуемо же ту можем доказать что доказуемо же вот ну как бы не
3:45:31
формально можно это сказать так что если у нас есть доказательства формулы же
3:45:37
значит у нас есть доказательства формы уже мы можем вот этот вот это доказательство весь этот вывод за
3:45:43
нумеровать и по цене и по у нас получится что у формула же окажется истинной вот это все доказуемо в паб и
3:45:51
почему потому что предикат вот этот позже он представляется в арифметики пеано вышли
3:45:57
май функцией соответственно вычисли масть вот этого вывода
3:46:04
формального она погружается в нашу арифметику и таким образом можем доказать позже ну тогда получается что
3:46:09
вот совместно из этих двух условий следует что п р ж и не псж доказуемо в
3:46:16
арифметики пеано давайте так напишем п р и неппер
3:46:22
а это не что иное как тождественно ложь то есть в арифметики пеано выводим а уж
3:46:28
а это означает противоречивость арифметики пеано то есть не con по
3:46:35
в противоречие с тем что мы получили вот здесь ну и второй вариант остается
3:46:43
допустим что не выводим они же то есть да будет допустим что выводим они же но
3:46:52
тогда получается что у нас
3:46:59
имеет место следующее ниже эквивалентно отрицанию вот этой формулы тогда
3:47:06
получается что арифметики пеано доказуемо плз
3:47:12
то есть мы можем доказать что
3:47:17
формула же доказуемо и тут опять я сейчас не буду отвлекаться на так
3:47:24
называемые аксиомы геделя либо для модельной логике но а прибегну просто как такому
3:47:31
неформальному объяснению до поскольку мы можем доказать что существует доказательство формулы же это значит что
3:47:38
мы можем предъявить что-то алгоритм который дает нам это доказательство как
3:47:43
только мы вытащили саму строку которая является доказательством фуру вы же мы
3:47:49
эту строку просто берем и говорим а вот вам она и есть доказательство формулы же то есть таким образом мы отсюда просто
3:47:56
извлекаем из из вот этой вот как бы сентенции до из этого вывода мы
3:48:01
извлекаем более простой вывод о том что в по выводим а формула же но тогда получается снова
3:48:10
противоречия выводим они же и выводим а же мы снова получаем что теория пьян они
3:48:17
совместно поэтому если мы предполагаем что теория пиана совместно то не выводим они же не ниже
3:48:25
так ну и наконец переходим к непосредственно к кости 2 теоремы говорю о неполноте для начала вспомним что мы
3:48:33
определили такой предикат который в арифметике выражает доказуемо
3:48:40
стиле магических формул то есть если мы говорим что какой-то формулы а это то же самое что в
3:48:49
по можно доказать формулу а ну имеется виду замкнутые формулы естественно
3:48:56
вот поэтому здесь еще можно так сказать что поскольку этот предикат является сигма 1
3:49:02
формулой 1 сигма 1 форму мы знаем теорема 7 1 пола те для арифметик не
3:49:08
только для планы для более слабых и это означает что истинность этого предиката в модели ну естественно когда здесь
3:49:17
натуральное число это номер какой-то формулы эквивалентно по сути тому что у нас сплавы вадима эта формула
3:49:24
это по определению истинность в модели по теореме о сигма 1
3:49:31
полноте также означает что у нас в по выводим а
3:49:36
выводим сам этот предикат то есть вот номера формулы а вы отсюда мы в общем
3:49:45
сразу можно увидеть одно из основных свойств предикаты доказуемо sti то что сам предикат и
3:49:52
выводимость самого предиката доказуемо stick его лента выводимости формулы а ну вот одно из свойств сейчас здесь коротко
3:49:58
запишем выглядит так в по
3:50:05
вадима формула а тогда я только тогда когда впо выводим предикат наказуемости
3:50:11
формулы а заметим что это довольно сильное условия
3:50:19
на приди к доказуемо если тем не менее для данного конкретного предикаты которые мы строили перед этим собственно
3:50:25
ради чего и были все эти наши построения с нумерацией алфавита форму вот со всеми
3:50:32
этим предикатами выражающими то что число натурально является кодом форму и
3:50:38
потом доказательства вот это все было ради того чтобы было вот такая аппликация
3:50:43
заметим что когда мы только что доказывали теорему первую терема году я неполноте мы как раз этим пользовались и
3:50:50
в ту и причем ее другую сторону следующее свойство предиката наказуемости собственно говоря такое
3:51:00
в нашей арифметики мы можем доказать что если доказуемо импликация а
3:51:09
следует б то есть тоже какая-то формула замкнутая мы посчитали ее номер именно
3:51:17
всей формулы с импликации да то тогда отсюда будет следовать
3:51:22
импликация следующего вида формула а доказуемо тогда формула-б доказуемо
3:51:32
то есть получается что вот этот как бы оператор прах его можно
3:51:40
вносить вот импликацию он как переходит на элементы аппликации на посылку и на
3:51:46
вывод и все вместе это оформляется и меня как теорема теории piano ну на
3:51:52
самом деле это достаточно простое и понятное правило общем-то это иллюстрация модус понос и
3:51:58
третье свойство это формализация вот этого отношения но только в одну сторону
3:52:04
слева направо вы это ну так впо доказуемо что из а
3:52:11
что из доказуемо stea
3:52:17
следует доказуемо сть
3:52:22
доказуемо sti а тут я пропускаю хотите символ выиграл of
3:52:29
угловые скобки местами ну понятно что всё это можно восстановить это теорема арифметики пеано по сути
3:52:38
являются формализации вот этой импликация только в одну сторону то есть здесь мы это убираем
3:52:43
вот здесь сказано что а доказуемо то есть вот оно здесь сказано что
3:52:49
доказуемо стo можно доказать вот собственно это она есть как бы более
3:52:54
сильный принцип но если здесь мы можем в обратную сторону повернуть в ряде случаев для конкретного нашего предиката
3:53:00
про то вот здесь уже не получится ну вернее как тут там помог полных
3:53:06
теориях может только бы вернуть назад а так нет теперь мы как обычно немножечко это все дела об
3:53:13
общин во первых мы дадим следующие обозначения а
3:53:22
именно символ бокс который часто используются в логике
3:53:28
пусть у нас есть просто какой-то предикат который что-то говорит нам про формулу
Аксиомы Гёделя-Лёба в модальной логике
3:53:35
ты-то где то это замкнутая формула то есть неважно на самом деле это просто
3:53:40
какой-то арифметический предикат с одним с одной переменной свободная и мы вместо этой переменной подставляем формулу ты
3:53:47
там вот вместо этого мы будем писать box ты-то это просто короче ну конечно
3:53:54
подразумевается под боксом именно связь с предикатом наказуемости вот но в общем
3:54:00
случае для разных теорий притекать доказуемо sti может определяться по-разному вот и он как раз вводится
3:54:08
не при помощи карт леской нумерации как мы это делали только что внутри
3:54:14
арифметики пеано вводится при помощи просто набор axium вот и вот следующие
3:54:19
аксиомы которые мы для этого оператора бокс приведем это по сути повторения вот этих трех аксиом свойств оператора
3:54:26
доказуемо sti которые можете переформулировать вот в таком виде и эти аксиомы называются
3:54:34
аксиомами удалять либо или гилберт одеты либо в общем случае давайте так назовем
3:54:41
да и к ним применяются отыщи слова условия вместо аксиом условия модуля
3:54:48
люба и они формулируются с используем вот этого
3:54:54
бок со следующим образом значит первое
3:55:01
если в теории т
3:55:08
выводим а формула а то тогда
3:55:13
в теории т выводим box-а формула бокс а то есть тот ровно то самое что мы
3:55:20
подразумеваем только без это куча дополнительных значков да по теории т понимается естественно
3:55:28
какая-то арифметическая теория ибо теории в которой мы можем право дозировать арифметику вот ну чаще всего
3:55:34
так потому что потому что нам кое-что нужно вычислять дальше второе условие года люба давайте
3:55:43
здесь так или 1 из 2 это выражение вот этой ну то есть
3:55:50
возможность внести наш символ бокс под импликации теории t должно быть у вадима
3:55:57
следующая теорема box-а следует б
3:56:03
тогда box-а следует бокс b и
3:56:13
третье третье аксиома либо это значит в теории
3:56:18
т выводим а следующая импликация если бокс
3:56:24
ту бокс бокс а это вот
3:56:30
представление вот этого ну и поскольку как мы рассказали предикат наказуемости стандартные в арифметике которые
3:56:37
вводятся как сигма 1 формула подчиняется вот этим правилом и даже более жестким
3:56:42
случае вот здесь вот поворота в обратную сторону импликации то понятное дело что
3:56:47
бокс определенные через предикат наказуемости в арифметики пеано он удовлетворяет эти максимум то есть мы
3:56:54
можем пользоваться свойствами предиката доказуемо sti арифметики пеано так как будто просто введен при помощи условий
3:57:01
идет либо чем эти условия хороши в принципе мы 10 ничем не ограничиваем нашу теорию
3:57:08
и по сути это ничто иное как кусок аксиоматике модальной логике модальная
3:57:15
логика это теория которая занимается изучением праздных логик то есть если до этого мы
3:57:22
смотрели на формальной системы как на объект изучения математической теории мета теорий то теперь мы поднимаемся еще
3:57:29
выше и вводим понятие модельной логике am анальная логика изучает
3:57:35
выводимость внутри вот этих всех формализма формальных систем и вот это
3:57:40
есть аксиоматика модель налоги на самом деле там есть еще пара принципов которые там какие-то водятся какие-то не водятся
3:57:47
в общем как в любой теории мы какие-то аксиомы добавляем какие-то нет зависимости от наших потребностей ну и
3:57:54
теперь собственно говоря приведем теорему либо которая
3:58:01
доказывается именно от в чистой модельные логике сейчас как бы мы немножечко на время забываем о том что мы идем к
3:58:09
вторую теореме геделя я бы арифметики доказываю такой чисто чисто формальную
3:58:18
теорему в модельной логике значит теорема звучит так
3:58:23
теорема люба если в теории т
Теорема Лёба
3:58:30
можно доказать вот такую такую импликацию такую теорему
3:58:36
из доказа из доказуемо stea следует сама а
3:58:42
то тогда в теории т доказуемо а
3:58:48
ну опять-таки мы этому боксу сейчас не придаём вообще не какой смысл но если
3:58:54
придать и так сказать погрузиться вашего наши до этого построения проведенные в
3:58:59
арифметики пеано то по сути теорема означает что если мы из
3:59:05
наличия доказательства формула а смогли вывести самую формулу а да то есть когда
3:59:10
у нас есть доказательства и тогда мы видим что формулой а истина тогда у нас в теории есть доказательства самой
3:59:16
формулы а на так немножко запутанного звучит тем не менее она очень полезно оказывается во всех вот этих
3:59:23
рассуждениях модельной логике ну давайте и докажем
3:59:30
доказательства такое ну в общем то достаточно техническое единственное
3:59:35
посыл здесь надо было догадаться о том с какой формулу начать начинаем мы со
3:59:41
следующей формулой мы придумаем такую вот форму был а
3:59:47
которая по сути выражает то что здесь написано но только вот этот бокс мы
3:59:53
заменяем на его определение опять же я говорю что это этот п.р. это просто
4:00:00
сейчас какой-то предикат мы забываем о том что и как он построена что он сделал это сказать и про его свойства мы просто
4:00:07
знаем что вот так связан с боксом a box удовлетворяют этим условиям и мы пишем что это у нас будет вот переменной а
4:00:15
импликация формула а формула то самое которая задана в
4:00:21
условии теорему либо ну дальше мы вспоминаем теорема
4:00:27
неподвижной точке да тут надо заметить что теорема неподвижной точке она использовала
4:00:33
предикат подстановки когда мы в диагональным методом подставляли форму и
4:00:40
же собственный номер вот соответственно у нас в теорий ты должен реализовываться предикат подстановки поэтому на то все
4:00:47
таки есть некоторые ограничения а именно она все таки должна быть какой тариф мотивируем а теория то есть
4:00:54
там должна быть какая-то часть арифметики или слабой арифметика или же она должна увидеть интерпретировать
4:01:00
эту самую арифметику например это может быть теории множеств ну и так дальше
4:01:05
предполагаю что ты арифметическая теория и предполагая вот это условие которое здесь написано задаем такую формулу и по
4:01:13
теореме неподвижной точке ищем-ищем решение этого уровня соответственно
4:01:19
из терема неподвижно точки следуют что в теории т выводим а следующая ки лоренци это
4:01:25
эквивалентно бокс это следует а
4:01:32
здесь я просто номер ты-то подставил сюда и применил вот это определение получилось бокс тета и так мы видим что
4:01:39
вот это это как бы корень уравнения вот этого эквиваленте и вот отсюда мы и
4:01:45
пойдем доказывать вот этот мы действуем следующим образом давайте нумеровать наши шаги значит
4:01:53
первый шаг во первых из того что мы умеем доказывать и ковариацию понятное дело мы умеем доказывать импликацию то
4:01:59
есть и стал эстета следует вот это напишем ест это следует да здесь я везде
4:02:07
впереди предполагают этого водянистые выводим а все что здесь пишу вопрос не
4:02:12
захламлять значит текст я вот один раз здесь укажу и все это выводим а если это следует
4:02:22
бокс то это следует хорошо это мы определили применили определение самой неподвижной
4:02:30
точке тета следующее что мы делаем мы видим что это
4:02:35
у нас некая импликация для импликации у нас есть соответственно вторая аксиома люба
4:02:42
давайте ее применять так
4:02:48
да прежде чем перейти к этой мы должны применить первое потому что мы хотим навесить бокс на всю эту формулу значит
4:02:55
навешиваем бокс что у нас будет бокс это импликация
4:03:04
бокс то это следует а мы привели el1
4:03:10
теперь наконец мы можем применить у нас стоит импликация под боксом применяем
4:03:15
вторую аксиому получаем то есть вносим бокс под импликацию мог ст это следует
4:03:22
бокс бокс ты то следует
4:03:29
ok это мы применили l2 теперь мы видим что у нас опять есть вот
4:03:35
кусок этой формулы это бог стоящей перед публикацией мы снова применяем эту
4:03:40
теорему раз как бы внесение бокса в эту импликацию выводим
4:03:46
а в нашей теории то мы можем продолжить эту импликацию и получить на
4:03:53
следующем шаге спасибо правила силлогизма следующий вывод
4:03:58
бокс это следует значит вносим получается бокс бокс это
4:04:08
следует бокс а это мы применили снова il-2
4:04:18
так теперь мы видим что у нас бокс а по сути выводится из двух посылок
4:04:24
из бокса это и бокс бокс это но мы знаем вот такую аксиому что есть бокс это
4:04:29
влечет бокс бокс тета2 место поставляем тета зафиксируем этот факт бокс это
4:04:37
влечет бокс бокс это но тогда комбинируя это
4:04:44
эту теорему с этой теоремы да мы понимаем что бог стоит а условия более
4:04:49
сильная чем бокс бокс это значит вот это условие можно выкинуть она и так следует
4:04:54
отсюда и у нас получается просто импликация отсюда сюда еще здесь мы применили или три а
4:05:02
на шестом шаге мы применяем мы просто комбинируем 4 5 шаги вместе
4:05:09
получаем бокс это влечет box а
4:05:17
это у нас 4 5 шаги вместе
4:05:27
так теперь мы вспоминаем о том что у нас
4:05:32
есть условия теорема мы находимся в условиях теорема либо которое нам
4:05:38
говорит что бокса влечет влечет саму а зафиксируем это условие
4:05:43
здесь бокса влечет сама к это просто условия
4:05:49
теоремы ну и теперь нам нужно снова применить
4:05:56
силлогизм то есть у нас бокс это следует бокса бокса следует а значит 8 шаг бокс
4:06:05
это влечет а
4:06:12
это у нас получается 6 и 7 правило 6 7
4:06:17
теорема теперь смотрим на вот эту штуку и
4:06:24
понимаем что у нас формул от это эквивалентно вот этой теореме просто моя
4:06:30
так выбрали эту самую эту поскольку это неподвижная точка была поэтому да здесь мы применяем в одну
4:06:38
сторону аппликация по определению в обе поэтому мы совершенно спокойно можем взять теперь импликацию в обратную
4:06:44
сторону и из вот этой вывести саму формулу тета поэтому на девятом шаге мы говорим что в
4:06:52
теории т мы вывели саму формулу ттт то оказалось истинной напоминаю у нас тут
4:06:57
впереди везде стоит что вы вводим это все в теории ты вот значит отсюда мы
4:07:03
перешли сюда просто по определению тета ну и теперь нам нужно применить
4:07:11
следующий шаг мы воспользуемся аксиомой r1 и заметим что ест это следует бокс это
4:07:23
это просто el1 и ну и теперь комбинируя соответственно 9
4:07:33
[музыка] ну да мы применяем
4:07:40
так только здесь у нас импликация конечно
4:07:50
здесь вот так надо было поставить в.т. выводим а вадима бокс это вот это
4:07:58
аксиома или 1 ну и теперь мы что видим у нас бокс это истинно по десятому 10
4:08:06
теореме а по 8 теореме xbox ты это следует а применяем модус подлость и 11 теорема будет звучать так в.т.
4:08:14
выводим а.а. давайте укажем явно что это модус pole
4:08:20
dance то есть в итоге мы получили что в.т. мы
4:08:25
доказали теорему а что мы собственно и хотели вот ну то есть видим что такой достаточно простой лобовой формальный
4:08:32
подход и если надо черного было догадаться это придумать вот эту форму с неподвижной точке на которых сети явно
4:08:38
вот прям указывает условия теоремы либо и теперь мы можем применить собственно
4:08:45
говоря терему либо к тому чтобы получить вторую теорему
4:08:50
геделя о неполноте но сначала как обычно парочку
4:08:55
замечание замечание будут следующего вида мы
4:09:03
говорим о том что теорема что теория непротиворечиво при этом у
4:09:10
нас есть такое понятие определения того что тела и
4:09:15
непротиворечиво оно таково что в теории
4:09:21
нельзя получить противоречие то есть это у нас по определению
4:09:28
означает что в цель нельзя вывести ложь я вывести ложь
4:09:35
но до под ложным можно понимать любое можно
4:09:40
высказывать например то что 0 не равна null или что-нибудь еще арифметическая может
4:09:46
такое взять вот поэтому вот эти вещи как канте и
4:09:51
vt не не выводим а ложь это одно и то же и мы соответственно бою
4:09:59
операцию вот на это определение в стандартной модели это просто будет определяться как ровно то же самое что
4:10:04
невозможно доказать ложь по всем правилам time эти галочки
4:10:12
который означает что мы применили какой-то номер для для данного высказывания и подставили numeral то
4:10:20
есть соответственно утверждение о не противоречивости теории т это то же
4:10:26
самое что сказать что vt не выводим а противоречивые высказывания
4:10:32
ну и вот поэтому на так сказать формализация того
4:10:37
что в теории т не выводимое и совместность а это есть вторая теорема геделя
Вторая теорема Гёделя о неполноте
4:10:46
значит если теория непротиворечиво то внутри ее нельзя
4:10:54
доказать ее непротиворечивость нельзя доказать вот такую формулу нельзя доказать
4:11:01
что мы выводим а ложь
4:11:07
вот и давайте воспользуемся нашим перри обозначением для удобства и напишем что
4:11:12
это будет то же самое что в теории т не выводим a box ложь не бокс ложь
4:11:23
при этом предполагается что теория т арифметическое
4:11:28
вот потому что мы должны уметь вот это в этот весь аппарат там применять уметь кодировать нашу формулу погружать
4:11:35
предикат доказуемо sti в нашу теорию вот поэтому скажем теорема геделя
4:11:45
не ко всем теории может быть применена скажем так ну и вот вопрос как собственно говоря
4:11:52
доказать что вот из непротиворечивости т следует тот факт что нельзя
4:11:58
доказать вот такую формулу в теории т давайте в терему либо вместо у подставим
4:12:08
тождественно ложь посмотрим что получится теорема люба
4:12:14
берем вместо а подставляем ложь что у нас получается получается там следующее
4:12:21
если в теории т доказуемо
4:12:26
бокс ложь следует ложь
4:12:32
то тогда в теории т доказуемо
4:12:38
ложь и
4:12:45
поскольку мы считаем что у нас теория ты непротиворечиво понятное дело там доказуемо стью лжи там
4:12:53
быть не может тогда учитывая посылку 2 теле мику доля
4:12:58
то что если теория если теория ты непротиворечиво
4:13:04
мы отсюда заключаем что вот это неверно раз неверно этот универ на и вот это
4:13:11
тогда получается что у нас в.т. ложь не выводим а
4:13:17
отсюда по теореме люба мы получаем что не выводимое вот это то есть vt не
4:13:24
вадима бокс ложь
4:13:30
следует лошадь
4:13:36
осталось вот эту формулу упростить по обычным логическим правил для то есть у
4:13:41
нас есть некая импликация выводе стоит 0 чему будет эта формула эквивалентно это
4:13:48
формула эквивалента просто-напросто не бокс ложь
4:13:54
таким образом мы получаем что
4:14:00
в теории темп не выводим а формула говорящая что невозможно
4:14:07
доказать ложь здесь я все-таки верну обратно то что это было уже нет ни определение конты которые здесь было
4:14:14
написано а это было перри формулировка вот этой штуки вот так
4:14:21
то есть на самом деле все из терема лёва все получается очень просто мы берем
4:14:27
вместо а подставляем ложь видим что если мы хотим чтобы теория была непротиворечиво как в посылке теорему
4:14:33
геделя то получается что вот это неверно раз это неверно то это верно и это а это
4:14:39
мы просто преобразовали упростили по правилам гулевская алгебры получается здесь не не бокс ложь но это утверждение
4:14:48
это и есть утверждение о совместности теории т то есть теллариты невозможно
4:14:54
доказать ложь мы можно по-другому это переписать что получается что vt необходимо can t
4:15:02
собственно это и есть утверждение вторую теорема геделя о неполноте то что мы если теории непротиворечиво то
4:15:09
она и умеет оказывается вы собственную непротиворечивость ну еще один
4:15:14
занимательный факт связан это же с таскать с неподвижными точками это
Теорема Тарского о невыразимости истины
4:15:20
теорема тарского о невыразимо sti истинности в арифметике
4:15:30
ну как мы уже отмечали есть такое понятие вырази масти
4:15:36
предикатов или определим асти предикатов теории которая будет следующая значит предикат
4:15:43
какой-то предикат p от свободной переменной а выразим
4:15:50
в арифметике это
4:15:57
означает что для любого натурального числа а а прям лежит нашему предикату п ну то есть
4:16:05
там подмножество тогда я только тогда когда соответствующая формула да давайте
4:16:12
. без on fashion предикат п как подмножество натурального
4:16:18
ряда выразим в арифметике тогда только тогда любого а принадлежит по тогда и только тогда когда
4:16:25
соответственно формула существует некая формула задающие the predicate которая истинно
4:16:31
на соответствующем набирали вот так вот да уже ничто не мешает взять стандартную
4:16:39
модель и рассматривать все истины и замкнутые формулы в этой модели есть даже такое
4:16:45
такое обозначение теория модели
4:16:50
н со своей там сигнатурой это все замкнутых формулы которые истины в этой
4:16:58
модели это как получается то что называть элементарной моделью
4:17:03
элементарной теории данные модели вот так вот давайте предположим что вот
4:17:09
мы взяли но что всех истинных форму которые в данной модели выполняются
4:17:15
то есть не в теории pian доказуемо именно истины в модели у них у всех у
4:17:20
них есть номера какие-то то есть мы их вашу перенумеровать при помощи гиады русской нумерации и мы можем сопоставить
4:17:27
вот эта теория множество ну скажем назовем его t
4:17:35
всех таких номеров что формула с номером n истинно
4:17:43
стандартная модель то есть формула истинна где
4:17:48
n это номер этой формулы и вот взяли такое множество ну и возникает
4:17:56
вопрос вот это множество вот этот предикат можно ли выразить в арифметике или нет то что это притекает понятно
4:18:03
душит подмножество натурального ряда оказывается нет и этой как раз есть суть теоремы тарского у
4:18:09
невыразимо sti истинности начнут давайте предположим что все-таки истинность выразим а
4:18:17
вот до оформят как теорему теорема тарского царского по
4:18:25
невыразимо sti еще и же иногда пишут о не реквизируем асти истинно
4:18:34
значит не существует такой вот формула мы ее назовем
4:18:42
замкнутая формула языке арифметики пеано не замка с одной свободной переменной от
4:18:48
а в арифметике ты она такой что
4:18:56
стандартной модели в стандартной модели
4:19:02
истинно формула а тогда я только тогда когда
4:19:11
в этой же самой стандартные модели истинно форму otter от номера а
4:19:21
ну это даже более сильное утверждение чем что-то мне хотя ну да выразилась
4:19:27
получается вот ну заметим что в частности не существует тем более не может существовать такого предиката
4:19:33
чтобы возьмите kipi она была доказуемо то для истинных форму а вот мы знаем что
4:19:40
до 7 форму это работает а вот вообще для всех истинных формул это не так но здесь
4:19:45
даже еще более сильное утверждение получается которая говорит что вообще даже в модели мы них не можем определить
4:19:51
предикат который бы выражался формулой с одной стороны
4:19:58
критики piano с другой стороны была при этом истинен ровно также где истины сами
4:20:03
формула ну доказательства такое предположим что такой предикат
4:20:10
существует пусть существует такой предикат тоже от а
4:20:16
тогда мы возьмем неподвижную точку его отрицание пусть
4:20:21
в арифметике выводим а
4:20:26
тут уже не пусть до потери полями а неподвижной точке мы просто получаем что
4:20:35
есть такая формула ты та которая эквивалентна то есть и это
4:20:42
доказуемо в арифметике эквивалентно отрицание от своего номера
4:20:48
то есть ровно та же сам прием который используется при доказательстве 1 тереме удали да мы там искали форму которая не
4:20:56
доказуемо и неопровержимо ровно тем же способом только вместо ты расстаял приди к доказуемо sti
4:21:02
ну хорошо допустим это так но мы знаем что всякая теорема доказуемая в про она
4:21:09
же истина будет и в модели вот сюда пойдем
4:21:14
она же будет истинно и в модели это свойство корректности
4:21:19
исчисления предикатов получается что в нашей модели истинно то что формула ты то естественно
4:21:28
тут предполагается что мы и про интерпретировали в модель там все лежащие операции выполнены она будет
4:21:34
эквивалентно не от своего номера
4:21:39
вот а номер считается на основе языка в котором это формул написано языка пиана
4:21:46
ну и дальше что мы видим давайте рассмотрим два кейса тут ровно то же самое что в парадокса лжеца происходит
4:21:53
предположим что ты это истинно что тогда тогда получается что неверно
4:22:01
вот это [музыка] неверно 3 вот это
4:22:08
но неверность ну то есть сложность ты рад это даже можем прямо вот так написать
4:22:14
так как то сложно ложность этой формулы в модели
4:22:23
да а в модели все формы и либо истина либо ложно третьего не дано значит
4:22:28
навешивать здесь вот отрицание ложного в модели эквивалентно ложности самой формулы все сюда будет следовать что это
4:22:37
ложно и вот мы из истинности то получаем важность это не ровно тем же самым прием
4:22:43
предполагаю что это ложно мы получаем что тогда будет истинно от это
4:22:51
ну а истинность а ты такой вариант на истинности тета то есть это будет истину
4:22:56
короче говоря из получается привод своего слова повторения парадокса лжеца
4:23:02
в любом случае мы получаем противоречие но и отсюда получается что у нас действительно истинность в модели она не
4:23:08
выразимо арифметическим предикатом поэтому правильнее говорить на самом деле не теорема он не выразил
4:23:14
естественности а теорема о не арифметически истинности опять-таки истинности стандартной модели
4:23:21
то есть тут всегда надо немножко говорится ну собственно на этом мы
4:23:27
завершаем разбирательство с 2 теорема геделя о неполноте напоминаю главный прием здесь был в том
4:23:34
чтобы некоторым способам очевидным алгоритмическим пронумеровать все формулы и все term и которые заданы
4:23:41
в нашей теории построить предикат которая оказывается ко всему прочему ещё
4:23:46
и сигма 1 формулой далее на самом деле для второй теряем говорят не так важно
4:23:52
как я уже говорил далее показать что для него выполняются условия для любой и с
4:23:58
их помощью с помощью теоремы либо собственно говоря получить то что из совместности теории
4:24:06
they совместности арифметики собственно говоря ну какой-нибудь арифметики
4:24:11
не выводим а значит если теория совместно то в ней
4:24:18
нельзя доказать его собственную совместность то есть теория не умеет про себя доказывать свою собственно
4:24:24
непротиворечивость это и есть суть 2 теорема геделя о неполноте принципе некоторым образом рассуждая
4:24:32
более поверхностно можно и из первой цели мы гадали о неполноте получить вторую теорему а
4:24:38
вот но я решил что будет более правильно провести вас именно через вот этот вот
4:24:43
формализм модальной логике с аксиомами году либо чтобы показать как наиболее
4:24:48
строго в современном виде показываются эти теорема всем пока
4:24:56
[музыка]
4:25:04
[музыка] а [музыка]