Understanding Hoare Logic Axioms
Here are some answers and hints to pursue your reflexions.


$\mathtt{Assignment}$


What $\phi([x \leftarrow E])$ means. You said yourself that the semantic of the precondition confuses you that was what the assignment $x := E$ was doing. But in fact your are precisely pointing out the crux of this rule: it affects the precondition exactly as the assignment would do it. This is the core reason of why this rule is actually sound.



Let study an exemple and leave the abstraction for a bit.
Take the program $P = (z:=x+1)$. 

Suppose we want to prove the postcondition $\phi(z) := \{z=2\}$
Intuitively what do we need to prove this ?  Obviously we need $x$ to be equal to $1$. Let see how it translates in Hoare's logic. The assignment rule tells us that the triple:
$$
\{\phi[z \gets x+1]\} (z:=x+1) \{\phi(z)\}
$$
is valid.

Unrolling the syntax gives:
$$
\{(z=2)[z \gets x+1] \} (z:=x+1) \{x=2\},
$$
that is 
$$
\{x+1 = 2 \} (z:=x+1) \{z=2\},
$$
and a bit of meta-logic says:
$$
\{x = 1 \} (z:=x+1) \{z=2\}.
$$

Which is what you wanted.

In an nutshell the assignment intuitively says: "The postcondition is true as soon as when I replace everything by the value of E in it, it is true"

$\mathtt{Conditionals}$

First of all $B$ is not a variable but a boolean predicate (like $X==1$ for instance).


$\{\phi[B]\}\ P_1\ \{\psi\}$ doesn't make any sense. $\phi$ is a predicate, so does $B$, so that you can't apply one to another.
For instance if $\phi = (x==1), B = (y==2)$ you can speak of $\phi\wedge B$ but $\phi[B] has absolutely no meaning.
$\{\phi \land B\}$ is true says $\phi$ is true and $B$ is true.
With my previous instances:  $\{\phi \land B\}$ as precondition asserts that on the one hand $(x==1)$, and on the other $(y==2)$. Nothing else.


$\mathtt{Iteration}$
 This one is subtle. As long as it terminates, you can have arbitrary many iterations BUT still a finite number. Think of a while as a for loop on which you don't know a priori the number of runs in this case. To see why the rule is sound, think of it as a nested sequence of if :

if B then 
     P
     if B then 
         if B then 
            P
            if B then
                 .....


And use a recurrence + conditional+ composition to convince you that the rule does what it is supposed to do.

If it doesn't terminates you can't say anything a priori so it doesn't matter. Remark that the rule DOES NOT say that the loop terminates.

$\mathtt{Weakening \to Strengthening}$
  It is the causal reasoning. Let us unroll the rule: Suppose that $\phi$ is true. Then $\phi$ is also true since  $\phi \Rightarrow \phi_1$. But the Hoare triple
$\{\phi_1\}\ P_1\ \{\psi_1\}$ is valid by hypothesis. Then $\psi_1$ is true. But we know that $\psi_1\Rightarrow \psi$. Hence $\psi$ is true as well: we just proved that $\{ \phi \} P \{\psi\}$ is a valid triple.