My question is based on this answer by Asaf Karagila. Emphasis mine.
Indeed as a first-order structure, $(\mathbb{R},≤)$ cannot define the operations $+,⋅$ or the constants $0,1$. In fact, even as an ordered group $(\mathbb{R},+,≤)$ cannot define the number 1. These are all simple exercises that can be given after the second week of a first course about model theory.
This passage suggests to me that there should be a reasonably direct way to prove that $1$ is not definable in $(\mathbb{R}, +, \le)$ or the similar structure $(\mathbb{R}, +, 0, \le)$.
I'm curious what the canonical way to prove this fact is. I'm also curious if there's a way to prove this that's "syntactic" rather than "semantic" in nature and doesn't appeal to specific models of the theories in question.
Coming up with an informal argument to prove this is relatively straightforward. Let $M^1$ denote the universe of the first model and $M^i$ denote the first model and so on for $(2, ii), (3, iii), (4, iiii), (5, v) \cdots$. Similarly, let $T^i$ be the first theory. For the purposes of this question, I'll assume that the universe of a model is nonempty.
Let $M^i$ be a model of the theory associated with $(\mathbb{R}, +, \le)$. $0$ is the unique solution to the equation with one free variable $\forall w \mathop. x + w = x$.
Let $M^{ii}$ be the model associated with $(\mathbb{R}, +, 0, \le)$.
I can think of two ways to show the non-first-order definability of $1$. I'm pretty sure that these arguments work.
The first is to note that $M^2$ could be $\{0\}$, since without $1$ we are not guaranteed the existence of a positive element. $1$ is not definable because it is not definable in at least one model of $T^{ii}$, therefore it isn't first-order definable.
The second is to look at the standard model of $T^{ii}$. There is more than one way to extend it to a model of the theory associated with $(\mathbb{R}, +, 0, 1, \le)$. If we pick a non-positive element of $M^2$, then it will satisfy all the multiplication-free sentences that $1$ satisfies in the theory associated with $(\mathbb{R}, +, \cdot, 0, 1, \le)$. Since the choice of $1$ is not unique in at least one model, $1$ is not first-order definable.
The intuitive idea behind these arguments, from my perspective, is to locate specific models where there either a) are no suitable candidates for $1$ or b) is more than suitable candidate for $1$.
However, first-order-definability feels like a syntactic property and it feels like I'm using a hypothesis without stating it by looking at specific models and arguing about the reasonableness of extending them with interpretations of new function symbols.
What's the canonical way to prove this fact? Also, is there a way to prove it that's more directly syntactic?
I don't really understand your proposed approach, so I can't comment on it.
I'm not sure it's "canonical" per se, but in my opinion the most natural way to attack a problem like this is via automorphisms.
One of the most important properties of first-order logic is its isomorphism-invariance (and indeed this is usually taken as one of the criteria for being a "logic" in the first place - in particular, everything that follows holds for second-order logic, infinitary logics, etc.):
We can use this to prove for example that $1$ is not a first-order definable element of the structure $\mathcal{R}=(\mathbb{R};\le,+)$ as follows. Let $f:\mathbb{R}\rightarrow\mathbb{R}:x\mapsto 2x$. This is an automorphism of the structure $\mathcal{R}$ and $f(1)=2$, so by the fact above we get in particular that for each formula $\varphi(x)$ in our language we have $\mathcal{R}\models \varphi(1)\iff\mathcal{R}\models\varphi(2)$. Consequently there is no formula in our language which holds, in $\mathcal{R}$, of exactly the element $1$. And recall that this is what it means for an element to be (un)definable:
Note that this is very semantic, contra your request. This is however part of the definition of the term, and it really only ever makes sense to talk about definability relative to a structure, although unfortunately we do often abuse language. See here for a summary of definability (both with and without parameters).
Now the above approach is extremely "coarse," and - unsurprisingly - doesn't always work. For example, the structure $\mathcal{N}=(\mathbb{N};<)$ has no automorphisms at all (= is rigid), and so we can't use the idea above to rule out any definability results at all, but of course only countably many subsets of $\mathbb{N}$ could possibly be definable in $\mathcal{N}$ (and if you want to think about definable elements rather than relations, consider an uncountable rigid structure like the linear order $(\omega_1;<)$).
For more subtle results we need to use more specific properties of the logic in question. For example, the set $E$ of even numbers is not first-order definable in $\mathcal{N}$ but it is second-order definable in $\mathcal{N}$, so if we want to prove the non-first-order definability of $E$ in $\mathcal{N}$ we'll need to use a fact which is more specific to first-order logic. For example, we have the notion of back-and-forth systems, a kind of "isomorphism analogue" for which first-order logic (but not second-order logic!) satisfies an appropriate invariance principle; these are often presented game-theoretically (as Ehrenfeucht-Fraisse games), and I've written a number of arguments here on MSE using this presentation.
The semantic nature of definability notwithstanding, there is a "definability-flavored" question which is purely syntactic. Suppose I have a theory $T$. I can ask whether there is a formula in the language of $T$ which $T$-provably has some property. For example:
This essentially asks whether Presburger arithmetic can implement a pairing operation. In case you're curious, the answer is negative (and despite being a syntactic question there's a semantic argument for this!).
We could also make allowances for incompleteness in our theory by permitting some casework (I'll talk about unary relations specifically for simplicity). Given a theory $T$ in a language $\Sigma$ and a sentence $\psi$ in the language $\Sigma\sqcup\{U\}$ for some fresh unary relation symbol $U$, say that $T$ almost defines a $\psi$-solution iff there is a finite sequence $\theta_1(x),...,\theta_n(x)$ of $\Sigma$-formulas such that $$T\vdash\bigvee_{1\le i\le n}\forall x(\psi[\theta_i/U]),$$ where $\psi[\theta_i/U]$ is the $\Sigma$-formula gotten by replacing "$U$" with "$\theta_i$" throughout $\psi$. This turns out to be equivalent to every model of $T$ having a parameter-freely-definable set satisfying $\psi$ in the obvious sense (this uses compactness).