A2.agda

module A2 where

------------------------------------------------------
-- 述語論理
 
-- まずは命題論理から
 
-- 真(⊤)，偽(⊥)の定義が必要
-- ⊥ は証明がひとつもないような命題だから, 空集合によって表す
-- 帰納的定義によって次のように表現することができる
 
data ⊥ : Set where
-- record 型は指定された値の型を1組にまとめたもの
-- つまり何も指定しなければ全体の集合すなわち ⊤ が表現できる

record ⊤ : Set where

-- 結合子を構成していく
-- 連言(AかつB)
record _∧_ (P Q : Set) : Set where
  field
    Elim1 : P
    Elim2 : Q

test1 : (P Q : Set) → Set
test1 p q = p ∧ {!!}

test2 : (P : Set) → Set
test2 p = p ∧ ⊥

-- 除去規則 P ∧ Q → P は　_∧_.Elim1 のようにかける
 
lemma1 : (P Q : Set) → P ∧ Q → P
lemma1 p q = _∧_.Elim1
 
-- 導入規則
∧Intro : {P Q : Set} → P → Q → P ∧ Q
∧Intro p q = record { Elim1 = p ; Elim2 = q }
 
-- 選言
data _∨_ (P Q : Set) : Set where
  ∨Intro1 : P → P ∨ Q
  ∨Intro2 : Q → P ∨ Q
 
∨Elim : {P Q R : Set} → P ∨ Q  →  (P → R) → (Q → R) → R
∨Elim (∨Intro1 a) prfP _ = prfP a
∨Elim (∨Intro2 b) _ prfQ = prfQ b
 
test3 : (P Q : Set) → Set
test3 p q = p ∨ q
 
lemma2 : (P Q : Set) → P → P ∨ Q
lemma2 p q = ∨Intro1
 
-- 含意 (PならばQ)
data _⊃_ (P Q : Set) : Set where
  ⊃Intro : (P → Q) → P ⊃ Q
 
-- ⊥Elim : 偽の除去規則
-- 存在のしない値は()としてmatchする
⊥Elim : {P : Set} → ⊥ → P
⊥Elim ()
 
-- ⊃Elim : 導入の除去規則
-- P ⊃ Q 型から P → Q 型の値への写像が存在する
⊃Elim : {P Q : Set} → P ⊃ Q → P → Q
⊃Elim (⊃Intro x) q = x q
 
-- 否定
-- 否定は p → ⊥ すなわち p ⊃ ⊥ として表現される
¬ : Set → Set
¬ p = p ⊃ ⊥

 
-- 命題1
-- prop1 : ((A ∧ B) → (A ∨ B)) 
-- A ∧ B が与えられたら，A から A ∨ B が作れる

prop1 : (A B : Set) → (A ∧ B) ⊃ (A ∨ B)
prop1 A B = {!!}

-- A ∧ B -> A
-- A -> A ∨ B ∨Intro1
-- (A -> B)


--prop1 : (A B : Set) → (A ∧ B) ⊃ (A ∨ B)
--prop1 A B = ⊃Intro (λ x → ∨Intro1 (_∧_.Elim1 x))
 

 
-- 述語論理へ
-- all,existを定義
-- 全称
-- この型の値が存在する -> allが書ける
data all (P : Set) (Q : P → Set) : Set where
  ∀Intro : ((a : P) → Q a) → all P Q
  
∀Elim : {P : Set} → {Q : P → Set} → all P Q → (a : P) → Q a
∀Elim (∀Intro f) a = f a
 
-- 存在
-- recordとdataは双対のような存在になっている
-- 指定された値の型を1組にまとめたもの
record exist (P : Set) (Q : P → Set) : Set where
  field
    evidence : P
    Elim : Q evidence
 
∃Intro : {P : Set} → {Q : P → Set} → (a : P) → Q a → exist P Q
∃Intro a p = record { evidence = a ; Elim = p }
 
-- prop3 : ∃x (∀y (P x y)) → (∀y (∃x P (x y))) 
prop3 : (A B : Set) → (P : A → (B → Set)) →
           exist A ((λ x → all B (λ y → P x y))) ⊃ (all B (λ y → exist A (λ x → P x y)))
prop3 A B p = ⊃Intro ( λ (pr : exist A (λ (x : A)
          → all B ( λ (y : B) → p x y))) → ∀Intro (λ (b : B) →
                record { evidence = exist.evidence pr ; Elim = ∀Elim (exist.Elim pr) b }))
 
-- 二重否定除去(DNE)
-- DNE : (P : Set) → ¬ (¬ P) ⊃ P

--または排中律(LEM)
-- LEM : (P : Set) → (P ∨ ¬ P)
--を与える．

-- つまり，not not A が A の世界
-- Agdaは直観論理(マーティン・レーフの直観主義的型理論(ML-ITT))
-- に基づいて構成されているので，二重否定除去律は公理ではない．
-- ¬¬ P →  P は示せない！
-- (¬¬¬ P → ¬ P は示せる)

-- postulate(仮定)により拡張してやる
 
-- postulate DNE : {P : Set} → ¬ (¬ P) ⊃ P
postulate LEM : (P : Set) → (P ∨ ¬ P)

-- この二つは同じ拡張をしているので，一方からもう一方を導き出せる
DNE : (P : Set) → ¬ (¬ P) ⊃ P
DNE p = ⊃Intro (λ x → ∨Elim (LEM p) (λ y → y) (λ z → ⊥Elim (⊃Elim x z)))