It's time to talk about models and theories! I'm going to spend some time whipping up the notions of language, structures, theories, and models, which are one of the ways we can use to define things and talk about things in mathematics.
Language
Since we're going to get into more formal mathematics, it quickly becomes useful to make rules for what's a valid statement to write down and check things about. And one way you can do that is by defining a language.
The above explains it fairly well, a language is just the decision of what's a valid statement to say, it includes valid variables, functions, constants, and relations. It is where you put all your syntax and grammar.
For example, a language for talking about the natural numbers might be:
S,+,*,0,1,2,3,4,5,6,7,8,9,x,y,z,<,=
With rules describing the arity (how many "arguments" something takes in before being valid. 0 has arity 0, because 0 is already a natural number, while + has arity 2, because it need to take in two valid expressions, one in each side, in order to be valid) and order of operations and the fact that you can put digits next to each other. And denoting which of these form "terms" (that being actual elements of what you are talking about.) and which of these form sentences (true false statements, relations checking whether or not something is true, such as < and =)
By convention, the usual logical symbols are allowed to connect sentences, but are not usually considered part of the language. The = sign is conventionally default as well. Those symbols are the underlying symbols that so much of mathematics uses we consider explicitly notating them a waste of time. They are part of the proof system you choose.
You also distinguish between constants and variables. This is because constants need something to be assigned to them, but variables do not matter (it changes nothing to allow them to be assigned, but it's not worth the effort to write an assignment). Variables must always be terms of arity 0.
Notably, at the moment, it is devoid of meaning beyond terms and sentences. We don't know what are variables and what are actual things. This only denotes what are valid ways to construct sentences. S(2)=8 is a valid sentence. 9=1 is valid. +=* is not, since the grammar rules aren't followed.
We usually like more minimal language that we can build syntactic sugar on later. That is, if you can express something in terms of other things in the language, instead of adding it in as a separate symbol, you can just claim that it is a shorthand for some other thing. An example of this is the standard language of sets, which only uses the operation ∈ . x⊂y is defined as a shorthand for "∀z z∈x⇒z∈y ".
Structures
A structure is a universe with an assignment of meaning to the language by providing an explicit construction.
Universes are collections of objects and functions and relations that act on the whole universe cannot take things outside of the universe.
For example, you can look at the natural numbers, and make a universe with one object, with functions that take it to itself, and assign that one object to every term. And assign true to every relation.
In this universe, 3=4, 1+1=0, 4<2, 2<4.
This is not the usual structure of the natural numbers. And not a useful one to think about. So we need a way to specify which structures actually count for what we are talking about.
Theories
A theory is a language, equipped with some sentences that must be guaranteed to be true, called our axioms. They are our wishlist for the structure. For example, the theory of groups can be stated as:
Language:
∙ with arity 2, 1, with arity 1.
a,b,c,x,y,z, x₀,x₁,x₂,x₃,x₄... as our variables, with arity 0. Because we'll want to use variables.
And then some sentences we wish to guarantee are true:
∀a 1∙a=a ⋀ a=a∙1
∀a∀b∀c (a∙b)∙c=a∙(b∙c)
∀a∃b ab=1 ⋀ 1=ba
That is it! The theory of groups! As a shorthand I will label these G0, G1, G2.
We often use the syntactic sugar thar xy is the same as x∙y.
We can use the axioms to figure out other things that also must be true beyond our wishlist. For example, we can prove that 1 must be unique in having the property that it is an identity. Since if we assume that:
xy=x
Then there is some z such that zx=1, hence
z(xy)=zx
And thus
(zx)y=zx
1y=1
y=1
Tadah!
We use thw turnstile symbol, ⊢ to claim that the theory with the sentences on the left of it "entail" the sentences on the right, or, in other words, any structure that satisfies the theory must also satisfy something on the right.
In order to do this formally, we use systems like lk-sequent calculus, or hilbert systems. Or a bunch of others.
I will use Groups to refer to all the axioms of groups packaged up. G0, G1, G2.
Details of the formality may look a bit silly, but I will likely do a later post explaining proof systems much more thoroughly. For now, a glimpse:
First I make all the substitutions I want:
1. ⊢ zx=zx
2. xy=x ⊢ z(xy)=zx
3. xy=x, z(xy)=(zx)y ⊢ (zx)y=zx
4. xy=x, z(xy)=(zx)y, zx=1 ⊢ 1y=1
5. xy=x, z(xy)=(zx)y, zx=1, 1y=y ⊢ y=1
And then I slowly show that most of these substitutions follow from the axioms, mostly by claiming that if I can prove it from specific assumptions about x, y, and z, then I can prove it if those assumptions hold everywhere. (∀-left).
6. xy=x, (zx)y=z(xy), zx=1, 1y=y ⊢ y=1
7. xy=x, ∀a∀b∀c (ab)c=a(bc), zx=1, 1y=y ⊢ y=1
Notably, that's G1, hence:
8. G1, xy=x, zx=1, 1y=y ⊢ y=1
9. G1, xy=x, zx=1, 1y=y ⋀ y=1y ⊢ y= 1
10. G1, xy=x, zx=1, ∀a 1∙a=a ⋀ a=a∙1 ⊢ y=1
But that's G0.
11. G0, G1, xy=x, zx=1 ⊢ y=1
12. G0, G1, xy=x, 1=zx ⊢ y=1
13. G0, G1, xy=x, xz=1 ⋀ 1=zx ⊢ y=11
14. G0, G1, xy=x, ∃b xb=1 ⋀ 1=bx ⊢ y=1
15. G0, G1, xy=x, ∀a∃b ab=1 ⋀ 1=ba ⊢ y=1
But that's G2.
16. G0, G1, G2, xy=x ⊢ y=1
17. Groups, ∃a ay=a ⊢ y=1
18. Groups ⊢ ∃a ay=a ⇒ y=1
Deductrium is an excellent free online game for actually learning about formal proofs. (Particularly in a hilbert system.)
Models
All a model is, is a structure that satisfies a theory. That is, a structure in which the axioms are true.
For example:
A universe 0,1 along with + where 0 is assigned to 1 in the theory, + is assigned to ∙. Under the following construction:
0+0=0
0+1=1
1+0=1
1+1=0
It's quite easy to check your way through G0 and G2. G1 is somewhat tedious.
Therefore that universe under that assignment is a model of the theory of groups.
We can say that this structure "models" the theory of groups. Or that this structure is a group.
This allows us to formally describe and define things.