Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Category:

Логика высказываний, минимальная аксиоматизация

Я тут почитал статью в википедии про логику высказываний и обнаружил, что там не приведена усовершенствованная (Девидом Мередитом) аксиоматизация Лукасевича! Что-ж, как-нибудь напишу её туда. А пока сюда.

Итак, язык логики высказываний состоит из
– константы ⊥ (“ложное высказывание”),
– связки => (“следовательно”),
– неограниченного алфавита переменных.

Связки “и”, “или” и “не” можно определить через то, что уже есть:
– “не A” это “A => ⊥”,
– “А или B” это “(A => ⊥) => B”,
– “А и B” это “(A => (B => ⊥)) => ⊥”.

Правил вывода два:
– Замена: можно заменить любую букву любой другой)
– Modus ponens: из P и P => Q выводится Q.

Аксиом четыре:
1) (P => (Q => R)) => ((P => Q) => (P => R)),
2) P => (Q => P),         # Verum ex quodlibet
3) ⊥ => P,                # Ex falso quodlibet
4) ((P => ⊥) => P) => P.  # Tertium non datur

Первые две аксиомы дают т.н. минимальную логику.
Добавление третьей аксиомы конструктивистскую логику.
Добавление четвёртой аксиомы даёт классическую логику.

Если добавить ещё четыре правила (конструкция и редукция ∀ и ∃), соответственно получится логика предикатов: классическая, конструктивистская или минимальная, солить по вкусу, помешивать.

Удобнство этой аксиоматизации проявляется в том, что совершенно прямолинейно устроен изоморфизм Карри-Говарда:
– минимальная/конструктивистская логика высказываний соответствует просто-типизированному лямбда-исчислению (без или с нулевым типом соответственно).
– минимальная/конструктивистская логика предикатов соответствует минимальной/конструктивной зависимой теории типов.
– классические логики соответствуют соответствующим штукам, в которые добавлен оператор call/cc, реализующий аксиому Tertium non datur.

* * *

А теперь вопрос к уважаемой публике. Я когда-то слышал, что зависимо-типизированный вариант call/cc реализует аксиому выбора (которая, как известно, является обобщением закона исключённого третьего). Кто-нибудь знает, какой-такой зависимо-типизированный вариант и как именно реализует? Я сегодня два часа голову ломал и не понял.

Upd: ОК, теперь понятно. В ITT (конструктивной теории типов Пер Мартин-Лёфа) аксиома выбора в слабом смысле верна априори. Слабый смысл это вот что: если у нас есть конструктивное доказательство, что функция сюрьективна, у нас есть и сечение. Если у нас есть “неконструктивное доказательство сюрьективности” (т.е. доказательство, что функция не несюрьективна), то конечно ничего подобного нет, однако стоит добавить в исчисление call/cc и у нас снова наличествует аксиома выбора в сильном смысле*, правда теория становится сильнее классической логики, что страшновато. Можно ослабить одно правило редукции, тогда вместо полной аксиомы выбора останется только зависимая, зато теория снова будет совместима с классической логикой. Большое спасибо deni_ok за ссылку которая оказалась прямо в точку!

______
* Аксиома выбора в сильном смысле гласит, что для любого непустого типа А и функции f: A => B найдётся g: B => A такое что fgf = f. В отличие от слабого смысла, сильный смысл имплицирует исключённое третье. Любой топос, где верна сильная формулировка аксиомы выбора, two-valued.
Subscribe

  • Towards Univalent Construction Calculus

    Modern constructive Martin-Löf Type Theories (MLTTs) are exceptionally expressive and convenient languages for mathematical reasoning. By “modern”…

  • (no subject)

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

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 8 comments