ELI maths enthusiast: I'm a bit hazy about the link between provability/decidability of a proposition, and existence of models. Does independence imply the existence of models going "either way"?
* The parallel postulate is independent from the other axioms of Euclidean Geometry. That means we cannot formally deduce the parallel postulate nor its negation from the other axioms, correct? And now crossing the river to the "existence of models" side, there are indeed models of Euclidean geometry (i.e. structures satisfying or "implementing" the axioms) which satisfy the other axioms plus the PP, and models which satisfy the other axioms plus the negation of PP.
* The axiom of choice is independent from ZF. That means that neither it nor its negation can be proven from ZF. Is the same about models true here? Are there models of set theory satisfying ZFC and other models satisfying ZF and the negation of C?
* Goodstein's theorem is independent from PA. Does that mean there are models of PA where Goodstein's theorem is true and others where it's false?
* If yes to the last question, what on earth do those models of PA where Goodstein's theorem fails look like? (Is this where these "nonstandard models of arithmetic" come into play?) If so, what does a sequence violating Goodstein's theorem actually look like? How can such a sequence fail to end up at 0?