▲一阶公式的普遍有效性的推定证明可用算法来检查有效性。用技术语言来说，证明集合是原始递归的。实质上，这就是哥德尔完备性定理，虽然那个定理的通常陈述使它与算法之间的关系不明显。

　　▲有效的一阶公式的集合是不可计算的，也就是说，不存在检测普遍有效性的算法。尽管以下算法存在：对此算法输入一个一阶公式，如果这个一阶公式是普遍有效的，那么算法将在某一时刻停机，如果不是普遍有效的，那么算法将会永远不停地计算下去。然而，即使算法已经运行了亿万年，公式是否有效仍是未知数。换句话说，这一集合是“递归枚举的”，用更通俗的话来讲，是“半可判定的”。

　　▲普遍有效的二阶公式的集合甚至不是递归可枚举的。这是哥德尔不完备定理的一个结果。

　　▲勒文海姆——斯科伦定理。

　　▲相继式演算中的切消定理。

　　▲保罗·科恩（Paul Cohen）在1963年证明的连续统假设的独立性。