研究一个逻辑系统，好比一个语言学家研究英文的文法跟规则，他需要其他语言来当一个客观的参照，避免陷入自己解释自己的矛盾循环中。我们要研究的逻辑语言称为目标语言(object language)，研究逻辑系统时，用来客观参照目标语言的语言称为元语言(metalanguage)，元语言的逻辑也会称为元逻辑(metalogic)。而在元逻辑下，推出目标语言的有关性质特称为元定理(metatheorem)。
事实上我们采用的元语言只是比较有条理的中文，配上一些逻辑符号:
(a)$\displaystyle \to$：实质条件意义下的推理
(b)$\ulcorner$, $\urcorner$：引用一段目标语言的叙述
(c)$\displaystyle\sim$：否定后面的叙述。
我们用中文的"或"跟"且"来代表元逻辑理的对应概念。我们也会使用中文语法里的否定去否定一段元逻辑的叙述。
所谓的推理一定是基于某些已知，运用某些推理规则而推出一个结果，这就是数理逻辑理解证明所依据的哲学，所以这边不会讨论如哲学家康德(Immanuel Kant)所相信的先验(a priori)或是自美国文学界兴起的超验(Transcendentalism)。
数学的终极目标就是找出让某个现象成立最少所需要的条件(最好能互相独立)，据以做为某套理论的基石，称为公理(axiom)；但是有时候，套用一个理论解释某个现象，像是用马克士威的方程式去解释电磁场在导线里的传播时，我们要额外考虑导线的截面是方形还是圆，这就是不在公理的范围里的前提假设(premise)。
由这些想法，就可以先粗略的给出数学理论在形式上要满足的要求:
(1)有一套符号作为这个理论语言的单元，而这一套符号的数量可能跟自然数一样多。任何一组符号称为公式(formulas)
(2)有一套文法去规定，怎样的符号组合是合于这个理论的形式而有意义的，符合规则的公式称为合式公式(well-formed formulas)，简记为$\displaystyle wf$，复数的时候加$\displaystyle s$。
(3)有一套$\displaystyle wfs$称为公理(axiom)。
(4)一套推理规则。
符合这些要求的数学理论称为形式理论(formal theory)
ex.
命题逻辑的形式理论
(1)$\displaystyle A_1,A_2,A_3....$采用当叙述字母；没有下标的大写英文字母用来表示任意的叙述字母；$\neg,\Rightarrow$采用当命题连接词；"$\displaystyle ($"和"$\displaystyle )$"被用来表示命题连接词的施用顺序。(小括弧太多的话，会额外采用中括弧跟大括弧以清楚标示)
(2)叙述字母都是$\displaystyle wf$；如果$\mathcal{B},\mathcal{C}$(注意这个是元语言的符号)是$\displaystyle wf$，那$(\neg\mathcal{B}),(\mathcal{B}\Rightarrow\mathcal{C})$都是$\displaystyle wf$。除此之外没有其他方法建构出$\displaystyle wf$。
括弧可以依照括弧规则的标准省略；习惯上用草写英文字母代表$\displaystyle wf$。
(3)公理：如果$\mathcal{B},\mathcal{C},\mathcal{D}$是$\displaystyle wf$
(4)推理规则：$(\mathcal{B}\Rightarrow\mathcal{C})$跟$\mathcal{B}$可以推出$\mathcal{C}$(MP律)
注意到我们定义$\displaystyle wf$的方式是用递回的方式，也就是以叙述字母为基础，依照既定的规则重复添加命题连接词建构出来的。
形式理论所谓$\mathcal{B}$的证明，指的是一列$\mathcal{C}_1,\mathcal{C}_2,....,\mathcal{C}_n$这样的$\displaystyle wfs$。其中$\mathcal{C}_1$可能是公理，也可能是前提假设。而中间任意的$\mathcal{C}_k\,(k>1)$，要不是前提假设或是公理；要不就是有$\displaystyle l, m < k$使$\mathcal{C}_{l}$和$\mathcal{C}_{m}$配上推理规则就可以推出$\mathcal{C}_{k}$。最后$\mathcal{C}_n$必须是$\mathcal{B}$。
ex.
命题逻辑的形式理论下，如果$\mathcal{B}$是$\displaystyle wf$，$\mathcal{B}\Rightarrow\mathcal{B}$的证明：
$\mathcal{C}_1$：$\{\mathcal{B}\Rightarrow[(\mathcal{B}\Rightarrow\mathcal{B})\Rightarrow\mathcal{B}]\}\Rightarrow\{[\mathcal{B}\Rightarrow(\mathcal{B}\Rightarrow\mathcal{B})]\Rightarrow(\mathcal{B}\Rightarrow\mathcal{B})\}$ (公理A2)
$\mathcal{C}_2$：$\mathcal{B}\Rightarrow[(\mathcal{B}\Rightarrow\mathcal{B})\Rightarrow\mathcal{B}]$ (公理A1)
$\mathcal{C}_3$：$\mathcal{B}\Rightarrow(\mathcal{B}\Rightarrow\mathcal{B})$ (公理A1)
$\mathcal{C}_4$：$[\mathcal{B}\Rightarrow(\mathcal{B}\Rightarrow\mathcal{B})]\Rightarrow(\mathcal{B}\Rightarrow\mathcal{B})$ ($\mathcal{C}_1$和$\mathcal{C}_2$加上MP律)
$\mathcal{C}_5$：$\mathcal{B}\Rightarrow\mathcal{B}$ ($\mathcal{C}_4$和$\mathcal{C}_3$加上MP律)
如果形式理论$\mathcal{L}$里，有一群$\displaystyle wfs$，以$\displaystyle\Gamma$代表；$\mathcal{B}$在形式理论$\mathcal{L}$有证明；而这个证明里或许有引用$\displaystyle\Gamma$里的$\displaystyle wf$，或是引用$\mathcal{D}_1,\mathcal{D}_2,....,\mathcal{D}_k$里的$\displaystyle wf$话，这种情况我们以符号$\Gamma,\mathcal{D}_1,\mathcal{D}_2,....,\mathcal{D}_k\,{\vdash}_{\mathcal{L}}\,\mathcal{B}$代表。不需要的$\displaystyle wf$可以省略不写。
如果$\mathcal{B}$在$\mathcal{L}$的证明不需要任何前提假设(也就是只需要公理或是自己就是公理)，$\mathcal{B}$被称为定理(theorem)，以${\vdash}_{\mathcal{L}}\,\mathcal{B}$代表。
如果采用哪个形式理论从上下文很清楚的话，${\vdash}_{\mathcal{L}}$的形式理论下标$\mathcal{L}$可以省略，像本章采用的形式理论都是命题逻辑，所以我们都省略。
其实一般数学理论的内容，定理会因为编者的个人判断；觉得重要性比较小而别称为命题(proposition)或是性质(property)，或根据前后的推理关系称为系理(corollary)或引理(lemma)。
在进一步说明形式理论的一些额外要求之前，需要了解一些命题逻辑的性质。
推论元定理(metatheorem of deduction)：
$\ulcorner\,\Gamma,\mathcal{B}\vdash\mathcal{C}\,\urcorner\to\ulcorner\,\Gamma\vdash\mathcal{B}\Rightarrow\mathcal{C}\,\urcorner$
| 证明 |
|---|
|
证明(注意这是元逻辑意义下的证明)： 假设$\mathcal{C}_1,\mathcal{C}_2,....,\mathcal{C}_n$就是条件所说$\mathcal{C}$的证明，如果$\mathcal{C}_1$本身是从$\displaystyle\Gamma$来的前提假设或是公理，那根据公理(A1)，$\vdash\mathcal{C}_1\Rightarrow(\mathcal{B}\Rightarrow\mathcal{C}_1)$，所以由MP律$\Gamma\vdash\mathcal{B}\Rightarrow\mathcal{C}_1$。 如果$\mathcal{C}_1$本身是$\mathcal{B}$，那根据我们讲解证明的例子($\vdash\mathcal{B}\Rightarrow\mathcal{B}$)，仍然可以推出$\Gamma\vdash\mathcal{B}\Rightarrow\mathcal{C}_1$，所以$\mathcal{C}_1$的情况已经全部证明完毕。 接下来我们要用归纳法；假设对$\displaystyle i<k$都有$\Gamma\vdash\mathcal{B}\Rightarrow\mathcal{C}_i$。如果$\mathcal{C}_k$是公理、或是从$\displaystyle\Gamma$来的、或是他自己根本就是$\mathcal{B}$，仿造$\mathcal{C}_1$的情况就可以证明$\Gamma\vdash\mathcal{B}\Rightarrow\mathcal{C}_k$。 剩下没考虑的状况是由MP律组合出$\mathcal{C}_k$的状况，也就是有$\displaystyle l,m<k$使得 $\mathcal{C}_m:\mathcal{C}_l\Rightarrow\mathcal{C}_k$。 套用公理A2有 $\vdash[\mathcal{B}\Rightarrow(\mathcal{C}_l\Rightarrow\mathcal{C}_k)]\Rightarrow[(\mathcal{B}\Rightarrow\mathcal{C}_l)\Rightarrow(\mathcal{B}\Rightarrow\mathcal{C}_k)]$ 套用我们归纳法的假设，加上MP律，就会发现$\Gamma\vdash\mathcal{B}\Rightarrow\mathcal{C}_k$。这样就可以一路归纳到$\mathcal{C}_n$也就是$\mathcal{C}$的情况，所以元定理得到证明。$\Box$ |
这个元定理说"$\Rightarrow$"跟"$\vdash$"可以互换；因为$\ulcorner\,\Gamma\vdash\mathcal{B}\Rightarrow\mathcal{C}\,\urcorner\to\ulcorner\,\Gamma,\mathcal{B}\vdash\mathcal{C}\,\urcorner$是很显然的，就只是MP律的应用而已。
有时会为了保持证明的"纯洁"，不用申明采用推论元定理，我们会偷懒的把定理表达成$\mathcal{A}\vdash\mathcal{B}$的样子，甚至以此类推，把$\Rightarrow$前的$\displaystyle wf$逐一的移到$\vdash$前以方便直观的理解。
注意到推论元定理的证明仅仅需要MP律、(A1)和(A2)(所以日后可以直接适用于一阶逻辑)。
由推论元定理配上MP律，可以很轻易得到以下很直观的逻辑定理
$\displaystyle (D1)$$\mathcal{A}\Rightarrow\mathcal{B},\mathcal{B}\Rightarrow\mathcal{C}\vdash\mathcal{A}\Rightarrow\mathcal{C}$
$\displaystyle (D2)$$\mathcal{A}\Rightarrow(\mathcal{B}\Rightarrow\mathcal{C}),\mathcal{B}\vdash\mathcal{A}\Rightarrow\mathcal{C}$
本节会用到一些常用的逻辑定理，请依照定理的代号查找。
提出命题逻辑的形式理论以后，会很自然地会要求，以真假值为基础的命题逻辑下的恒等式，理当是这个形式理论下的定理，反过来也要对。
读者回忆一下命题逻辑#合式公式曾证明的MP律；然后自证(A1)~(A3)都是恒等式，这样就可以证明形式理论下的定理都是恒等式。
在证明恒等式都是命题逻辑形式理论的定理之前，我们需要一个辅助的元定理
元定理：
$\mathcal{A}$是一个含叙述字母$\displaystyle A_1,A_2,....,A_n$的$\displaystyle wf$；若根据某组指定的叙述字母真假值，得出的$\mathcal{A}$真假值下，做以下的选取
$A_k': \begin{cases} \begin{matrix} A_k & (A_k:\top) \\ \neg A_k & (A_k:\bot) \end{matrix} \end{cases}$ $\mathcal{A}': \begin{cases} \begin{matrix} \mathcal{A}& (\mathcal{A}:\top) \\ \neg\mathcal{A} & (\mathcal{A}:\bot) \end{matrix} \end{cases}$
则在形式理论下$A_1',A_2',....,A_n'\vdash\mathcal{A}'$
| 证明 |
|---|
|
$\displaystyle wf$是以$\Rightarrow$、$\neg$和叙述字母基础，用递回的方式建构出来的，所以我们针对两者的总数量做归纳，就可以遍及一切$\mathcal{A}$的可能形式。 数量为零的情况，$\mathcal{A}$就只是叙述字母，显然本元定理是成立的。 现在假设$\Rightarrow$和$\neg$的数量少于$\displaystyle n$的情况，元定理是正确的；若$\mathcal{A}$内含有数量$\displaystyle n$个的$\Rightarrow$或$\neg$，则根据我们对$\displaystyle wf$的定义，这里会有$\Rightarrow$和$\neg$的总数量少于$\displaystyle n$的$\mathcal{B}$和$\mathcal{C}$，使得$\mathcal{A}$可以表达成$\neg\mathcal{B}$或$\mathcal{B}\Rightarrow\mathcal{C}$这两种可能的形式。 (1)$\mathcal{A}:\neg\mathcal{B}$
(2)$\mathcal{A}:\mathcal{B}\Rightarrow\mathcal{C}$
综上所述，元定理已对所有可能的$\mathcal{A}$形式完成证明$\Box$ |
例子：
$\mathcal{A}:\neg(\neg A_1\Rightarrow A_2)$，若指定$\displaystyle A_1$和$\displaystyle A_2$都为真，则会得到$\mathcal{A}$为假，这种情况下$\displaystyle A_1'$仅仅是$\displaystyle A_1$；$\displaystyle A_2'$仅仅是$\displaystyle A_2$，$\mathcal{A}'$为$\neg\neg(\neg A_1\Rightarrow A_2)$，则
$A_1,A_2\vdash\neg\neg(\neg A_1\Rightarrow A_2)$ (A1, DN)
这个元定理非常的直观；也就是没有加上"$\neg$"可以视为形式理论的"真"，反之视为"假"，这样的"真假组合"的确可以推出跟真假值相符合的"真值函数"。
元定理：(命题逻辑形式理论的完备性)
命题逻辑的真假值的恒等式也一定是命题逻辑形式理论里的定理
| 证明 |
|---|
|
假设$\mathcal{A}$是含叙述字母$\displaystyle A_1,A_2,....,A_n$的$\displaystyle wf$，是真假值的意义下的恒等式，根据上面的元定理 $A_1',A_2',....,A_n\vdash\mathcal{A}$ $A_1',A_2',....,\neg A_n\vdash\mathcal{A}$ 所以根据(C3)配上推论元定理 $A_1',A_2',....,A_{n-1}'\vdash\mathcal{A}$ 以这样的手法消去，最后我们会得到$\vdash\mathcal{A}$。$\Box$ |
真假值要求$\mathcal{A}$和$\neg\mathcal{A}$不能同时为真，所以两者不可能同时为定理；一般来说，一个$\mathcal{A}$和$\neg\mathcal{A}$不能同时为定理的形式理论称为自洽的(consistent)。更进一步的，回忆一下(M0)，这个定理的直观意义是若有个$\displaystyle wf$他的否定跟本身都是对的，则可以推出任意$\displaystyle wf$是对的；这引申出自洽性更一般的定义，一个并非所有$\displaystyle wf$都是定理的形式理论称为绝对自洽的(absolutely consistent)