Negation-incompleteness, Godel's theorems and interpretations

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).

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 $$\neg\psi$$ we automatically interpret it as false?

Yes -- that's how the usual semantics of first-order logic works. Once an interpretation of the theory (actually an interpretation of the logical language the theory is expressed in), every sentence has a definite truth value, either "true" or "false".

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.

Yes, with the important caveat that your interpretation needs to be a model of the theory -- that is, every axiom of you theory must be "true" in that interpretation.

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 $$\neg\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?

Yes, that is correct.

But then does it mean that mathematics is empirical

No, not in what I would think is a useful sense. It just tells you that no matter which set of reasonable axioms you choose, they won't allow you to prove everything about the model you have in mind.

If you have a theory about, say, the integers, it is not the job of the theory to produce models. You're supposed to already have a model in mind (usually this will be the integers and arithmetic you learned in elementary school), and the theory then defines something you decide to accept as "definitely convincing proofs".

The fact that the theory has models other than the one you had in mind originally is interesting, but doesn't mean that you suddenly can't distinguish those models from what you had in mind.

The integers and their arithmetic come before formal logic. Logic gives you a mathematical model of the usual semi-rigorous concept of "proof". It's not what creates the integers themselves, nor is it what causes proofs to be convincing to real mathematicians.

• thanks for the great answer! One more question, does it mean if there are two different models for some theory then if I remove some axioms from this theory then there still will be at least two different models for the new theory? – Daniels Krimans Oct 29 '18 at 22:30
• @DanielsKrimans Yup - removing axioms leads to more models (or at least, no fewer models). Think of axioms as restrictions on the class of structures. – Noah Schweber Oct 29 '18 at 22:42
• @DanielsKrimans: A "sentence" is a technical term here -- it means a formula that has no free variables. Therefore "$x$ is even" is not a sentence. The semantics gives a definite truth value to non-sentences only when we have both an interpretation and a particular value to assume for each of the free variables. – Henning Makholm Oct 29 '18 at 22:45
• @DanielsKrimans A bit of abstraction: given a structure $M$, we can think of a formula $\varphi$ with $n$ free variables $x_1,...,x_n$ as giving a map from $M^n$ to $\{\top,\perp\}$ (and the preimage of $\{\top\}$ under this map - that is, the set of variable assignments making the formula true in $M$ - is usually denoted "$\varphi^M$"). Note that even a formula which is always true like "$x=x$" (or always false like "$x\not=x$") is still not a sentence: basically, this is the difference between the constant function $M\rightarrow\{\top,\perp\}: m\mapsto \top$ and the truth value $\top$. – Noah Schweber Nov 2 '18 at 0:38
• This is all utterly unnecessary here, and often just adds confusion, but I think you might find it a little "grounding" in the sense that it shows we're not somehow ignoring formulas in favor of sentences, we just have to be a bit more clever how we think about them mathematically. – Noah Schweber Nov 2 '18 at 0:38