具现

具现 (或称具现解释) 是一类研究直觉主义逻辑的方法, 它给出了 “证明” 的形式化定义, 并称之为具现子. 若具现子 $x$ 对应的命题 $A$ 的证明, 那么称 $x$ 具现了 $A$ .

具现可以视为一种 Brouwer–Heyting–Kolmogorov 解释的形式化定义, 后者抽象地使用 “证明” 这一概念来定义了构造主义逻辑, 而具现考虑证明的具体表示. 也可以粗略地将两者视为同一概念, 因为二者对逻辑连接词的理解是一致的.

Kleene 研究的具现以自然数作为具现子, 用 Kleene 第一代数编码函数, 这也是最早的关于具现的研究. 而 Kreisel 使用有类型的 $λ$ 演算作为具现子.

1例子

(...)

•	具现意象是一种以具现为内逻辑的意象, 有效意象是其特殊情况.

术语翻译

具现 • 英文 realizability

具现子 • 英文 realizer