The paper deals with the question how to introduce constructive mathematics into theoretical physics. \textit{W. K. Burton} [Contrib. Math. Logic, Proc. Logic Colloquium, Hannover 1966, 75-89 (1968; Zbl 0181.30801)] first showed that the Giles formulation of thermodynamics [\textit{R. Giles}: Mathematical foundations of thermodynamics (1964; Zbl 0116.45204)] includes some undecidable principles. He interpreted such result as the proof that constructive mathematics is not able to express a physical theory. That a principle is undecidable means that we have no algorithm to test whether it holds true or not in general; hence, it cannot be a universal statement; in other words, it cannot be the principle of any theory. Here, principles of Carathéodory's formulation [\textit{C. Carathéodory}, Math. Ann. 67, 355-386 (1909)] are scrutinized for a constructive version (by adopting a particular constructive mathematics, the computable mathematics by \textit{O. Aberth } [Computable analysis (1980; Zbl 0461.03015)]). It is shown that Carathéodory's Axiom is undecidable, as well as the principles of some more formulations (Buchdahl, Cällen). On the contrary, the principles of the common Carnot-Kelvin-Clausius formulation are trivially decidable. Therefore constructive mathematics results are effective in either accepting or rejecting formulations of a physical theory. Among some philosophical implications of the above results, it is stressed that constructive mathematics, even if not so powerful as classical mathematics, not only is able to produce almost every significant result pertaining to classical mathematics (as Aberth showed), but rejects some formulations of a physical theory as essentially platonistic in their principles.