diff --git a/10.md b/10.md
index d7103459fc1477fe57110e9f54a111250b453fb0..f05f1bf6aee8540e15970682b93974c98f59c2ed 100644
--- a/10.md
+++ b/10.md
@@ -215,11 +215,11 @@ False
 
 我们将借此机会重新表述前面的命题逻辑的语法规则，并添加量词的形式化规则；所有这些一起组成一阶逻辑的句法。此外，我们会明确相关表达式的类型。我们将采取约定：`<e^n, t>`，一种由`n`个类型为`e`的参数组成产生一个类型为`t`的表达式的谓词的类型。在这种情况下，我们说`n`是谓词的元数。
 
- > 1.  If P is a predicate of type 〈e&lt;sup&gt;n&lt;/sup&gt;, t〉, and α[1], ... α&lt;sub&gt;n&lt;/sub&gt; are terms of type e, then P(α[1], ... α&lt;sub&gt;n&lt;/sub&gt;) is of type t.
-> 2.  If α and β are both of type e, then (α = β) and (α != β) are of type t.
-> 3.  If φ is of type t, then so is `-`φ.
-> 4.  If φ and ψ are of type t, then so are (φ `&` ψ), (φ `|` ψ), (φ `->` ψ) and (φ `<->` ψ).
-> 5.  If φ is of type t, and x is a variable of type e, then `exists x.`φ and `all x.`φ are of type t. 
+ > 1.  如果`P`是`<e[n], t>`类型的谓词，并且`α[1]，..., α[n]`是`e`类型的项，则`P(α[1], ..., α[n])`的类型为`t`。
+> 2.  如果`α`和`β`均为`e`类型，则（`α = β`）和（`α != β`）均为`t`类型。
+> 3.  如果`φ`是·类型，则`-φ`也是。
+> 4.  如果`φ`和`ψ`为`t`类型，那么`(φ & ψ), (φ | ψ), (φ -> ψ), (φ <-> ψ)`也是如此。
+> 5.  如果`φ`是`t`类型，而`x`是`e`类型变量，则存在`x.φ`，而所有`x.φ`都是`t`类型。
 
 3.1 总结了`logic`模块的新的逻辑常量，以及`Expression`模块的两个方法。
 
diff --git a/8.md b/8.md
index 12cd25388665a1131cf0bff78ff4b392f7354f41..417378d250f14c214b090fa3c76a85e37a53c0ae 100644
--- a/8.md
+++ b/8.md
@@ -465,7 +465,7 @@ grammar = nltk.PCFG.fromstring("""
 *   句子都有内部组织结构，可以用一棵树表示。组成结构的显著特点是：递归、中心词、补语和修饰语。
 *   语法是一个潜在的无限的句子集合的一个紧凑的特性；我们说，一棵树是符合语法规则的或语法树授权一棵树。
 *   语法是用于描述一个给定的短语是否可以被分配一个特定的成分或依赖结构的一种形式化模型。
-*   给定一组句法类别，上下文无关文法使用一组生产式表示某类型 *A* 的短语如何能够被分析成较小的序列α[1] ... α&lt;sub&gt;n&lt;/sub&gt;。
+*   给定一组句法类别，上下文无关文法使用一组生产式表示某类型 *A* 的短语如何能够被分析成较小的序列`α[1] ... α[n]`。
 *   依存语法使用产生式指定给定的中心词的依赖是什么。
 *   一个句子有一个以上的句法分析就产生句法歧义（如介词短语附着歧义）。
 *   分析器是一个过程，为符合语法规则的句子寻找一个或多个相应的树。