This work has been prompted by the surprising lack of mathematical coherence in the common usage of some of the fundamental entities in the theory of probability, with an inherent risk of contradiction. While disentangling the intricacies, we realized that the same issue has been raised many times, with only partial solutions, notably by Boole, Hilbert, De Finetti and Renyi, among others. In particular, a restoration of foundational coherence in the usage of probability theory appears to be a missing piece in the solution of Hilbert VI problem. Here we solve the problem by a new formalization of probability theory based on a minimal collection of axioms with additional context dependent conditions, whose overall consistency is then semantically verified. In Elementary Probability, i.e. probabilities involving boolean combinations of finitely many events, our theory leads to algebraization and, using Tarski Seidenberg reduction, to a proof of decidability of all problems. Inconsistency in Elementary Probability, on the other hand, is equivalent to, suitably redefined, arbitrage or Dutch Book. In the continuous case this leads to nonstandard analysis.