>>54
>例えば、自然数論の無矛盾性が
自然数論についてはゲーデルの不完全性定理が言える。
一方で実閉体の理論のように無矛盾性が証明されている理論も存在する。

https://en.wikipedia.org/wiki/Real_closed_field#Decidability_and_quantifier_elimination
Tarski showed that Trcf is complete, meaning that any Lrcf-sentence can be proven either true or false from the above axioms.
Furthermore, Trcf is decidable, meaning that there is an algorithm to determine the truth or falsity of any such sentence.

any Lrcf-sentence can be proven either true or false from the above axioms　すなわち「あるLrcf-文φが存在して Trcf|-φ かつ Trcf|-¬φ」は偽、すなわちTrcfは無矛盾。