Does an axiom have to be “true”? For instance, is it allowed to build a formal system similar to the
one discussed in the video, but starting from the axiom “1+1=3” ?
no it axiom can be false and formal system consistent to the false axiom
because
Axioms are not proven; they are accepted as the foundation of a system.
The truth of an axiom is relative to the system it defines.
You can build a formal system with any axioms, even ones that contradict conventional mathematics, as long as the system is logically consistent (or you explore what happens when it isn’t).