Created
March 28, 2015 02:07
-
-
Save kdxu/3ecf21603abe9e9a409e to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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