So, as far as I understand, Godel's theorem says that sufficiently strong theories such as Peano Arithmetic are negation-incomplete, which means that there exists a formula $\phi$ such that neither $\phi$ nor its negation $\lnot \phi$ are provable within the formal system.
I have read somewhere that it can be understood that it means there are different models for the same axioms. By that I mean that there is an interpretation of axioms such that all axioms are true, say, interpretation $I_1$, and there is a different interpretation of axioms such that all axioms are true, say, interpretation $I_2$, and also there is a statement $\phi$ which in $I_1$ is taken to be true but in $I_2$ is taken to be false, and, thus its negation is taken as true [?1?].
Question 1: Is it true that in interpreting formal theories we always for each formula give either true or false, and for some formula $\psi$ we interpret it as true statement in the interpretation then for $\lnot \psi$ we automatically interpret it as false? If yes then what is the motivation for it? If not then what is the motivation for it?
Then, intuitively, it feels to me that if I fix some interpretation then if I prove something using formal system then it should be true in the interpretation. This is because I agree that axioms are true and deductive rules are true, so the reasoning should be true, and whenever I prove it formally, I prove it also for my interpretation.
Question 2: Is this reasoning correct?
Does it then mean that if there are two different interpretations $I_1, I_2$ then the formula about which they disagree $\psi$ is unprovable because if it was then it would be true in both interpretations by previous reasoning. The same applies for $\lnot \psi$. Can I thus conclude that Godel's theorem says that there are models that interpret axioms as true but differ in interpretation of some statements? But then does it mean that mathematics is empirical because, for example, if I want to reason about strings (which are physical objects) and I set up sufficiently strong axiomatic system for them then there will be different models and then by manipulating strings and finding empirically whether some statement is true or not I can understand which interpretation makes sense and which does not? Doesn't it show that then axiomatization in mathematics makes no sense because I would still have to perform some empirical measurements to find out the interpretation that makes sense, so that I assign truth values according to the physical reality? What I mean is that I thought axiomatization is needed in order to leave intuition and work purely syntactically. But say I want to make axiomatic theory for physics. Then, I want to be able to interpret theorems. But in order to do that I still have to make some intuitive statements and empirical statements about which interpretation to choose. So, axiomatic theory does not give me precise answer to what to expect in physical reality.
I probably went somewhere super wrong and far away from mathematics, and probably confused myself. I hope that at least some small portion of this text makes sense. Please feel free to add any comments or advice concerning this question (if it is possible to understand what I mean).