Our main result is a new proof of correctness of Euclid's algorithm. The proof is conducted in algorithmic theory of natural numbers Th3. A formula H is constructed that expresses the halting property of the algorithm. Next, the proof of H is is presented. In the proof we make use of inference rules of calculus of programs. The only formulas accepted without the proof are axioms of program calculus or axioms of the theory Th3. We complete our result by showing that the theorem on correctness of Euclid's algorithm can not be proved in any elementary theory of natural numbers.

翻译：我们的主要结果是给出了欧几里得算法正确性的一个新证明。该证明在自然数算法理论Th3中完成。我们构造了一个表达算法停机性质的公式H，随后给出了H的证明过程。在该证明中，我们运用了程序演算的推理规则。除程序演算公理或理论Th3的公理外，所有公式均无需证明即可接受。最后，我们通过证明欧几里得算法正确性定理在任何初等自然数理论中都不可证，完成了研究结论。