Похожие чаты

Есть ли примеры теорий, которые не могут быть финитно аксиоматизированы

в одном языке, но при этом есть их полная и непротиворечивая финитная аксиоматизация в другом, более богатом языке? Например, логика какого-нибудь класса шкал Крипке, которая конечно не аксиоматизируема в базовом модальном языке, но если его расширить с помощью универсальной модальности, то логику этого же класса шкал можно финитно аксиоматизировать? Если это невозможно, то есть ли у этого какое-то формальное доказательство? Есть кочующий из книги в книгу принцип "чем богаче язык, тем все хуже с аксиоматизируемостью/разрешимостью/сложностью", но я нигде не встречал формального доказательства этого принципа

10 ответов

6 просмотров

Второпорядковая формализация теории множеств не требует схем аксиом

Стикер

пільнуй-сабаку Автор вопроса

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

пільнуй сабаку
да, но если я хочу аксиоматически описать какие-то...

Вместо того чтобы брать первопорядковую логику, а потом расширять её равенством, сразу берите первопорядковую логику с равенством! 🤣

йо привет! если я правильно понял вопрос, то вроде нет (для модальных логик по крайней мере). часто отсутствие финитной и рекурсивной аксиоматизаций показывается редукцией от сигма^1_1 проблемы типа тайлинга с особой тайл, которая появляется бесконечно много в первом ряду. если в языке L1 мы делаем такую редукцию, т.е. находим формулу которая сатисфайбл ифф можно покрыть пространство с данными тайлами, то в более экспрессивном языке L2 будет эквивалентная формула

пільнуй-сабаку Автор вопроса
Rust Skye
йо привет! если я правильно понял вопрос, то вроде...

спасибо! А можешь мб назвать какую-нибудь статью, где это доказательство через редукцию к сигма^1_1 проделано? Хочу в детали вчитаться, был бы очень благодарен)

пільнуй сабаку
спасибо! А можешь мб назвать какую-нибудь статью, ...

ты как с эпистемной логикой? есть моя статья, я могу там в деталях подсказать

пільнуй сабаку
Самое то

https://rgalimullin.gitlab.io/TARK23/main.pdf

пільнуй сабаку
Самое то

https://rgalimullin.gitlab.io/TARK23/tarkpresshort.pdf

Похожие вопросы

Обсуждают сегодня

30500 за редактор? )
Владимир
47
any reference of this implementation?
BitBuddha
29
Ⓐrtto, [4/23/24 7:02 PM] Please explain more fully how it is not working exactly, and what are the steps you are taking, and what error messages come or what happens. Ⓐrtto, ...
Ezza Kezza
2
sounds like people have lost their kaspa on tradeogre... does this mean tradeogre not trustworthy?
Ezza Kezza
15
Страшнейшая правда про списки ЦБ. С первых дней жизни P2P сферы, молодые человеки, начитавшись законодательной базы и "внутренних" документов, решили, что им противостоит сер...
Foxcool
3
Недавно Google Project Zero нашёл багу в SQLite с помощью LLM, о чём достаточно было шумно в определённых интернетах, которые сопровождались рассказами, что скоро всех "ибешни...
Alex Sherbakov
5
So much speculation in the last week. So much volatility in price. This is because Hedera has a GC that isn't using the network it's governing. Why aren't people asking why a...
Summit Seeker R
9
Anyone else having this error when trying to make transactions?
Datzel
11
Question: How viable is it to use Anvil as the backend infrastructure for managing a TradFi portfolio, while integrating Flexa for instant liquidity and payment solutions? Cou...
Kevin
2
вы делали что-то подобное и как? может есть либы готовые? увидел картинку нокода, где всё линиями соединено и стало интересно попробовать то же в ddl на lua сделать. решил с ч...
Victor
8
Карта сайта