Mathematics and logic are part of a strategy that I’ll call “formalization”. Informal speech leans on (human) biological capabilities. We communicate ideas, including ideas like “natural number” and “set” using informal speech, which does not depend on definitions. Informal speech is not quite pointing and grunting, but pointing and grunting is perhaps a useful cartoon of it. If I point and grunt to a dead leaf, that does not necessarily pin down any particular concept such as “dead leaves”. It could just as well indicate the concept “things which are dry on top and wet on bottom”—including armpits. There’s a Talmudic story about a debate that might be relevant here. Nevertheless (by shared biology) informal communication is possible.
In executing the strategy of formalization, we do some informal argumentation to justify and/or attach meaning to certain symbols and/or premises and/or rules. Then we do a chain of formal manipulations. Then we do some informal argumentation to interpret the result.
Model theory is a particular strategy of justifying and/or attaching meaning to things. It consists of discussing things called “models”, possibly using counterfactuals or possible worlds as intuition boosters. Then it defines the meaning of some strings of symbols first by reference to particular models, and then “validity” by reference to all possible models, and argues that certain rules for manipulating (e.g. simplifying) strings of symbols are “validity-preserving”.
Model theory is compelling, perhaps because it seems to offer “thicker” foundations. But you do not have to go through model theory in order to do the strategy of formalization. You can justify and/or attach meaning to your formal symbols and/or rules directly. A simple example is if you write down sequences of symbols, explain how to “pronounce” them, and then say “I take these axioms to be self-evident.”.
One problem with model theory from my perspective is that it puts too much in the metatheory (the informal argumentation around the formal symbol-manipulation). Set theory seems to me like something that should be in the formal (even, machine-checkable?) part, not in the metatheory. It’s certainly possible to have two layers of formality, which in principle I have no objection to, but model theoretical arguments often seem to neglect the (informal) work to justify and attach meaning to the outer layer. Furthermore, making the formal part more complicated has costs.
Mathematics and logic are part of a strategy that I’ll call “formalization”. Informal speech leans on (human) biological capabilities. We communicate ideas, including ideas like “natural number” and “set” using informal speech, which does not depend on definitions. Informal speech is not quite pointing and grunting, but pointing and grunting is perhaps a useful cartoon of it. If I point and grunt to a dead leaf, that does not necessarily pin down any particular concept such as “dead leaves”. It could just as well indicate the concept “things which are dry on top and wet on bottom”—including armpits. There’s a Talmudic story about a debate that might be relevant here. Nevertheless (by shared biology) informal communication is possible.
In executing the strategy of formalization, we do some informal argumentation to justify and/or attach meaning to certain symbols and/or premises and/or rules. Then we do a chain of formal manipulations. Then we do some informal argumentation to interpret the result.
Model theory is a particular strategy of justifying and/or attaching meaning to things. It consists of discussing things called “models”, possibly using counterfactuals or possible worlds as intuition boosters. Then it defines the meaning of some strings of symbols first by reference to particular models, and then “validity” by reference to all possible models, and argues that certain rules for manipulating (e.g. simplifying) strings of symbols are “validity-preserving”.
Model theory is compelling, perhaps because it seems to offer “thicker” foundations. But you do not have to go through model theory in order to do the strategy of formalization. You can justify and/or attach meaning to your formal symbols and/or rules directly. A simple example is if you write down sequences of symbols, explain how to “pronounce” them, and then say “I take these axioms to be self-evident.”.
One problem with model theory from my perspective is that it puts too much in the metatheory (the informal argumentation around the formal symbol-manipulation). Set theory seems to me like something that should be in the formal (even, machine-checkable?) part, not in the metatheory. It’s certainly possible to have two layers of formality, which in principle I have no objection to, but model theoretical arguments often seem to neglect the (informal) work to justify and attach meaning to the outer layer. Furthermore, making the formal part more complicated has costs.
I think this paper by Simpson: Partial Realizations of Hilbert’s Program might be illuminating.