Questions about the fundamental theorem of arithmetic The fundamental theorem of arithmetic states that every positive integer greater than 1 is either a prime or a product of primes. 

First question: why "either a prime or a product of primes", if every prime is in fact a product of primes with one factor? Wouldn't it be simpler to just say that every positive integer greater than 1 can be written as a product of primes?

The fundamental theorem of arithmetic is proved using strong induction. The formal definition of strong induction (in its transfinite version) is: $\forall n [\forall k [k&lt;n \rightarrow P(k)] \rightarrow P(n)] \rightarrow \forall nP(n)$. In this case, $P(x)$ is substituted by "if x>1, then x is prime or x is a product of primes". 

Second question: which are the formal definitions of x is prime and of x is a product of primes? Velleman says that x is not prime is the same of $\exists a\exists b[n=ab \land a&lt;n \land b&lt;n]$. Therefore, I would assume that x is prime would be $\forall a\forall b[n=ab \rightarrow a \geq n \lor b \geq n]$. Is it correct? How about x is a product of primes?

Now, expanding the inductive hypothesis  inside the scope of the natural numbers and excluding the vacuosly true statements, we end up with the following result:

$P(2) \land [P(2) \rightarrow P(3)] \land[P(2)\land P(3) \rightarrow P(4)] \land ... \rightarrow \forall n P(n)$

Third question: how is it possible that if 2 is prime or a product of primes implies that 3 is prime or a product of primes?
There is nothing wrong with the phrasing, even allowing "product of primes" to be understood to include the case of a product with one factor (which most mathematicians allow). Phrasing need not be the shortest possible, nor does the "or" need to be exclusive: the most important thing is that it not be misunderstood. You could just as well phrase the existence part of the Fundamental Theorem of Arithmetic as:


  Every positive integer is a (possibly empty) product of primes. 


Why do we not phrase it that way? In part, for historical reasons. Euclid excluded $1$ (it wasn't a "number"); Gauss phrases the theorem as follows (Disquisitiones Arithmeticae, Section II.16, from the English edition translated by Arthur A. Clarke):


  Theorem. A composite number can be resolved into prime factors in only one way.


thus putting primes themselves on a separate category. Traditionally, people said numbers were either "primes or products of primes", before allowing $1$ to be considered a "number." The idea of having products with one or fewer factors is relative new.

I will note that your phrasing is incomplete: an oft-ignored part of the FTA is the uniqueness of the decomposition (up to order and, in modern parlance, associates). In fact, that's the part that Gauss is concerned with, saying


  "It is clear from elementary considerations that any composite number can be resolved into prime factors, but it is often wrongly taken for granted that this cannot be done in several different ways."


Gauss was the first to prove it explicitly (Euclid only proves it for square-free composite integers).

There are other ways to phrase it; you can specify that the uniqueness is only "up to order of the factors" if you want to make sure people don't think that $21$ can be factored two ways (as $3\times 7$ and as $7\times 3$). You can specify "up to associates" if you suddenly discover that negative numbers exist and that if $p$ is a (positive) prime number, then so is $-p$ (under the divisibility definition). Etc. 

The formal definition of "$x$ is a prime" is

Definition. A (positive) integer $p$ is prime if and only if it is not $0$, not $1$ (or $-1$), and whenever $p$ divides a product $ab$, it divides one of the factors.

This is not the classical definition. Euclid defines a prime as a number (hence greater than $1$) which is divisible only by $1$ and itself; in modern parlance, this would be an irreducible, not a prime (though in the integers, the two concepts coincide). 

"A product of primes" would be harder; you would want to have an operator that takes an arbitrary but finite number of integers and assigns an integer to it (their product). Or you could say that $m$ is a product of primes if 


  there exists a positive integer $n$ [greater than $1$ if you want to exclude the one-factor product] and positive integers $p_1,\ldots,p_n$ such that $p_i$ is prime for each $i$ and $m=p_1p_2\cdots p_n$.


In fact, the inductive step is usually proven as follows:

Assuming that for any $k$, $1\lt k\lt n$, $k$ is either prime or a product of primes, consider $n$. If $n$ is prime, we are done. If $n$ is not prime, then there exist $a,b$, $1\lt a,b\lt n$ such that $n=ab$ (*). Applying the inductive argument to $a$ and $b$....  etc.

Now, (*) is not the definition of prime, but it is an equivalent property to "prime" in the integers.

Theorem. let $m$ be a positive integer, $m&gt;1$. The following are equivalent:


If $m=ab$ with $a,b$ positive integers, then $a=1$ or $b=1$.
If $m=ab$ with $a,b$ positive integers, then $a=m$ or $b=m$.
If $m|ab$ with $a,b$ integers, then $m|a$ or $m|b$.
If $1\leq k\lt m$, $k$ an integer, then $\gcd(k,m)=1$.
For any integer $a$, $\gcd(a,m)=1$ or $\gcd(a,m)=m$. 


And so the argument uses 1 or 2 to guarantee the existence of $a$ and $b$. 

The implication "$2$ is a prime or a product of primes $\Rightarrow$ $3$ is a prime or a product of primes" holds because the consequent is true. For that matter, the implication "$6$ is a prime $\Rightarrow$ $7$ is a prime" is also true... because the consequent is true.
The wording is proper.  A prime (say $7$) is not a product of primes.  Since $1$ is not a prime, $7$ is not a product of primes--that is, one that requires the operation of multiplication.  What product could that possibly be??  (The "empty product" is explicitly not a product.) Taken alone, $7$ is not a product, any more than $28$ is a "product."

Such a weird attempt then makes every number prime: $28 = \prod\limits_{i\in I}$ where $I = \{ 28 \}$.  What an absurdity and mess!!!

Attempts to define a prime by some novel interpretation of product that has no argument, such as $7 = \prod\limits_{i\in I}$ where $I = \{ 7 \}$, have no justification.  The product function must take an argument, and this ad-hoc approach (which I've never seen in 40 years of working in mathematics) requires a redefinition of what a function is...  i.e., something that takes no argument.

From the Dictionary of mathematics:

product: The result of multiplication or any operations on mathematical objects deemed close enough in resemblance to multiplication. (Such as the scalar product and the vector product in vectors.)

The dictionary highlights the key property of "product" which is of course multiplication.  The ad-hoc attempts such as $7 = \prod\limits_{i\in I}$ where $I = \{ 7 \}$, involve no multiplication whatsoever, despite the symbol.  

If you want to re-define prime in this way, you're forced to redefine product (and likely other foundational terms) in weird ways and admit that now every integer can be defined as a prime.

Good luck with that!