For (some) much simpler first-order logic systems, the answer is certainly true. Tarski's axioms imply that there exists an algorithm that, for every propositio

For (some) much simpler first-order logic systems, the answer is certainly true. Tarski's axioms imply that there exists an algorithm that, for every proposition in (a restricted) Euclidean geometry, can be shown either true or false.