全文走过的路，可以按“用了什么前文”串成一条线：

1. 自然语言在结构、完备、量词、自指、可检查性上的五个弊端（ [例] 结构歧义 至 [例] 贝里悖论 ），引出对象语言与元语言的分层（ [定义] 对象语言与元语言 ）。
2. 用“满足封闭条件的最小集合”定义项（ [定义] 项的集合 ），“最小”直接给出结构归纳（ [定理] 结构归纳原理（structural induction） ）。
3. 用同样的“最小”定义求值关系（ [定义] 一步归约 ），得到对推导归纳（ [定理] 对推导归纳 ），再证明确定性（ [定理] 确定性 ）。
4. 用推导规则定义类型（ [定义] 类型与类型判断 ）。语法导向给出反演（ [引理] 反演 ），反演给出类型唯一和典范形式。
5. 进展与保型合起来得到类型安全（ [推论] 类型安全 ）。
6. 证明检查器相对规则可靠且完备，把“检查器接受”与“运行不受阻”接上（ [推论] 检查器接受的程序不会受阻 ）。

贯穿始终的方法只有一个：先把东西定义成满足某些规则的最小对象，再沿着这些规则归纳。语言变大以后，规则会变多，证明会变长，但这个方法不变。它在数学和逻辑史上的来历，见 [注记] “最小 + 归纳”的历史 。