Wiki. “内蕴语言” [内蕴语言]

任何意象 $\mathcal E$ 都带有一种内蕴语言 (internal language). 直观地说, 使用这种语言, 我们可以假装 $\mathcal E$ 的对象是集合, 态射是集合的映射, 并且像对待集合一样对 $\mathcal E$ 的命题进行推理. 例如, 满态射 (epimorphism) $\alpha\colon X\to Y$ 的概念可使用内蕴语言表达为 $$ \mathcal E \models \forall y:Y. \exists x:X . \alpha(x)=y. $$ 其中 $X,Y$ 是 $\mathcal E$ 的对象. 对于集合, 满射的复合是满射; 那么在抽象的意象中我们也有满态射的复合是满态射.

有一条元定理 (metatheorem) 是说, 若语句 $\varphi$ 在意象 $\mathcal E$ 的内蕴语言中成立, 且逻辑上 $\varphi$ 推出 $\psi$, 则 $\psi$ 也在这一内蕴语言中成立.

需要注意的是, 意象的内蕴语言通常是直觉主义 (intuitionistic), 而非经典 (classical) 的. 这意味着不能使用排中律, 且一个命题 $P$ 的否定之否定不能推出 $P$ 本身.

应用

概形上的层语义

概形上的层意象的层语义简化了代数几何中的许多概念和命题.

物理

一个量子力学系统可赋予一个 Bohr 意象.

其他

另见 Newton–Puiseux 定理