TITLE: Prove that sentence is not tautology. Check if contradiction this one has finite model.
QUESTION [0 upvotes]: I am trying to prove that following sentence is not tautology.
$$\phi=(\forall x\forall y((f(x)=f(y))\to(x=y)))\to(\forall x\exists y(f(y)=x))$$  
For me, it is sufficient to show $f:\mathbb{N}\to\mathbb{N}$ such that $f(n)=n+1$. Then $f$ fulfill left side of $\to$, but there is no such $y$ that $f(y)=0$ because $f[\mathbb{N}]=\{1,2,3,...\}$.
I am not sure if I am correct.  
When it comes to second part:
Check if $\neg\phi$ has finite model.
$\neg\phi $ is $(\forall x\forall y((f(x)=f(y))\to(x=y)))\wedge \exists_x\forall_y(f(y)=x)$.
I don't know what does it mean finite model... Moreover, I am not sure about corectness of first part. Can you help me ?

REPLY [0 votes]: The first part is just correct.
What does it mean to have finite model? Well, just to be satisfied in a model which has finite universe (sometimes called "domain"). A model is a structure where a formula can be interpreted - your example of $(\mathbb{N}, S)$ is a model - a structure consisting of set ($\mathbb{N}$) and some relations (in this case a function $S: \mathbb{N} \to \mathbb{N}$). However, this model is not finite, as $\mathbb{N}$ has infinitely many elements.
So basically the question is: can be $\neg \phi$ be true in (you could say: "about" instead of "in") finite structure? You have shown, that it can be true in infinite one.
Below I attach an answer to the second question, however I would recommend you to try to find it out yourself - it is really not hard, and It looks like you just should get familiar with basic definitions.
The answer is negative: note, that the antecedent of $\phi$ just states that $f$ is injective (i.e. does not map two distinct elements to one value). If we take any structure with finite universe, an injective function is a bijection (you can prove this easily, e.g. by induction). So it is not possible that there is an element which is not a value of the function.
{"set_name": "stack_exchange", "score": 0, "question_id": 1975526}