I have some really big doubts about what is the real starting point of all (formal) mathematics.

For example: when I search on internet or study texts about the foundations of mathematics such as model theory, they always name "formulas" and "sets of formulas" quite easily. Model theory is done in set theory, such as ZFC of ZF (right?). But if it is really done in set theory (where everything is a set), shouldn't this formulas be sets? From what I know there should be some way to define or code formulas, but I haven't understood it yet so I'm not sure.

This is only one of my doubts, but now I'm going to explain my point of view of mathematics step by step so that it is possible to see if I'm missing something!

First order logic (FOD) can be defined and introduced without using the notion of set. Formal definitions are given in formal languages but since we haven't one yet, we eventually have to define the notions of first order logic in our natural language. This is not a tragedy, because in a certain sense we perfectly know our natural language and if we "assume" it, we can define the notions of FOD such as terms and well formed formulas. This definitions are not 100% formal, because we stated them in our language, but again, if we "assume" our natural language, then it's fine.

Now we have first order logic and well formed formulas. We can take as a primitive notions the membership predicate $\in$ and the equality predicate $=$. At this point we can state the axioms of set theory (ZFC for example), choose our inference rules and prove theorems about them. We can develop our usual mathematics with this axioms and objects, like analysis or analytic geometry. At this level, we say things like $$\exists x \forall y (y \not \in x) \hspace{20pt} \forall x \in \mathbb{N} \ \exists y \in \mathbb{N}(x+y=0) \hspace{20pt} \lim_{x \to 0} \frac{1}{x} = \infty \hspace{20pt} \zeta(s) = \sum_{n=1}^{\infty} \frac{1}{n^s}.$$

So far, inside ZFC the notions of "proof", "theory", "inference rule", "axiom", "language" are informal and their definition could be stated only in our informal natural language outside ZFC.

But now if we struggle a bit, we can use sets and what we know about them to formalize into ZFC our intuitive notions of formal languages, predicates, formal systems and formal theories, rules of inference, proofs and theorems (even if I don't know very well how all this complicated definitions are given). So we have defined our FOD idea into ZFC (that makes use of our intuitive FOD!). Now in ZFC we are able to formally define what a formal theory is and study it, defining the relations of "provable" $\vdash$ for set of predicates and "satisfiable" $\vDash$ between algebraic structures ("models") and set of predicates. At this level we can now say things like $$\lbrace p,q\rbrace \vdash p \wedge q \hspace{20pt} \mathcal{M} \vDash \sf PA \hspace{20pt} \textrm{Con}(T) \Leftrightarrow \nexists \varphi ( T \vdash \varphi \wedge T \vdash \neg \varphi)$$ and all of this objects are sets of our intuitive ZFC domain of discourse, so we can treat them as usual sets. In short, we are doing metamathematics in ZFC, studying theories (such as PA) written in some formal languages and asking if they are consistent, complete or sound, and all this objects are just sets. We could also study ZFC itself and define it as the set of axioms that we initially stated before. Note that now we have a formal definition of what a proof is for the formal languages that we have defined, but this is a definition for our object theories and not for our first ZFC, which has been defined just with our natural language (unless we are studying ZFC itself).

Is this view of mathematics correct or is there something that I'm missing?

I see that often it is used a completely different approach, and sometimes I even find that some metamathematical argouments or definitions are circular. I feel there's something that I'm not getting... but I don't know what it is.

Thank you for the possible help :P

  • 2
    $\begingroup$ Regarding your first question, sure, when we formalize model theory in set theory, our formulas, like any other mathematical objects, will be encoded as sets. If you are familiar with Godel numbering, it is the same as that, only with sets rather than numbers. And in set theory we can encode formulas much more naturally off the shelf, e.g. using nested ordered pairs to represent the syntax tree. $\endgroup$ – spaceisdarkgreen Feb 24 at 16:10
  • $\begingroup$ I’m not sure I fully understand the rest (but I haven’t read that closely), but note that while model theory requires some set theory in the metatheory to formalize, we don’t need model theory to carry out and verify proofs in ZFC. For this a very weak, even finitary metatheory suffices. $\endgroup$ – spaceisdarkgreen Feb 24 at 16:20
  • 1
    $\begingroup$ @Luis and btw I should have emphasized above that the reason we need nontrivial amounts of set theory to do model theory has nothing to do with formulas which we know can be encoded in much weaker theories. It is to handle structures. $\endgroup$ – spaceisdarkgreen Feb 24 at 17:36
  • 1
    $\begingroup$ It is probably worth pointing out that many texts in mathematical logic are not attempting to be foundational. They assume you're already fine with ZFC somehow, and are simply trying to explore logic from a mathematical perspective. If you took them as foundational, i.e. as trying to justify logic, then they really would be circular. Texts with a more foundational orientation usually work in PA or PRA, and the formulas will usually be represented by numbers, not sets. These usually take a proof-theoretic rather than model-theoretic approach. $\endgroup$ – Derek Elkins Feb 25 at 8:47
  • 1
    $\begingroup$ @Luis I know this is in various books but no reference springs to mind. You use the parsability of ordered tuples. For terms you can encode the n-th variable as $(n,0)$ and you can encode a set parameter $a$ as $(a,1).$ For formulas, you can write atomic formulas $t=u$ as $(0,c(t),c(u))$ where $c$ is the coding function we’re defining recursively. Similarly for $t\in u$ only with a $1.$ Then can code $\lnot \phi$ as $(2, c(\phi)),$ similarly for $\land$. $\exists x_n\phi$ would be $(4,n,c(\phi)).$ So $\exists x_1 (x_1\in x_2)$ would be encoded $(4, 1, (1, (1,0),(2,0))).$ $\endgroup$ – spaceisdarkgreen Mar 7 at 15:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.