This question is an additional question for my previous question,one week ago.
Link : understanding provability
Fortunately, some persons kindly commented for my question. However, I think I still be in confusion.
I modified previous question like this.
There are two sentences sort-of-says.
P: "X is provable" ∧ "Q is provable"
Q: P is provable
(1) for direction ->
If P is provable → (X is provable" ∧ "Q is provable) is provable → (Q is provable) is provable → Q is provable
P is provable → Q is provable, regardless of X
(2) for direction <-
IF Q is provable → (P is provable) is provable → P is provable
Q is provable → P is provable, regardless of X
Therefore,
P is provable <-> Q is provable regardless of X
By this result, can I say one of these?
1) P is equivalent with Q regardless of X
or
2) P is a statement of "P is provable", regardless of X
or
3) P is a statement sort-of-says, "I am provable" regardless of X
Surely, my reasoning has an error. Because Löb's theorem says that the sentence of "I am provable is provable. It means P is always provable regardless of X. It is contradiction.
What is my error?
For one week ago's question, a person commented to me that direction <- has an error. But I cannot understand yet exactly what is the error.
Let's work with PA here for simplicity. What I say here is true for ZFC and other systems as well.
Keep in mind that "P is provable" is shorthand for "there exists x such that x codes a proof of P". Now if $PA\vdash$"there exists x such that x codes a proof of P", then also $\mathbb{N}\models$"there exists x such that x codes a proof of P", since $\mathbb{N}\models PA$, so there is some standard x coding a proof of P. This x can be translated into a really proof (of finite length) of P in PA, and we can conclude that $PA\vdash P$.
Now let's look at your argument. You assume P, conclude that Q is provable, and from this conclude Q. That is,
$PA + P \vdash$"there exists x such that x codes a proof of Q".
Can we conclude that $PA + P\vdash Q$? Not necessarily! It may be that $\mathbb{N}$ is NOT a model of $PA + P$. In fact, this is the case if $X$ is a statement which is false in $\mathbb{N}$. Then $PA + P\vdash$"there exists x such that x codes a proof of P" means that every model of $PA + P$ (if this theory is even consistent) has an element which codes a "proof" (from the perspective of this model) of P. But if this element is a nonstandard element, then this "proof" won't translate to a real finite proof.