module Интуиционистское_Исчисление_Высказываний where

{- Часть 1 | Интуиционистское исчиcление высказываний -}

open import Вспомогательные_определения

{-
Сначала определим логическую часть - позитивный фрагмент
интуиционистского исчисления высказываний.
-}

{-
Φ набирается как \GF или \Phi
Чтобы узнать как набрать символ, наведите
на него курсор и M-x describe-char
-}

{-
Определение 1.1. Множество формул Φ задается индуктивно.
                 Пусть V - некоторое бесконечное множество переменных
                 (в нашем случае множество строк String). Тогда
                 ∙ всякая переменная является формулой
                 ∙ если φ, ψ - формулы, то φ ⊃ ψ - формула.
-}

infixr  _⊃_

data Φ : Множество where
  ппер : Строка → Φ
  _⊃_ : Φ → Φ → Φ

{- Определение 1.2. Контекст (обозн. Γ) - Список формул -}

Контекст = Список Φ

{-
Определение 1.3. Доказательство (формулы φ в контексте Γ) в ИИВ -
                 дерево вывода, где
                 ∙ Корень - Γ ⊢ φ - то, что доказывается
                 ∙ Лист - аксиома
                 ∙ Каждый узел связан с родительским по правилу вывода
-}

{- Определение 1.4. Отношение выводимости ‌⊢ ⊆ L(Φ) × Φ
                    задается индуктивно правилами вывода. -}

{-
===================================
ПРАВИЛА ВЫВОДА ПФ ИИВ

1) Группа аксиом:

-------- (Ax)
φ, Γ ⊢ φ

2) Логическая группа:

φ, Γ ⊢ ψ
--------- (⊃I)
Γ ⊢ φ ⊃ ψ

Γ ⊢ φ ⊃ ψ     Γ ⊢ φ
------------------- (⊃E)
Γ ⊢ ψ

3) Структурная группа:

Γ ⊢ φ
--------(Ослабление)
ψ, Γ ⊢ φ

Δ, φ, ψ, Γ ⊢ σ
--------------(Обмен)
Δ, ψ, φ, Γ ⊢ σ
===================================
-}

{-
Комментарий.

Аксиома - Аксиома. Мы можем делать предположения. Не требует предусловий.

⊃В - Введение импликации (alias теорема Эрбрана,
     теорема о Дедукции). В нашей системе, в отличие от Гильбертовской,
     мы берем ее без доказательства

⊃У - Удаление импликации (alias Modus Ponens).
     Широко известное правило отделения.
-}

infix  _⊢_
data _⊢_ : Контекст → Φ → Множество where

  Аксиома : ∀ {Γ φ} →
  
    ---------
    φ ∷ Γ ⊢ φ
    
  ⊃В : ∀ {Γ φ ψ} →
  
    φ ∷ Γ ⊢ ψ →
    -------------
    Γ ⊢ φ ⊃ ψ
    
  ⊃У : ∀ {Γ φ ψ} →
  
    Γ ⊢ φ ⊃ ψ →      Γ ⊢ φ →
    ------------------------
               Γ ⊢ ψ

postulate
  Ослабление : ∀ {Γ φ ψ} → Γ ⊢ φ → ψ ∷ Γ ⊢ φ
  Обмен : ∀ {n Γ φ} → Γ ⊢ φ → обмен n Γ ⊢ φ

{- В качестве примера докажем φ ⊃ φ, А также певвые две аксиомы Гильберта -}

private
  Пример1 : ∀ {φ} → [] ⊢ φ ⊃ φ
  Пример1 {φ} = ⊃В Аксиома

  Пример2 : ∀{φ ψ} → [] ⊢ φ ⊃ (ψ ⊃ φ)
  Пример2 {φ} {ψ} = ⊃В (⊃В (Ослабление Аксиома))

  Пример3 : ∀{φ ψ ν} → [] ⊢ (φ ⊃ (ψ ⊃ ν)) ⊃ (φ ⊃ ψ) ⊃ (φ ⊃ ν)
  Пример3 {φ} {ψ} {ν} =
    ⊃В (⊃В (⊃В (⊃У {Γ}{ψ}{ν} (⊃У{Γ}{φ}{ψ ⊃ ν}(Обмен {} {Γ}
    (Ослабление (Ослабление Аксиома))) Аксиома)
    (⊃У (Ослабление Аксиома) Аксиома))))
    where Γ = φ ∷ (φ ⊃ ψ) ∷ (φ ⊃ (ψ ⊃ ν)) ∷ []