Noncontradiction behind the uniqueness proof and proof by mathematical induction

Question

I'm walking through equivalences, as it appears, between $$\exists!x:P(x)\,\,{\overset{\mathrm{?}}{\equiv}}\,\,\exists x:P(x)\wedge(P(x_1)\wedge P(x_2)\rightarrow x_1=x_2),$$ where I am not sure what binds the variables $x_1$ and $x_2$ in the consequent, and $$\forall n:P(n)\,\,{\overset{\mathrm{?}}{\equiv}}\,\,P(1)\wedge(P(n)\rightarrow P(n+1)).$$

What raises question with regard to the formulae above is that we prove the existence of a concrete $x$ in the uniqueness proof to then derive from that the conjunction which apparently must hold for arbitrary $x_1$ and $x_2$. If this is correct, how can "one or more" imply "for all"?

And then the induction in which we do nothing too much different, with first proving $\exists k:P(k)$ for a concrete base $k$ from which we assume $P(n)$. But that only means that $n$ may be that very $k$ and possibly $x_1=x_2=x$ above or some other element of the domain of discourse. So is there supposed to be an $\exists n$ or an $\forall n$ before this antecedent $P(n)$? If it's $\forall$, then we again conclude from $\exists$ to $\forall$ which I can't explain. And otherwise we can't prove $\forall n:P(n)$

I've encountered these formulae actually mostly without any quantifiers before the free variables.

And as you may have noticed, I'm also not sure whether an equivalence holds in the formulae. Please let me also know whether my formalization of the proof techniques feels or is wrong.

Answer 1

FIRST How can we formalize "there is exactly one thing which is $P$" in first-order logic with identity? This will obviously do the trick:

$\exists x(Px \land \forall y(Py \to y = x))$

Something is $P$, and whatever is $P$ has to be that thing. Or we can do the formalisation as two conjoined clauses.

$(\exists xPx \land \forall x\forall y((Px \land Py) \to x = y))$

At least one thing is $P$ and at most one thing is $P$. Either will do as a definition of $\exists!xPx$. Exercise: prove these two wffs are equivalent in your favourite system of FOL!

Sidenote: in some but not all syntaxes, the second wff is equivalent to

$\forall x\forall y(\exists xPx \land ((Px \land Py) \to x = y))$

but that tangling of variables is often banned.

SECOND The second displayed formula in the original question was nonsense. If you are trying to define the bounded quantifier $(\forall n \geq k)$, what you want is:

$ (\forall n \geq k)\varphi(n) =_{def} \forall n(n \geq k \to \varphi(n))$

No existential quantifier is involved.

[ADDED] The new second displayed formula is ill-constructed. What is true in arithmetic is

$\forall nPn \leftrightarrow P1 \land \forall n(Pn \to P(n+1))$

with the left-to-right conditional trivially true, and the right-to-left conditional the induction principle. But note the placement of the quantifiers. NB though it would be a bad confusion to assimilate this with the first formula. The first originally displayed formula is a [fumbled] definition, this new one is a theorem of arithmetic.

THIRD The remarks about induction seem muddled. Induction from $1$ up involves starting from the $P1$ and the universal claim $\forall n(Pn \to P(n+1))$ and deducing $\forall n\,Pn$. [Induction from $k$ up involves starting from the $Pk$ and the universal claim $(\forall n \geq k)(Pn \to P(n+1))$ and deducing $(\forall n \geq k)Pn$.] That's deducing a universal conclusion from (inter alia) a universal premiss: so no problem!