The definition of logical implication. Is the following definition correct?
I think it is not.

"A proposition $P_1$ implies another proposition $P_2$ if $P_2$ is true when­ever $P_1$ is true".

Comprehensive Mathematics for Computer Scientists 1 Sets and Numbers, Graphs and Algebra,
Logic and Machines, Linear Geometry (Second Edition)
Thank you!
 A: The definition you give is correct, that is, it is one among several possible (and correct) ways of defining logical implication. (See, e.g., the alternatives listed below.)  I don't think that the use of the word "whenever" is helpful though. It's too connected to the term "when", which carries with it temporal connotations which aren't really appropriate here, even if they were not intended.
So: "$P$ implies $Q$" $\iff$ "$Q$ is true whenever $P$ is true" should be read as saying: "$P$ implies $Q$" $\iff$ "$Q$ is true, if $P$ is true", or better yet: $P\implies Q \iff$ "if $P$ is true, then $Q$ is true." 
Note that this definition is vacuously satisfied (it is vacuously true that the definition holds) if $P$ happens to be false, so if you're bothered by the fact that the definition you posted fails to say explicitly what happens when $P$ is false, please refresh your memory of what it means for a statement to be vacuously true (i.e., in this case, what it means for a definition to be vacuously satisfied).
Another way to state this is "$P\implies Q$ is true if and only if it is not the case that $P$ is true and $Q$ is false.
Yet another way of saying this is $P\implies Q$ is false if and only if $P$ is true, and $Q$ is false.
An explicit definition if $P \implies Q$ can be summarized, of course, in a truth-table:

A: Within a logical system I have no problems with this definition, because within a logical system any tautology (theorem) will imply any other tautology (theorem respectively, even if semantic completeness does not hold).  However, and I speak on the basis of having misunderstood certain metatheoretical ideas before, this definition makes no sense outside of a logical system.  If you used this definition when talking about the independence of axioms you would get nowhere in terms of understanding that idea.  For a system like {1-CCpqCCqrCpr, 2-CCNppp, 3-CpCNpq} (you don't need to understand what these mean here, so long as you assume them as axioms) under substitution and detachment, you would have 1 implying 2, 2 implying 3, and 3 implying 1 which would entail that talk about the independence of axioms would become nonsense.  Consequently, outside of a logical theory, or equivalently when discussing the metatheory of a logical system, this definition either needs modification or use terms like "derivational implication" or "inferential implication".  By those terms I mean that if we keep the rules of a system constant when comparing different propositions or propositional schema, then a proposition A implies proposition B if under the rules of the system, we can prove B using just those rules and A.
And I wouldn't underestimate the methodological importance of at least establishing the independence of axioms.  Part of the reason of the flourishing and development of non-Euclidean geometries as well as new and alternative logical theories, as well as other set theories, and even many different algebraic theories may well come as connected to the problem of establishing or refuting independence of axioms.  Many of the founders of modern logic (such as Gottlob Frege, Bertrand Russell, and David Hilbert) didn't create systems with independent axioms and they may well not have realized that.  It is not necessarily an easy problem to solve by hand.  On top of that, oftentimes when the independence of axioms gets established, you can show such by exhibiting a table or matrix of some sort and indicate that certain calculations can get done which does such.  When people do this, it gives us a way of talking metatheorically in a rather concrete way which often doesn't require sophisticated reasoning or complex ideas like mathematical induction, and probably oftentimes comes as more convincing to empirically oriented people than other metatheortical ideas like semantic completeness.
