When one for example define a formal theory like ZFC, or even a formal theory of arithmetic, now such theories has infinitely many strings of symbols, that serve as its axioms, theorems etc.. Now proofs can be understood as collections of those strings that are closed under inference rules, and even those rules are also expressed by stings of symbols. Now the whole machinery is assumed to go on infinitely.
My question is from where we bring the necessary ink to write down all of these symbols?
If we are defining a formal system then we must be assuming that it can be written in some realm. Otherwise it makes no sense to speak about writing down something that cannot be written.
I'm of course not speaking about pieces of mathematics that can be written by an actual computer, I'm speaking about theories of theoretic mathematics that has an infinite output. The physical world doesn't have an infinite supply of material. So are we presupposing platonism here? That is, a hypothetical world where all the symbols and sentences of a formal theory or actually of a formal langauge can be written. A world that can provide such unlimited supply of ink?
If we don't want to make that pre-supposition, then how we can account for speaking about such theories and carrying inferences in them, if there is no world in which their symbols are guaranteed to be written? It appears to me that without that pre-supposition we don't really have a formal theory.
If that is pre-supposed then a formal theory must start with that hypothetical stipulation of such a world. Like for example in saying:
IF there exists a world in which we can write down all sentences of the language of arithmetic and any set of those sentences (theories), then in that world we write the following .. and we state our axioms, inference rules, provability criteria, etc...
This explicit statement would make mathematics clearly based on the Platonism thesis, since without it there is no guarantee for any of its inferences to be carried out.
Platonism doesn't have to be assumed when writing down formal theories. I'm going to give formalist answers to this however other philosophies of mathematics have there own answers.
In formalism mathematics is considered to be a system of symbols that are manipulated according to rules. However a key aspect of such systems of symbols is that you can define a new symbol systems that is isomorphic to the previous one.
So the system of arithmetic using Hindu-Arabic numbers is equivalent to the system that uses the Peano axioms. However the Hindu-Arabic numbers are more compact.
Some of these isomorphism are so compact that a finite string manipulation rule in one system is equivalent to an infinite number of string manipulations in another. So while we say informally that there are infinite axioms created by the first order axiom schema of induction; formally what is said is that there is an axiom schema which has certain text manipulation behaviours.
Formally we never deal with an infinite strings, rather we deal with finite strings that are isomorphic to infinite string systems.