Семинар 3. Интуиционистская логика и некоторые конструктивные логики на её основе

Математический конструктивизм впервые возник в связи с кризисом оснований математики в начале XX века. Хотя изначально задача конструктивистов сводилась к устранению парадоксов «наивной теории множеств», дальнейшее развитие подход конструктивистов получил в рамках интуиционистской математики, которую возглавил Л.Э.Я. Брауэр. Сторонники Брауэра считали, что источником возникновения различных трудностей в теории множеств служит уподобление бесконечных множеств конечным и необоснованный перенос законов классической логики, верных для конечных множеств, на бесконечные.
Доклад мы начнём с описания интуиционистского подхода в рамках неформальной семантики Брауэра–Гейтинга–Колмогорова для «логики исчисления задач», из которой далее получим уже формальную семантику реализуемости для интуиционистской арифметики. Затем, отталкиваясь от требования большей релевантности классической импликации, мы построим семантику возможных миров, иначе — семантику типа Крипке, в рамках которой парадоксы материальной импликации уже не будут иметь места. Наконец, обсуждая проблему интуиционистского отрицания, мы придём к понятию сильного отрицания $\sim$ и конструктивным логикам Нельсона, в которых $\sim \Phi$ на семантическом уровне будет означать существование контрпримера к $\Phi$.