Skip to content

Instantly share code, notes, and snippets.

@kdxu

kdxu/A2.agda

Created Mar 28, 2015
Embed
What would you like to do?
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)))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.