Is there a non standard model of Peano arithmetic that has a definable non standard point? My first attempt is to consider theory $PA+\neg con(PA)$, and its countable model (say $\mathcal M$). So we can define a subset of non-standard points in $\mathcal M$. But it didn't quite answer the question, I need to find one unique non-standard point to be defined.
Another similar question is: Is there a non-standard model of Peano arithmetic that has no definable non-standard points. I wonder if the constructions of these two models are somehow related.
 A: Below, "definable" means "parameter-freely definable."
Your second question is easier to answer: if $M$ is a nonstandard model of true arithmetic $\mathsf{TA}$, then the definable elements of $M$ are exactly the standard elements of $M$. This is a good exercise (you'll want to use the fact that every standard natural is definable, and "reflect" between $M$ and $\mathbb{N}$ a couple times). (It may be easier to solve this by first proving "If $M\models\exists x\varphi(x)$, then there is a standard element $m\in M$ such that $M\models\varphi(m)$.")
Meanwhile, the answer to your first question is yes, and you are in fact very close to a proof - you just need to apply induction! Specifically, remember that the induction scheme is equivalent to the well-ordering scheme saying that every nonempty definable set has a minimal element (if you haven't seen this before it's a good exercise). Suppose $M\models\mathsf{PA+\neg Con(PA)}$. In $M$, let $X$ be the set of codes for $\mathsf{PA}$-proofs of $0=1$. $X$ is nonempty by assumption and definable a la Godel so by induction $X$ has a least element $c$, and this $c$ is definable as "The smallest code for a $\mathsf{PA}$-proof of $0=1$."
The two paragraphs above are related as follows. If $M$ is a nonstandard model of $\mathsf{PA}$, let $D_M$ be the set of parameter-freely-definable elements of $M$. Induction guarantees that $D_M\preccurlyeq M$, so every element of $D_M$ is definable in $D_M$ (that is, $D_M$ is pointwise-definable). Note that $\mathbb{N}$ is pointwise-definable, and $D_M$ is nonstandard iff $M$ is not a model of true arithmetic $\mathsf{TA}$. Moreover, it's a good exercise to check that $D_M\cong D_N$ whenever $M\equiv N$, so we get a canonical bijection between completions of $\mathsf{PA}$ and isomorphism types of pointwise-definable models of $\mathsf{PA}$.
