Upgrade to Pro
— share decks privately, control downloads, hide ads and more …
Speaker Deck
Features
Speaker Deck
PRO
Sign in
Sign up for free
Search
Search
Coqの公理
Search
Masaki Hara
April 23, 2016
Science
0
310
Coqの公理
Coqの公理について
Masaki Hara
April 23, 2016
Tweet
Share
More Decks by Masaki Hara
See All by Masaki Hara
Getting along with YAML comments with Psych
qnighy
1
67
状態設計から「なんとなく」を無くそう
qnighy
84
27k
日付時刻A to Z
qnighy
1
490
Hands-on Native ESM @ JSConf JP 2022
qnighy
0
5.4k
computed_modelの紹介 / Introducing computed_model (2)
qnighy
0
550
computed_modelの紹介 / Introducing computed_model
qnighy
0
340
Rust: imperative language 2.0
qnighy
10
2.3k
Making an opinionated Web framework
qnighy
2
4.3k
BigQueryでprotobufをパースした話 / parsing protobuf in BigQuery
qnighy
1
2.2k
Other Decks in Science
See All in Science
Ph.D. defense "Convex Manifold Approximation for Tensors"
gkazunii
0
200
PRML Chapter 1 (1.3-1.6)
snkmr
1
100
O ChatGPT e outras IAs vão mudar toda a pesquisa científica
cardososampaio
0
180
Pandas 2 vs Polars vs Dask (PyDataGlobal 2023 December)
ianozsvald
0
490
AI(人工知能)の過去・現在・未来 —AIは人間を超えるのか—
tagtag
0
120
遺伝子発現プロファイルに基づく新しい薬物間相互作用予測法
tagtag
0
110
Machine Learning for Materials (Lecture 2)
aronwalsh
0
600
ultraArmをモニター提供してもらった話
miura55
0
120
データで課題を解決する -因果関係を調べる統計的因果推論-
sshimizu2006
4
1.4k
Machine Learning for Materials (Lecture 9)
aronwalsh
0
120
最新のAI技術を使った材料シミュレーションで材料研究現場に変革を
matlantis
0
510
20分で分かる Human-in-the-Loop 機械学習におけるアノテーションとヒューマンコンピューターインタラクションの真髄
hurutoriya
3
930
Featured
See All Featured
Fireside Chat
paigeccino
22
2.7k
How GitHub Uses GitHub to Build GitHub
holman
468
290k
Happy Clients
brianwarren
92
6.4k
4 Signs Your Business is Dying
shpigford
176
21k
Designing for humans not robots
tammielis
247
25k
Responsive Adventures: Dirty Tricks From The Dark Corners of Front-End
smashingmag
245
20k
The Cost Of JavaScript in 2023
addyosmani
21
4k
Debugging Ruby Performance
tmm1
70
11k
Robots, Beer and Maslow
schacon
PRO
155
8k
Code Reviewing Like a Champion
maltzj
515
39k
Creating an realtime collaboration tool: Agile Flush - .NET Oxford
marcduiker
14
1.5k
The Art of Programming - Codeland 2020
erikaheidi
43
12k
Transcript
Coqの公理 Masaki Hara (qnighy) 2016/04/23
型システムと公理系 Coqの型システム (CIC/pCIC) 強正規化性により 正当化 Coqの公理系 集合モデルにより 正当化 HoTTの公理系 ∞-亜群モデルにより
正当化 両立しない
Coqの公理 同一性 2つの値の同一性を 保証する。 構成 何らかの値の存在を 保証する。 古典論理 選択 記述
真偽に基づく 2択の提供 存在するものを 集める Coqの項として 書ける
同一性の公理 関数の外延性 各点で等しい関数は等しい FunctionalExtensionality.functional_extensionality 命題の外延性 同値な命題は等しい 対応する公理なし Coq.Sets.Ensembles.Extensionality_Ensembles の帰結 証明非依存性
証明は区別できない ProofIrrelevance.proof_irreleavance JM同値性 集合間の同値性はただ1つ JMeq.JMeq_eq
値の強さ ∀, ∃, , ∀, ∃! , , ∀, ,
∀, , ∃, ∀, , 各点での存在のみ。 各点での一意存在。 一様に存在。 具体的な項。 具体的な項。
一意選択 ∀, ∃, , ∀, ∃! , , ∀, ,
∀, , ∃, ∀, , 各点での存在のみ。 各点での一意存在。 一様に存在。 具体的な項。 具体的な項。 一意選択 各点で一意存在するなら一様に存在 ClassicalUniqueChoice.unique_choice
選択 ∀, ∃, , ∀, ∃! , , ∀, ,
∀, , ∃, ∀, , 各点での存在のみ。 各点での一意存在。 一様に存在。 具体的な項。 具体的な項。 選択 各点で存在するなら一様に存在 ClassicalChoice.choice
関係選択 ∀, ∃, , ∀, ∃! , , ∀, ,
∀, , ∃, ∀, , 各点での存在のみ。 各点での一意存在。 一様に存在。 具体的な項。 具体的な項。 関係選択 各点での存在を一意存在に絞れる RelationalChoice.relational_choice
記述 ∀, ∃, , ∀, ∃! , , ∀, ,
∀, , ∃, ∀, , 各点での存在のみ。 各点での一意存在。 一様に存在。 具体的な項。 具体的な項。 記述 各点での一意存在を具体的な項に Description.constructive_definite_description
不定記述 ∀, ∃, , ∀, ∃! , , ∀, ,
∀, , ∃, ∀, , 各点での存在のみ。 各点での一意存在。 一様に存在。 具体的な項。 具体的な項。 不定記述 各点での存在を具体的な項に IndefiniteDescription.constructive_indefinite_description
古典論理 古典論理 命題の真偽で場合分けする証明 Classical.classic 情報つき排中律 命題の真偽で場合分けする構成 対応する公理なし ClassicalDescription.excluded_middle_informative
非古典論理のもとでの不定記述 不定記述 各点での存在を具体的な項に IndefiniteDescription.constructive_indefinite_description ヒルベルトの 「酒場のパラドックス」型不定記述 Epsilon.epsilon_statement 非古典論理では不定記述より強い