An Introduction to Smooth Infinitesimal Analysis

魔法少女と次のような会話を交わし, 参考文献を教わってきた.

つどい, 一人で複数個発表してもいいの 

@functional_yy 集合論とロジックで制圧説 

@phasetr 楽園 

@functional_yy 超準解析と物理学で殴られる 

@phasetr 直観主義者として smooth infinitesimal analysis を推してゆきたい 

@functional_yy 参考文献教えてください 

@phasetr http://www.math.cornell.edu/~oconnor/sia.pdf 

@functional_yy ありがとうございます. あとで読みます

というわけで参考文献を読んでみた.

Axiom 1. 略
Furthermore, we have that \(\forall x ((x \neq 0) \Longrightarrow (\exists y xy=1))\), but I don't want to call \(R\) a field for a reason I'll discuss in a moment.

\(R\) を体と言わない (そもそも \(F\) とか \(K\) と書かない) らしい. 行方を注視しよう.

Axiom 2. 略
but I don't want to call \(<\) total, for a reason I'll discuss in a moment.

無限小とか出てくると色々アレなのだろう, という話なのだろうが, 割と戦慄する.
Axiom 4. がやばい. 初見, 意味が分からなかったがその後の説明を読んで戦慄. 興味がある向きは実際に P.2 をご覧頂きたい. 無論, 直観主義の話であって, 排中律が使えない (採用しない) というその辺の話だ.

Fact.
There is a form of set theory (called a local set theory, or topos logic) which has its underlying logic restricted (to a logic called intuitionistic logic) under which Axioms 1 through 4 (and also the axioms to be presented later in this paper) taken together are consistent.

topos logic, 名前だけで修羅っぽい.

2 節ラストで Axiom 1, 2 での注意も明かされる. 引用が面倒なので各自確認されたい.
Proposition 1. は全ての \(f \in R^R\) で成り立つの. やばいのでは.

Proposition 3. の curve というの, 何を言っているの. 「連続関数」とかいうのは入っているの. ただの関数と思っていいのこれ. Straight の意味が分からない. P.5 で積分が出てくるが, これ定義何なの.

\(D\) が抽象的にしか与えられていないが, これ, そもそも具体的に書けるのだろうか.

参考文献, Sheaves in geometry and logic とかある.

何かよく分からないがやばそうだということだけ把握し, 一旦撤退する. 微分幾何やりたい. あと超準解析と物理学読みたい.