diff --git a/template.typ b/template.typ
index 8b22761..33c2baa 100644
--- a/template.typ
+++ b/template.typ
@@ -4,6 +4,7 @@
 
 #import "@preview/lemmify:0.1.6": *
 #import "@preview/commute:0.2.0": node, arr, commutative-diagram
+#import "@preview/showybox:2.0.3": showybox
 
 #let __print_commute = true
 #let old-commutative-diagram = commutative-diagram
@@ -276,16 +277,104 @@
     name
 }
 }
+
+
+#let frame-map = (
+  Proposition: (
+    border-color: blue,
+    title-color: blue.lighten(30%),
+    body-color: blue.lighten(95%),
+    footer-color: blue.lighten(80%)
+  ),
+  Theorem: (
+    title-color: green.darken(40%),
+    body-color: green.lighten(80%),
+    footer-color: green.lighten(60%),
+    border-color: green.darken(60%),
+  ),
+  Lemma: (
+    title-color: orange.darken(40%),
+    body-color: orange.lighten(80%),
+    footer-color: orange.lighten(60%),
+    border-color: orange.darken(60%),
+  ),
+  Corollary: (
+    title-color: red.darken(40%),
+    body-color: red.lighten(80%),
+    footer-color: red.lighten(60%),
+    border-color: red.darken(60%),
+  ),
+  Definition: (
+    title-color: purple.darken(40%),
+    body-color: purple.lighten(80%),
+    footer-color: purple.lighten(60%),
+    border-color: purple.darken(60%),
+  ),
+  Example: (
+    border-color: red.darken(40%),
+    title-color: red.darken(30%),
+    body-color: red.lighten(90%),
+    radius: 0pt,
+    thickness: 2pt,
+    body-inset: 1em,
+  ),
+  Remark: (
+    border-color: green.darken(40%),
+    title-color: green.darken(30%),
+    body-color: green.lighten(90%),
+    radius: 0pt,
+    thickness: 2pt,
+    body-inset: 1em,
+  ),
+  Algorithm: (
+    border-color: blue.darken(40%),
+    title-color: blue.darken(30%),
+    body-color: blue.lighten(90%),
+    radius: 0pt,
+    thickness: 2pt,
+    body-inset: 1em,
+  ),
+)
+
+#let theorem-like-style(thm-type, name, number, body) = {
+  showybox(
+    body,
+    title: [#strong(thm-type) #number #if name != none [ (#name) ]],
+    frame: frame-map.at(thm-type)
+  )
+}
+
+#let proof-style(thm-type, name, number, body) = {
+  showybox(
+    breakable: true,
+    title: "Proof",
+    frame: (
+    border-color: red.darken(30%),
+    title-color: red.darken(30%),
+    body-color: red.lighten(90%),
+    radius: 0pt,
+    thickness: 2pt,
+    body-inset: 1em,
+    dash: "densely-dash-dotted"
+  ),
+  )[
+    #body
+    #linebreak()
+    #h(1fr)
+    #box(scale(100%, origin: bottom + right, sym.square.stroked))
+  ]
+}
+
 #let (
   theorem: theo, lemma: lem, corollary: cor,
   remark: rem, proposition: prop, example:ex , definition:def,
   proof: pr, rules: thm-rules
-) = default-theorems("thm-group", lang: "en")
+) = default-theorems("thm-group", lang: "en", thm-styling: theorem-like-style, proof-styling: proof-style)
 #let (
   theorem: theo1, lemma: lem1, corollary: cor1,
   remark: rem1, proposition: prop1, example:ex1 , definition:def1,
   proof: pr1, rules: thm-rules1
-) = default-theorems("thm-group-linear", lang: "en", thm-numbering: thm-numbering-linear)
+) = default-theorems("thm-group-linear", lang: "en", thm-numbering: thm-numbering-linear, thm-styling: theorem-like-style, proof-styling: proof-style)
 #let my-ans-style(
   thm-type, name, number, body
 ) = block(spacing: 11.5pt, {
@@ -305,8 +394,8 @@
   #body
   #parbreak()
   ]
-#let (alg, rules: alg-rules) = new-theorems("thm-group", ("alg": text[Algorithm]))
-#let (alg1, rules: alg-rules1) = new-theorems("thm-group-linear", ("alg1": text[Algorithm]), thm-numbering: thm-numbering-linear)
+#let (alg, rules: alg-rules) = new-theorems("thm-group", ("alg": "algorithm"))
+#let (alg1, rules: alg-rules1) = new-theorems("thm-group-linear", ("alg1": "algorithm"), thm-numbering: thm-numbering-linear)
 #let theorem(name, body) = _convert(theo, name, body)
 #let lemma(name, body) = _convert(lem, name, body)
 #let corollary(name, body) = _convert(cor, name, body)
@@ -338,65 +427,7 @@
 ]
 #let algorithmLinear(name, body) = _convert(alg1, name, body)
 
-//#let theorem = base_env.with(
-//  type: "Theorem",
-//  fg: blue,
-//  bg: rgb("#e8e8f8"),
-//)
-//
-//#let proposition = base_env.with(
-//  type: "Proposition",
-//  fg: blue,
-//  bg: rgb("#e8e8f8"),
-//)
-//
-//#let example = base_env.with(
-//  type: "Example",
-//  fg: orange,
-//  bg: rgb("#f8e8e8"),
-//)
-//#let definition = base_env.with(
-//  type: "Definition",
-//  fg: orange,
-//  bg: rgb("#f8e8e8"),
-//)
-//
-//#let lemma = base_env.with(
-//  type: "Lemma",
-//  fg: purple,
-//  bg: rgb("#efe6ff"),
-//)
-//
-//#let corollary = base_env.with(
-//  type: "Corollary",
-//  fg: green,
-//  bg: rgb("#e8f8e8"),
-//)
-//#let equationNumber = locate(
-//  location => {
-//    let lvl = counter(heading).at(location)
-//    let i = counter("equation_number").at(location).first()
-//    let top = if lvl.len() > 0 { lvl.first() } else { 0 }
-//        counter("equation_number").step()
-//        align(end)[(#top.#(i+1))]
-//  }
-//)
-// Proof environment
-//#let proof(body) = block(spacing: 11.5pt, {
-//  set enum(numbering: "Step 1.1.")
-//  emph[Proof.]
-//  [ ] + body
-//  linebreak()
-//  h(1fr)
-//  box(scale(160%, origin: bottom + right, sym.square.stroked))
-//})
-//#let answer(body) = block(spacing: 11.5pt, {
-//  set enum(numbering: "Step 1.1.")
-//  body
-//  linebreak()
-//  h(1fr)
-//  box(scale(160%, origin: bottom + right, sym.square.stroked))
-//})
+
 #let note(title: "Note title", author: "Name", logo: none, date: none,
           preface: none, code_with_line_number: true, withOutlined: true, withTitle: true, withHeadingNumbering: true, 
           withChapterNewPage: false,
@@ -426,6 +457,9 @@
   show: thm-rules1
   show: alg-rules
   show: alg-rules1
+
+
+
   show emph: it => {
     text(it, weight: "bold")
   }
diff --git "a/\346\225\260\347\220\206\351\200\273\350\276\221/main.typ" "b/\346\225\260\347\220\206\351\200\273\350\276\221/main.typ"
index b1d1eec..741b66b 100644
--- "a/\346\225\260\347\220\206\351\200\273\350\276\221/main.typ"
+++ "b/\346\225\260\347\220\206\351\200\273\350\276\221/main.typ"
@@ -1295,3 +1295,60 @@
     #proof[
       只证明半可判定性。事实上，不难发现按照推理的定义，对于任意的 $n$，$n$ 步的推理序列是有限的，只要枚举所有的证明序列，则可证明的公式都可以被枚举到。
     ]
+= 数学基础
+  上一章建立的一阶逻辑是足够一般的，其中的符号可以给出任意的解释。然而，数学上有很多朴素的直觉（例如等号的对称性）并不是任何一阶逻辑解释中的有效式。我们只希望研究使得这些直觉有效的解释，也就是希望研究将这些直觉作为公理的一阶系统。
+  #definition[一阶理论][
+    一个一阶理论（有时简称理论）就是在一个一阶系统中增加公理得到的扩充。
+  ]
+  我们所谓的数学基础，也就是希望在一阶理论中引入合适的公理集来扩充一阶逻辑，以表达（尽可能多）的某个数学领域的数学定理和逻辑定理。
+  Hilbert 认为，数学的所有公理应该可以用一阶逻辑进行形式化，而数学中非形式化的证明都可以用一阶逻辑中的形式化证明精确写出。
+  == 带等词的一阶系统
+    #definition[等词公理][
+      令 #language 是一个带等词的一阶语言，也就是添加以下公理：
+      - E6: $A_1^2(x_1, x_1)$
+      - E7: 对于任意函项符 $f$ ，都有：
+        $
+          A_1^2 (u, k) -> A_1^2 (f(t_1, ..., u, ..., t_k), f(t_1, ..., k, ..., t_k))
+        $
+        其中 $t_i$ 是任意项
+      - E8: 对于任何谓词符 $A$，都有：
+        $
+          A_1^2 (u, k) ->  A(t_1, ..., u, ..., t_k) -> A(t_1, ..., k, ..., t_k)
+        $
+        其中 $t_i$ 是任意项
+    ]
+    一般而言，我们讨论数学系统时，默认它们都是带有等词公理的一阶理论（这种一阶理论也称为*带等词的一阶逻辑*）
+    #proposition[][
+      若一个一致的一阶理论有等词公理，则它存在一个模型，其中 $A_1^2$ 的解释为 $=$
+    ]
+    #proof[
+      取等价类即可
+    ]
+    #theorem[规范模型][
+      称一个带等词的一阶理论中的一个模型是规范的，如果它是至多可列无穷，且 $A_1^2$ 的解释是 $=$ \
+      任何含有等词公理的一致一阶理论都有规范模型
+    ]
+    #theorem[][
+      带等值的一阶理论也具有可靠性与完备性，同时也是一致的。
+    ]
+    #definition[摹状词][
+      有时，我们用 $iota x A(x)$ 代表满足 $A(x)$ 的项 $x$. 有时，我们要求 $A(x)$ 的项存在唯一，这种摹状词称为定摹状词。而有时只要求存在，这种摹状词称为不定摹状词。我们只讨论定摹状词，也就是对于任何谓词 $B$，定义：
+      $
+        B(iota x A(x)) := exists y (forall x (A(x) <-> x = y) and B(y))
+      $
+    ]
+    #definition[纯谓词演算][
+      不含函项符和常元的谓词演算称为纯谓词演算。在纯谓词演算中，斯科伦前束范式与原式等价。
+    ]
+  == 群语言
+    本节中，我们建立一个一阶语言，它用来描述所有群论中的形式推理。
+    #definition[群系统][
+      定义以下一阶语言：
+      - 常元: $1$
+      - 函相符: $times, *^(-1)$
+      - 谓词符: $=$
+      并在一阶逻辑的基础上添加公理：
+      - G1: $(x_1 x_2) x_3 = x_1 (x_2 x_3)$（结合律）
+      - G2: $1 x = x$（左单位元）
+      - G3: $x^(-1) x = 1$（左逆元）
+    ]
\ No newline at end of file
diff --git "a/\350\275\257\344\273\266\345\210\206\346\236\220/main.typ" "b/\350\275\257\344\273\266\345\210\206\346\236\220/main.typ"
index 9a1592e..c6aa750 100644
--- "a/\350\275\257\344\273\266\345\210\206\346\236\220/main.typ"
+++ "b/\350\275\257\344\273\266\345\210\206\346\236\220/main.typ"
@@ -718,7 +718,7 @@
       $
       i = T, i = F
       $
-      就立刻检查两个值的前驱节点。矛盾意味着这些前驱节点的值不能都同时成立，必须有一个改变，因此可以创建新的子句，代表这一组值可能产生矛盾。结束之后，直接跳回这些导致矛盾的前驱节点，重新搜索（实践表明尽管浪费了一些推导，但这样的技巧可以改善启发式选择变量的效果）。
+      就立刻检查两个值的前驱节点。矛盾意味着这些前驱节点的值不能都同时成立，必须有一个改变，因此可以创建新的子句，代表这一组值可能产生矛盾。结束之后，直接跳回这些导致矛盾的前驱节点（新加子句相关赋值的倒数第二次位置），重新搜索（实践表明尽管浪费了一些推导，但这样的技巧可以改善启发式选择变量的效果）。
 
       事实上，这样的方法保证了我们永远不会碰到相同的一组冲突，所以甚至不需要记录之前遍历过的赋值，每次任意选择剩下的变量和赋值即可。最后如果空赋值就能推出不可满足，则判定不可满足，否则继续进行。