It's easy to find satisfiable FOL-Formulas that are satisfiable by countably finite or infinite models. If we have a formula with a countably infinite model, we can prove the existence of an uncountable model for that formula (Upward Löwenheim-Skolem Theorem).
But, to my knowledge (and please correct me if I'm wrong), classical FOL does not give us the tools to formally denote such an uncountable model.
Then, the question arises whether there exist classical FOL formulas that ONLY have uncountable models (no finite or infinite countable ones). My answer would be no, because we always get a model of lesser cardinality due to the Downward Löwenheim-Skolem Theorem.
So my questions:
- Why is it impossible to define uncountable models in FOL? What "tools" would be needed to do that?
- Is my reasoning about the non-existence of FOL-Formulas with only uncountable models correct?
You're right, no such sentence exists: if $\varphi$ is a sentence true in an uncountable structure $\mathcal{M}$, by the downward Lowenheim-Skolem theorem there is a countable $\mathcal{N}\preccurlyeq\mathcal{M}$, and clearly $\mathcal{N}\models\varphi$.
I'm assuming the language is finite, but that's WLOG - the sentence $\varphi$ itself can only use finitely many symbols.
The essential point that makes downward Lowenheim-Skolem work is Skolem functions. Given a structure $\mathcal{M}$, we can consider an expansion $\mathcal{M}^+$ of $\mathcal{M}$ by all the relevant Skolem functions. Now it's easy to see that any substructure of $\mathcal{M}^+$ corresponds to an elementary substructure of $\mathcal{M}$, so we can find a countable elementary substructure of $\mathcal{M}$ just by using the fact that closing a countable starting set under countably many (since there are only countably many sentences in the first place) finite-arity (since formulas only have finitely-many quantifiers) functions results in an at-most-countable set.
What could break this? Well, in second-order logic, witnesses are no longer elements but sets, and so the entire approach breaks down. In infinitary logic meanwhile, we seem to have too many Skolem functions to handle - while a weak downward Lowenheim-Skolem still does wind up holding for individual $\mathcal{L}_{\omega_1\omega}$-sentences, it's harder to prove, and it fails for higher infinitary logics like $\mathcal{L}_{\omega_1\omega_1}$. A third option would be to look for logics where the notion of Skolem function doesn't even make sense in the first place, but I'm not familiar with these.
So that's how you escape downward Lowenheim-Skolem: work in a logic where Skolem functions either $(i)$ are of too high type, $(ii)$ wind up occurring implicitly too many times in a given sentence, or $(iii)$ (hypothetically) don't even make sense in the first place.