2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки


Правила форума


Посмотреть правила форума



Начать новую тему Ответить на тему На страницу Пред.  1, 2, 3  След.
 
 Re: Метатеоремы
Сообщение23.11.2019, 19:14 


17/08/19
246
arseniiv
Спасибо, про объекты понял.

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

Читаю Шенфилда - у него функции и отношения, когда еще и $ZFC$ близко нету.

Или про алфавит. Вот есть алфавит. Что это такое? Конченый или счетный набор каких-то различных символов. А что такое счетный? Натуральных чисел же нету пока еще.

И так во всем.

Вобщем, мне бы почитать что-нибудь, где с самого начала объяснялись бы элементарные вещи, причем строго. Я уже поднимал вопрос про литературу, но там я его слишком широко поставил. У меня основное желание - разобраться с основаниями. Причем меня интересует то, что идет либо "до" $ZFC$, либо "параллельно" с $ZFC$. Сама $ZFC$ не очень интересует.

 Профиль  
                  
 
 Re: Метатеоремы
Сообщение23.11.2019, 19:39 
Заслуженный участник


27/04/09
28128
oleg.k в сообщении #1427356 писал(а):
Тем не менее я так и не разобрался, где дно и как оно выглядит...
Дном может быть только неформальная теория, общественные соглашения (и в математике это не какие попало соглашения, а довольно чёткие), просто из-за того как устроен человек. У нас очень похожее устройство психики, и одно это сильно помогает нам понимать друг друга, но если бы у нас был какой-то неизменный формализованный кусок чего-то прямо в головах, и мы бы были несомненно уверены в том, что он у всех одинаковый, мы могли бы (может быть — это уж больно гипотетично и я не могу быть уверен) строить башню формальных теорий прямо с него, он был бы дном. А так нет.

-- Сб ноя 23, 2019 21:48:59 --

oleg.k в сообщении #1427356 писал(а):
Или про алфавит. Вот есть алфавит. Что это такое? Конченый или счетный набор каких-то различных символов. А что такое счетный? Натуральных чисел же нету пока еще.
А почему нету? Вас пугают нестандартные модели арифметики? Вы ведь вряд ли разойдётесь с другими людьми (математически подкованными, а не теми, кто объявляет 0 ни чётным, ни нечётным) в базовых операциях и отношениях от конкретных натуральных чисел. Почему бы и не принять тогда, что они даны. Нам всё равно приходится доверять вещам просто так, никакая наука без этого не обходится. И потом, как уже заметил mihaild, результаты обосновывают нам, почему нам стоило довериться исходным положениям.

oleg.k в сообщении #1427356 писал(а):
Вобщем, мне бы почитать что-нибудь, где с самого начала объяснялись бы элементарные вещи, причем строго.
По-моему, такой литературы нет. Я уж не знаю как так выходит, хотя математику и популяризуют и вроде есть для таких текстов какая-то ниша. Считается, что или люди в конце концов принимают и понимают правила игры, или пускай уж проходят стороной (может они недостаточно пытались или может им это будет не особо полезно — в принципе довольно сносные аргументы для такого).

Вот скажите, удовлетворит ли вас (как сейчас видится) описание понятий в виде наборов операций, которые с ними можно делать, и соотношений, которым они должны удовлетворять? При этом эти операции и соотношения все записаны в виде утверждений конечной длины. (Но не обязательно в виде формализованной теории! чтобы не ходить как раз по кругу.) И вообще в каких свойствах таких простых понятий вы не уверены? Может, залатать дырки будет ещё быстрее.

-- Сб ноя 23, 2019 21:50:24 --

Когда-то у меня были подобные вопросы, но каким-то образом я от них ушёл и думаю теперь в другую сторону. Не могу сказать, что знаю, что именно надо сделать для этого, но я по крайней мере немного заинтересован кому-то с этим помочь.

-- Сб ноя 23, 2019 21:51:47 --

Хотя наверно не в такой степени как я тут несколько раз наблюдал. Из-за программирования или чего у меня всегда была какая-то уверенность в свойствах конечных строк или подобных структур.

 Профиль  
                  
 
 Re: Метатеоремы
Сообщение23.11.2019, 19:51 


17/08/19
246
arseniiv в сообщении #1427358 писал(а):
Дном может быть только неформальная теория, общественные соглашения (и в математике это не какие попало соглашения, а довольно чёткие), просто из-за того как устроен человек.
И пусть она будет неформальной. Ничего страшного. Именно эти соглашения мне и хочется узнать. Я их вижу так:

1. Мы можем отличить какой-то конкретный символ некоторого алфавита от кота.
2. Мы можем считать до ста (натуральных чисел мы не знаем) (вместо 100 можно взять число и побольше если потребуется, но конечное)
3. Если перед нами два символа, то мы способны сказать, различны они или совпадают.
... и т.д.

Никаких натуральных чисел, счетных алфавитов, булевых функций и т.д.

Об этом вообще где-нибудь написано?

 Профиль  
                  
 
 Re: Метатеоремы
Сообщение23.11.2019, 20:04 
Заслуженный участник


27/04/09
28128
Про различимость символов алфавита где-то точно писали, но этому обычно не отводится слишком много места.

Кстати гляньте Манина, например перевод (нескольких книг разом, насколько понимаю) на английский с дополнениями:
    Yu. I. Manin, Neal Koblitz, B. Zilber. A Course in Mathematical Logic for Mathematicians
— там ближе к началу есть немало отступлений на подобные темы (потом они уже оказываются не нужны и кончаются). Может быть будет достаточно, может нет, но гарантирующих проговаривание таких вещей источников пока не помню.

 Профиль  
                  
 
 Re: Метатеоремы
Сообщение23.11.2019, 20:06 


17/08/19
246
arseniiv в сообщении #1427358 писал(а):
Вы ведь вряд ли разойдётесь с другими людьми (математически подкованными, а не теми, кто объявляет 0 ни чётным, ни нечётным) в базовых операциях и отношениях от конкретных натуральных чисел. Почему бы и не принять тогда, что они даны.
Брауэр и Гильберт тоже вроде математически подкованными были :wink: Если серьезно, то я не понимаю, какие правила рассуждений приемлимы... На меня неслабо так парадокс Рассела подействовал. Я бы был удовлетворен, например, такой ситуацией. Есть конечная корзина способов рассуждений. Выбирается набор приемлимых рассуждений. Одна группа людей может выбрать один набор, другая группа - другой набор. Получили две (или $n$) нетождественные математики. Далее строим формальные системы, выбираем аксиомы, что-то доказываем и т.д. Но все это после декларации "правил игры".

 Профиль  
                  
 
 Re: Метатеоремы
Сообщение23.11.2019, 20:18 
Заслуженный участник


27/04/09
28128
(К предыдущему.) Кажется, туда попали (видел пару похожих кусков в определении рекурсивных функций и ещё где-то) в том числе его «Вычислимое и невычислимое» и «Доказуемое и недоказуемое»; это в какой-то степени популяризация — ещё есть его просто лекции, уж что из них на что повлияло, точно не знаю, но его лекции я особо не читал, потому что нашёл только в машинописном варианте, а этого мои бедные глаза не выдерживают.

oleg.k в сообщении #1427366 писал(а):
Если серьезно, то я не понимаю, какие правила рассуждений приемлимы... На меня неслабо так парадокс Рассела подействовал.
Но ведь он не логический: мы можем из логики вытащить всё, что его вызывает, в собственно теоретико-множественные аксиомы.

Вообще я бы предполагал, что классическое исчисление высказываний (не предикатов) должно бы быть можно спокойно принимать как данность. Там ничего страшного возникнуть ну просто не может (в каком-то смысле). Интуиционистское — в ту же коробку, хотя оно может настораживать людей; однако оно на деле ещё менее рискованная затея чем классическое исчисление (вот посмотрите на странный закон Пирса — он там не выводится). Логики первого порядка уже наверно имеют полное право немного настораживать. Логики второго порядка обычно пытаются без нужды никому не показывать (зато там можно определить равенство логически; с другой стороны это не «зато», а «ибо»).

oleg.k в сообщении #1427366 писал(а):
Но все это после декларации "правил игры".
Да, потому например была советская школа конструктивизма. Но я не думаю что так легко использовать какой-то не принимаемый никем способ доказательства и при этом самому не заметить что-нибудь странное. Если его получится свести к более надёжно выглядящим способам, и хорошо.

 Профиль  
                  
 
 Re: Метатеоремы
Сообщение23.11.2019, 20:48 


17/08/19
246
arseniiv в сообщении #1427369 писал(а):
Там ничего страшного возникнуть ну просто не может (в каком-то смысле).
Не могли бы Вы расшифровать этот фрагмент?

-- 23.11.2019, 20:51 --

Я просто где-то видел про какие-то сильные теоремы об исчислении высказываний, которые доказаны исключительно финитными методами. Вы об этом?

 Профиль  
                  
 
 Re: Метатеоремы
Сообщение23.11.2019, 22:07 
Заслуженный участник


27/04/09
28128
oleg.k в сообщении #1427376 писал(а):
Не могли бы Вы расшифровать этот фрагмент?
Это в том смысле, что пока мы не начинаем рассматривать совсем хитрые задачи, там ничего внезапного и неочевидного (и бесконечного) вылезать не должно. Например мы можем проверить любую формулу от $n$ пропозициональных переменных на то, тавтология она или нет, за $O(2^n)$ времени. Это конечно, хотя на практике обычно и неудовлетворительно.

oleg.k в сообщении #1427376 писал(а):
Я просто где-то видел про какие-то сильные теоремы об исчислении высказываний, которые доказаны исключительно финитными методами. Вы об этом?
Изначально нет, но навскидку я кстати сейчас не вспомню, какие бы из полезных теорем там требовали чего-нибудь нефинитного: выводы конечны, оценки переменных — конечные функции и т. д., выводы обычно конструктивно получаются, если например взять теорему о дедукции и другие теоремы о выводимости чего-то, если выводится что-то.

 Профиль  
                  
 
 Re: Метатеоремы
Сообщение23.11.2019, 23:07 
Заслуженный участник
Аватара пользователя


23/07/05
17973
Москва
oleg.k в сообщении #1427349 писал(а):
Someone в сообщении #1427334 писал(а):
Утверждение об объектах предметной теории является её теоремой.
А разве теорема предметной теории - это не последняя строка в доказательном тексте?
Да, конечно, это последняя строка в формальном доказательстве. Но только само это доказательство, как и всякий текст, является объектом метатеории.

 Профиль  
                  
 
 Re: Метатеоремы
Сообщение23.11.2019, 23:34 


17/08/19
246
А можно определить операции и отношения, не определяя функций и множеств?

 Профиль  
                  
 
 Re: Метатеоремы
Сообщение23.11.2019, 23:43 
Заслуженный участник
Аватара пользователя


23/07/05
17973
Москва
Можно. Посмотрите на арифметику Пеано. В ней нет множеств. Однако операции и функции благополучно есть.
А вообще, читайте учебники. Форум не предназначен для пересказа учебников.

 Профиль  
                  
 
 Re: Метатеоремы
Сообщение23.11.2019, 23:49 


17/08/19
246
Someone в сообщении #1427407 писал(а):
Можно.
Это слово закрывает большую часть моих вопросов. Теперь читать учебники станет гораздо проще.

 Профиль  
                  
 
 Re: Метатеоремы
Сообщение25.11.2019, 21:01 
Заслуженный участник
Аватара пользователя


28/09/06
10413
arseniiv в сообщении #1427369 писал(а):
Вообще я бы предполагал, что классическое исчисление высказываний (не предикатов) должно бы быть можно спокойно принимать как данность. Там ничего страшного возникнуть ну просто не может (в каком-то смысле).
Смотря что считать страшным. Я бы сказал, что различие между "следует" и "выводится" - уже довольно страшно. И возникает оно как раз в классическом исчислении высказываний.

 Профиль  
                  
 
 Re: Метатеоремы
Сообщение25.11.2019, 21:46 
Заслуженный участник


27/04/09
28128
Разве в классическом?

 Профиль  
                  
 
 Re: Метатеоремы
Сообщение25.11.2019, 23:26 
Заслуженный участник


02/08/11
6874
oleg.k в сообщении #1427361 писал(а):
Об этом вообще где-нибудь написано?
Я знаю одно место (я выделил жирным курсивом):
Н. Вавилов в Не совсем наивной теории множеств писал(а):
Потрясает наивность людей, которые считают, что понятия элемента, множества, функции, бесконечности, числа требуют дальнейшего анализа и обоснования, в то время как понятия символа, текста, конструктивного объекта, правильно составленной формулы, формального языка, выводимости, доказуемости, истинности ясны сами по себе. В действительности это иллюзия, обоснование математики с помощью логики - это обоснование прозрачного с помощью туманного.
<...>
Конструктивная математика опирается на тысячи неявных предположений, подразумеваемых, но не сформулированных аксиом. Кто может гарантировать, что за ночь в тексте не появляются новые символы и не исчезают старые, что мы в состоянии отличить один символ от другого.
Но это частное мнение одного математика. Я не знаю какой процент математиков с ним согласится, а какой будет спорить.

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 40 ]  На страницу Пред.  1, 2, 3  След.

Модераторы: Модераторы Математики, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: Mikhail_K


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group