Ну и зачем всё это нужно? Применение у этого есть?Хихи

(Reply to this) (Thread)

Применение тут такое, что я могу теперь читать Белла про булево-злачные модели

(Reply to this) (Parent)

Функтор это функция между объектами из разных математических миров?
МИМО гумапидор

(Reply to this) (Thread)

Да можно и так сказать.

Но эти математические миры называются категориями.

(Reply to this) (Parent) (Thread)

а может быть такое что функторы тоже образуют категории, какие-то функторы похожи на друг друга, и между функторами можно тоже функтор провести?
МИМО ГУМАПИДОР

(Reply to this) (Parent) (Thread)

Функторы между парой ктегорий тоже образуют категорию. И, да, между ними тоже бывают функторы.

(Reply to this) (Parent) (Thread)

И там че - бесконечный регресс?

(Reply to this) (Parent) (Thread)

Поче регресс? Прогрессия.

(Reply to this) (Parent) (Thread)

да, регресс это про причиность и аргументацию, скорее тогда рекурсивность и итерационность процесса "категории функтов категорий функтов..."

(Reply to this) (Parent) (Thread)

*функторов

(Reply to this) (Parent)

Хочешь сказать, во всём тобой написанном действительно есть какой-то особый смысл?.. :3

(Reply to this) (Thread)

Cсыслобычный, впрочем, как всегда

(Reply to this) (Parent)

Привет, я хочу узнать твое мнение о работах Ершова в матлогике, вроде симпатично.

(Reply to this) (Thread)

Это работы вполне серьезного мирового уровня. Эту область науки, где работает Ершов, я бы назвал алгебраической теорией моделей. А теория моделей это вполне серьезная математика.

Но я н читал их, поэтому ничего конкретно сказать не могу. И про личность Ершова тоже.

(Reply to this) (Parent) (Thread)

Андрей Петрович Ершов был не только замечательным учёным, учителем и борцом за свои идеи, но и выдающейся, разносторонне одарённой личностью: он прекрасно играл на гитаре и пел, писал стихи, переводил на русский язык английских поэтов, в частности, Редьярда Киплинга.

Умер после тяжёлой болезни.

(Reply to this) (Parent)

Ершов, Юрий Леонидович
Проект «Новосибирск» (уровень III, важность высокая)

(Reply to this) (Parent) (Thread)

Что за проект "Новосибирск"?

(Reply to this) (Parent) (Thread)

уровень III, важность высокая

(Reply to this) (Parent) (Thread)

Это что-то из википедии?

(Reply to this) (Parent) (Thread)

https://computer-museum.ru/books/n_mozaika/ershov2.htm

это наверное

(Reply to this) (Parent) (Thread)

Не, я писал про Юрия Леонидовича, там правда на википедии проект "Новосибирск", важность высокая, уровень доступа III

(Reply to this) (Parent) (Thread)

Так что же это такое - эта ваша загадочная Теория Нумераций? Постоянно слышу что Колмогоров ею занимался, но сегодня такой дисциплины вроде нет

(Reply to this) (Parent) (Thread)

Нумерация, это техника, которую использовал Гедель в своих теоремах о неполноте.

Наверное это такая теория про обобщения таких доказательств.

(Reply to this) (Parent)

У почти-консистентной теории существуют почти-модели?

(Reply to this) (Thread)

Не знаю. Наверное, в этом нет большого смысла.

Если вы не уверены консистентна ли теория, то можно предположить, что у нее есть модель, а потом построить на ее основе новую с желаемыми свойствами. Такие модели, конечно, будут воображаемыми.

(Reply to this) (Parent) (Thread)

допустим, мы знаем, что самое короткое доказательство противоречия - очень длинное. есть ли тогда нечто, что можно считать "локально" моделью?
например, добавим к ПА отрицание частного случая теоремы Крускала.
эта теория выводит кучу истин о стандартных натуральных числах и почти никогда - ложь

(Reply to this) (Parent) (Thread)

> о стандартных натуральных числах

стандартных - ужасно лишнее здесь слово, сорри

(Reply to this) (Parent)

В теории моделей все протворечивые теории будут эквивалентны. Но кажется я понял, что ты имеешь в виду.

С точки зрения теории доказательств можно действительно оценить сложность какого-то доказательства. Например в ПА можно считать число индукций. А если, например, индукция используется для доказательства шага индукции, то это будет индукция в квадрате. В итоге у каждого доказуемого утверждения будет своя степень, многочлен в целых числах типа I^2 + 2I.

Тогда для противоречивых теорий можно посчитать степень противоречивости как степень утверждения bot. Модели в теории доказательств вроде не особо расматривается. Но можно попробывать посчитать расстояние от теории до не-модели как минимальную степень утверждения, которое не верно для модели. Потом этих степей можно вычислять численное растояние между теориями и моделями типа как d(T,M) = 2^-(deg(T,M)(2))

(Reply to this) (Parent) (Thread)

Хочется что-то уметь сказать про эту квазимодель, если расстояние мало.
В моем примере утверждения, имеющие обозримые доказательства, истины в достаточно большом и полезном куске квазимодели. (кажется)
Изучается ли что-то такое?

(Reply to this) (Parent) (Thread)

Я прямо такого не встречал.

Вам бы я посоветовал для начала формализовать, что значит "большой и полезный кусок квазимодели", как отличить его от "маленького" или "бесполезного", и что такое "обозримое" и "необозримое" доказательство.

(Reply to this) (Parent) (Thread)

Нет, именно это я это формализовать не хочу, это будет ультрафинитизм, а я не к тому клоню, а думаю про чтото типа этого
https://gowers.wordpress.com/2008/12/28/how-can-one-equivalent-statement-be-stronger-than-another/

(Reply to this) (Parent) (Thread)

Гауэрс еще чтото говорил конкретно о ситуации, когда вывод противоречия очень длинный, но я не могу найти

(Reply to this) (Parent) (Thread)

Ну вот видите, что вы все равно апеллируете к длине доказательств.

Proof Complexity, это вполне себе формальная дисциплина.

Вот, статья например https://arxiv.org/abs/1802.09377

(Reply to this) (Parent) (Thread)

спасибо, попробую подступиться к этой дисциплине.
еще дурацкий вопрос:
как думать про омега-противоречивые теории типа PA+~Con(PA)
тут выполняются условия Гильберта-Бернайса?
эта теория П1-некорректная?

(Reply to this) (Parent) (Thread)

Я не специалисты по этой теме, и точно не знаю. Я видел примеры, что теории типа X= ZF + ~Con(ZF) могут быть относительно непротиворечивы. Тут тонкий вопрос как Сon(Y). Потому что Сon(Y) должен записываться на языке теории множеств или арифметики нужного порядка, а не на мета-языке. Поэтому нельзя просто подставить X само в себя и получить противоречие.

(Reply to this) (Parent) (Thread)

Конечно. Критерий того, что Con выразимо и есть условия Г-Б. Традиционно(*), первая ТГ требует только первые два условия, а вторая - еше третье, потому что не только Con должен выражаться, но и все доказательство первой ТГ.
Это тонкость, которую я понимаю, но обращаться с ней не умею.

(*) Традиционно: заметил, что последнее время роль чисто синтасического док-ва первой ТГ перестали подчеркивать. Рассказывают, что Россер "усилил результат".

(Reply to this) (Parent)

а ты не в курсе как в модальной логике определяются операторы necessary и possible, через возможные миры базово?

(Reply to this) (Thread)

В логике возможных миров возможность это отношение между мирами.

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

possible значит, что cуществует мир, возможный для нашего мира, где выполняется аргумент. То есть если я говорю: возможно пойдет дождь. То для меня есть возможный мир пойдет дождь.

При этом есть текущий мир, который играет роль модели в классической логике. И от его выбора истинность модальных высказываний меняется.

(Reply to this) (Parent) (Thread)

интересно, а сколько есть модальностей не сводимых к друг к другу?
и как "существование" соотносится с модальностями?
например,
существование
X есть-is-exists
отрицание
X нет-is not-doesn't exist
модальности
X is necessary
отрицание
X is not necessary-unnecessary что семантически похоже на то что X is possible, если он не обязателен, то по крайней мере возможен
далее
X is possible
отрицание
X is not possible-impossible что семантически означает что X невозможен ни в одном из миров, и это как раз похоже на противоположность X is necessary
получается есть 3 модальности и 2 состояния существования - necessary,unnecessary=possible,impossible и is, is not.

потом
если X is, то X может быть necessary, и может быть possible, но не может быть impossible раз он есть (ну и не может быть is понятное дело)
если X is not, то X может быть possible, то есть где то вероятно появиться, может быть impossible, так как его вообще может нигде не быть, но он не может быть necessary, ведь если бы он был necessary, то он бы автоматом существовал.
если X necessary, то он is, он possible, но не может быть is not и не может быть impossible
если X possible/unnecessary, то он может is, может is not, но не может быть impossible, а вот может или не может он быть necessary - хз, мне интуитивно кажется что следствия тут нет.
если X impossible, то он может быть is not, но не может быть is, necessary и possible

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

еще можно подумать можно ли к модальности possible припихнуть и определить more likely/less likely.

(Reply to this) (Parent) (Thread)

второй параграф можно наверное графически изобразить как схему

(Reply to this) (Parent)

https://plato.stanford.edu/entries/formal-epistemology/

(Reply to this) (Parent)

Мне кажется вы правильно рассуждаете.

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

(Reply to this) (Parent)