I would want to do mathematics properly, so that the proofs of results can be trusted on instead of them being just suggestions on which results could perhaps apply. This means formulating the math in explicit substitution rules on finite symbol sequences (so something of which workings everyone can agree on initially). Because I could not find any decent text on this on (enough expressive) type theories, I thought I could do with material set theories which I am little familiar with to begin with, so at least I know where to start. I, however, ran into problems, the main one (that I see) currently being that I cannot find a practical set of proof rules for FOL.
Namely, my idea was obviously that I would use FOL (special case of which my set theory would be), but to formulate mathematicians' arguments (that usually are claimed to be inside set theory) in this, I would need proof rules to which to be able to transfer their arguments. However, I observed right away that mathematicians seem to assume certain first-order proposition schemas that I here call "evidently valid" without reference to any proof rules. As I found no suitable set of proof rules in which the proofs of these would be evident, my next idea was to do enough with known unpractical rules to achieve something more practical by some meta-argument. However, I did not manage this either.
Obviously most mathematicians can be seen not to specify at all that their proving would be anything other than that it complies to some cultural standards, but the exception I found was some logicians who seemingly claim that they can formally prove propositions by what is essentially model theory itself or completeness. Indeed, I especially observed that in many books on mathematical logic a writer would use few proof rules until proving completeness and then refer to that in the proofs. However, I do not see that the naive idea "use Hilbert-style deduction until completeness and then all the intuitive proof machinery mathematicians use is available" does really work. In fact, I found no way to use completeness at all.
To consider this technically, suppose I manage to formulate FOL embedded inside (my set theory) with suitable short-hands to make it manageable. It seems to me it gets generally quite complicated to work with embedded theories inside the set theory, but suppose for now I manage to prove completeness for the embedded FOL.
This does not yet say anything about my outer set theory, so what I believe I need to do next is prove in my meta theory an embedding theorem that any formula is provable in my outer set theory if its embedded version is provable – the embedded version representing provability of the same formula but in the embedded set theory (special case of the inside FOL) in which completeness applies.
First of all, whereas this is seemingly formal, this defeats the idea that set theory was the foundation in the first place – indeed, above makes the meta theory much more used than to set up the foundational theory. Instead, it is used quite heavily to show arguments about the foundation.
I do not think it is a good idea either to suddenly decide the foundation is set theory inside set theory and not even try to show anything in the outer theory – indeed, I believe this kind of "transfer" sweeping problems under the rug leads eventually even to more embeddings, so one never gets anything done to any fixed theory really. Moreover, I believe any kind of unreturnable embeddings make the theory pretty much unusable being so complex in that one has to work through many different levels even to make simplest argument.
Let us then assume we accept we use the meta theory more heavily (this is not true problem with formality after all because the needed arguments in the meta theory are still achievable with conclusions about symbol sequences). Then, probably I could manage the embedding theorem.
However, the real complication I think actually arises even after this. Namely, the whole point was to be able to use completeness to prove things, but I found no (general) way to actually transfer anything to the outer set theory from what now technically seems to be is just some incoherent intuition about workings of some models. Obviously countable completeness suffices and the set theory needed does not need to be so strong, but this does not seem to make things any easier.
In fact, I would argue that if one could actually deduce from completeness that the "evidently valid" proposition schemas are provable, then one should be able to factually write this argument symbolically hence get an axiomatization together with a proof rule that one could use in the outer theory of FOL in the first place when defining it.
Now, obviously this supposed rule cannot prove all valid formulas as otherwise it being based on the evident validity would make validity of propositions of FOL decidable, but the idea is that the rule is sufficient enough to prove the "evidently valid" proposition schemas.
So my questions are, 1) is there a known system of axioms and proof rules of FOL that would actually capture how mathematicians do mathematics, so one could formulate their proofs formally in the initial theory per the requirements I set forth? If such set of rules is not known, then as far as no one has verified proofs of mathematicians with any of the seemingly unusable proof rules like some normal Hilbert system (this is I believe quite difficult), 2) what exactly is the approach to formalize mathematics using material set theory that is (I believe) generally claimed to exist?
One might postulate that there is no set of rules that show the "evidently valid" proposition schemas, but I find this a bit difficult to believe. Indeed, it seems the arguments mathematicians do are something they can presumably do in their head, so if anything any "evidently valid" schema should be very shortly describable hence short as schema in formal FOL. So my instinct is that they should definitely be describable if not all in total very shortly then at least say provable as together by a computer by modus ponens and quantifier rule from some very short list of axiom schemas (after all, the schemas should for example probably have some small upper bound in their length).
However, if no one has described these evidently valid proposition schemas (e.g.\ specified them as axioms), I find it really difficult to grasp how can mathematicians exactly claim there is formality in their arguments at all. If the case is that the material set theories are claimed to be foundational only in the sense that it is believed the arguments of mathematicians "could be" transferred to some simple set of proof rules, 3) what exactly is the value of this kind of "belief" i.e.\ is there perhaps some kind of formal argument that I could formally really see to make sense but which is distinct from specifying the "evidently valid" schemas?
I would also be interested in the continuation. Even if I find a suitable way for FOL to work well enough, 4) at what point am I going to just tangle myself in problems with the material approach anyway? and 5) is some kind of type theory a viable solution already i.e.\ has someone actually demonstrated that there one would not need to e.g.\ assume dynamically "evidently valid" claims or use computation otherwise to describe the system (or is this perhaps at least probable)?
Overall I have so many questions about the formalization ability of type theory and have found no sources that answer these in any satisfying way. I would for example want clarification on 6) whether classical proving in type theory is so primary concept that one can be guaranteed not to have need to argue in the meta theory i.e.\ outside type theory itself (which seems to be major problem with any such weak system as material set theories)? I have yet to find a book that would even describe properly any enough expressible formal type theory, so that I could really get to type theory.
