算术化

数理逻辑中使用的一种方法。这个方法就是对一个形式系统的对象：初始符号、公式(符号的有穷序列)以及公式的有穷序列加以编码，使每一个初始符号、公式以及公式的有穷序列都对应一个特定的自然数。一个符号，公式或公式的有穷序列所对应的自然数称为该符号、公式或公式的有穷序列的数。通过这样的编码，就在形式系统的对象与自然数的一个子集之间建立一个一一对应。关于公式与公式之间的关系或关于公式的运算就转换成关于自然数间的关系成关于自然数的运算。例如，关于公式A与它的证明A，……，A(=A)之间的关系，就可用关于公式A的数a与公式序列A，……，A的数b的一个数论公式B(a，b)表示：a是公式Aa(Aa表示数a对应的公式)的数，b是公式Aa的证明的数。这样，就可以将关于形式系统的元逻辑命题转换为数论命题，把元逻辑算术化，使一个形式系统的元逻辑成为数论的一部分。特别是对于形式算术系统，在算术化之后，关于该系统的语法就可以用系统中的公式来表示。该系统中某些谓词和命题是关于该系统的谓词和命题。

K．哥德尔在他的证明形式算术系统的不完全性的论文中第一次提出应用算术化的方法。他用算术化方法和对角线法，构造了一个公式，此公式经解释后是一个真命题，但此公式及其否定在系统中都不可证。1936年，A．丘奇应用算术化证明了一个算术的不可解问题。

这种给形式系统中的对象(符号、公式以及公式的有穷序列)编码，在形式系统的对象与自然数的一个子集之间建立一一对应的方法，通常称为哥德尔配数法，形式系统的符号、公式以及公式序列所对应的数称为该符号、公式以及公式序列的哥德尔数。