Let us review 4 distinct concepts of «truth» for a mathematical formula, from the simplest to the most subtle.
We first saw the relative truth, that is the value of a formula interpreted in a supposedly given model (like an implicit free variable, ignoring any difficulty to specify any example). In this sense, a given formula may be as well true or false depending on the model, and on the values of its free variables there.The proof of the completeness theorem, first expressed as the existence of a model of any consistent firstorder theory, goes by constructing such models out of the infinite set of all ground expressions in a language constructed from the theory (the language of the theory plus more symbols extracted from its axioms). As the set of all ground expressions in a language can itself be constructed from this language together with the set ℕ of natural numbers, the validity of this theorem only depends on the axiom of infinity, that is the existence of ℕ as an actual infinity, sufficient for all theories (ignoring the diversity of infinities in set theory).
However, these are only theoretical properties, assuming a computer with unlimited (potentially infinite) available time and resources, able to find proofs of any size. Not only the precise size of a proof may depend on the particular formalism, but even some relatively simple formulas may only have «existing» proofs that «cannot be found» in practice as they would be too long, even bigger than the number of atoms in the visible physical Universe (as illustrated by Gödel's speedup theorem). Within limited resources, there may be no way to distinguish whether a formula is truly unprovable or a proof has only not yet been found.To include their case, the universal concept of provability (existence of a proof) has to be defined in the abstract. Namely, it can be expressed as a formula of firstorder arithmetic (the firstorder theory of natural numbers with operations of addition and multiplication), made of one existential quantifier that is unbounded in the sense of arithmetic (∃_{ℕ} p, ) where p is an encoding of the proof, and inside is a formula where all quantifiers are bounded, i.e. with finite range (∀x < (...), ...), expressing a verification of this proof.
However, once given an arithmetical formula known to be a correct expression of the provability predicate (while all such formulas are provably equivalent to each other), it still needs to be interpreted.On the other hand, it is not always refutable when false : no matter the time spent seeking in vain a proof of a given unprovable formula, we might still never be able to formally refute the possibility to finally find a proof by searching longer, because of the risk for a formula to be only provable by unreasonably long proofs.
In lack of any possible fixed ultimate algorithm to produce all truths of arithmetic, we can be interested with partial solutions: algorithms producing endless lists of ground arithmetic formulas with both qualitiesBoth conclusions should not be confused :
A standard universe U' might be axiomatically described as very big by setting it a little bigger than another very big one U, but the size of this U would need a different description (as it cannot be proven to satisfy the same axioms as U' without contradiction), but of what kind ? Describing U as also a little bigger than a third universe and so on, would require the axioms to keep track of successive differences. This would rapidly run into inefficient complications with incompatible alternatives, with no precise reason to prefer one version against others.
The natural solution, both for philosophical elegance and the efficiency and compatibility of axioms, is to focus on the opposite case, of universes described as big by how much bigger they are than any smaller one (like how we conceived a ultimate universe as the union of a standard multiverse) : axioms must be
It is also convenient because such descriptions are indeed expressible by axioms interpreted inside the universe, with no need of any external object. Indeed, if a property was only expressible using an external object (regarding this universe as a set), we could replace it by describing instead our universe as containing a subuniverse of this kind (without limiting its size beyond it), and why not also endlessly many subuniverses of this kind, forming a standard multiverse: stating that every object is contained in such a subuniverse. This is axiomatically expressible using objects outside each of these subuniverses, but inside our big one; and such axioms will fit all 3 above qualities.
Finally, the properly understood meaning of set theory is neither axiomatic nor realistic, but some fuzzy intermediate between both: its axioms aim to approach all 3 qualities (strong and open but still sound) selecting universes with the corresponding 3 qualities (big and open but still standard), but these qualities are all fuzzy, and any specific axioms list (resp. universe) only aims to approach them, while this quest can never end. Fortunately, rather simple set theories such as ZF, already satisfy these qualities to a high degree, describing much larger realities than usually needed. This is how a Platonic view of set theory (seeing the universe of all mathematical objects as a fixed, exhaustive reality) can work as a good approximation, though it cannot be an exact, absolute fact.Set theory and
Foundations of mathematics 

1. First
foundations of mathematics 
Philosophical
aspects 
1.1. Introduction
to the foundations of mathematics 1.2. Variables, sets, functions and operations 
Intuitive representation and
abstraction
Platonism vs Formalism 
1.3. Form of theories: notions, objects, metaobjects 
Realistic vs. axiomatic
theories

1.4. Formalizing
types and structures 1.5. Expressions and definable structures 
Time
in model theory
The time of interpretation
The metaphor of the usual time The infinite time between models 
1.6. Logical connectives 1.7. Classes in set theory 
Truth
undefinability
The Berry paradox
Zeno's Paradox 
1.8. Binders in set theory  Time
in Set theory
Expansion of the set
theoretical universe
Can a set contain itself ? 
1.9. Quantifiers 
The relative sense of open
quantifiers
Interpretation
of classes ⇦Classes in an expanding
universe
Concrete examples 
1.10. Formalization
of set theory 1.11. Set generation principle 
Justifying the set
generation principle
Concepts of truth in mathematics Alternative logical
frameworks

⇨ 2. Set theory
(continued)

3. Model theory
