Give a signature to express an strict lineal order on a set and show that the minimal element is the minimum.
What I've done is set our signature as $\Sigma = \{ A, <\mid_2, a \}$, where $A$ is the set we'll be working with, $<$ is a $2$-arity predicate and $a$ is a constant representing the minimal element of $A$. Then the axioms of a strict order (antireflective and transitivity) would read as follows: $$\forall x \forall y \forall x ((x < y) \land (y < z) \rightarrow (x<z))$$ and $$\forall x \neg (x < x)$$ Now I want to formalize that each two distinct elements can be compared. I have set that property as $$\forall x \forall y ((x<y) \lor (y<x))$$ I had some doubts regarding this last one since I didn't not mention at all that $x$ and $y$ are not equal, but that case is excluded from the fact that $<$ is antireflective and hence, we cannot have $x < x$ on the first place. Finally, I want to express that $a$ is minimal, that is, there is no element smaller than $a$, which reads as $$\forall x \neg(x<a)$$ And finally, to prove that $a$ is the minimum of the set, I would write that as follows $$\forall x (a < x)$$ Now, in order to prove the assertion, negate the conclusion, that is, $\neg \forall x (a <x)$. From that I can say that $\neg (a<b)$ from some $b$. Now, since $\forall x \neg(x < a)$ I can say that $\neg (b <a)$ for some $b$. Now, I can compare $a$ and $b$ and we must have that $a <b$, which contradicts $\neg (a <b)$, or $b < a$, which contradicts $\neg (b < a)$. Then, the set of all premises along with the conclusion negated is unsatisfiable, an hence, the minimal element is the minimum, as desired.
Is this proof okay? Thank you in advance!
You're right to doubt $\forall x\forall y(x<y\lor y<x)$. In first-order logic there's nothing that prevents two nested quantifiers from being instantiated to the same element of the domain, so that axiom would be demanding, among other things, that $c<c\lor c<c$. So your theory is inconsistent.
In order to complete your task here, you need a way to speak about equality of elements. In some developments of first-order logic, $=$ is actually considered a part of the logic, with automatic rules to go with it, and in that case you can just write $$\forall x\forall y(x<y\lor y<x \lor x=y)$$
Otherwise you need manufacture a $=$ yourself. In that case you cannot actually get all the way to having your theory speak about "a strict linear order on a set", but need to make do with having a theory that describes a strict linear order on equivalence classes of indistinguishable elements of the universe. But in practice that is often considered good enough -- you can derive all the same theorems under that interpretation, for example.
Your options are then basically either
Add a $=$ symbol to your signature, and provide axioms that force it to behaves like equality ought to behave -- in particular, enough to guarantee that $=$ is an equivalence relation, and let us derive $\phi(x)$ from $x=y$ and $\phi(y)$ for all formulas $\phi(\cdots)$.
Declare that $x=y$ is an abbreviation for $\neg(x<y \lor y<x)$ and again provide axioms that guarantee this will actually behave like equality.