This is a part of exercise $4$ page $38$ in A Friendly Introduction to Mathematical Logic by Leary
Find a structure $M$ for a suitable language $L$ such that $M \not\models (\forall x)(\exists(y)[x<y \rightarrow x+1=y]$
My attempt :
Let $L=[\{1,+,<\}$ be our suitable language where $1$ is a constant symbol , $<$ is a $2$-ary predicate , $+$ is a $2$-ary function . Define $M$ to be a structure whose universe , $A=\{6,7\}$ and $1^{M} = 6 ,\ <^M = \{(7,6)\} ,\ +^M=\{[(x,y),7]:x,y \in A\}$
In other words , the function $+^M$ sends every pair $(x,y)$ in $A\times A$ into $7$.
Let $s:Vars \rightarrow A=\{6,7\}$ be our assignment function where $Vars$ is the set of variables of $L$ and let $s(x)=6 \ \& \ s(v)=7 \ \text{for every}\ v\ne x$
Now , define $h(v)=\underline{s[x|a][y|b]}(v)$
$\text{note that}: \underline{s[x|a][y|b]} \text{ means the Terms assignment function}$
So , $M\models (\forall x)(\exists y)(x<y \rightarrow x+1=y)[s] \equiv \text{for every $a\in A$ there is $b\in A$ s.t. }$ $ $ $M\models (x+1=y)[h] \text{ whenever } M\models (x<y)[h] \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (1)$
Now , I calim that this condition $(1)$ fails when we consider our particular $s$ and $M$ and so we proved the required! to show this :
for $a=7$
notive that:
1- $M\models (x<y)[h] \text{ iff } [h(x),h(y)]\in <^M$. and we have , $[h(x),h(y)]=[a,b]=[7,b]\in <^M \text{ iff } b=6$
2- $M\models (x+1=y)[h] \text{ iff } h(x+1)=h(y) \text{ iff } +^M[h(x),h(1)]=h(y) \text{ iff } +^M(6,6)=b \text{ iff } b=7$
So for $a=7 , \text{ there is no $b\in A$ s.t. }M\models (x+1=y)[h] \text{ whenever } M\models (x<y)[h]$
So it's not true that , $\text{for every $a\in A$ there is $b\in A$ s.t. } M\models (x+1=y)[h] \text{ whenever } M\models (x<y)[h]$
Hence , $M\not\models (\forall x)(\exists y)(x<y \rightarrow x+1=y)[s] \boxtimes$
I wonder if my solution works . I also hope you can provide better structures which makes the gived formula false!
The exercise unfortunately contains a typo, though one which you might perhaps have spotted. Why?
Because whatever the domain, whatever the constant 1 denotes, and whatever function + denotes, $x + 1$ must have a value in the domain , given an assignment of a value to $x$. That's because in standard first order logic, all functions are total. Hence
$$ \forall x\exists y(x + 1 = y)$$
will be true in all models. So, a fortiori, whatever relation < is,
$$ \forall x\exists y[x < y \to x + 1 = y]$$
also has to be true in all models. OK?? So your attempt to describe a model in which it fails must be wrong!
Moral: Always, always, print out the online errata for any logic book, in this case http://www.geneseo.edu/~leary/errata.pdf