Are mathematical theorems entailments, or merely implications? I have a background in Electrical Engineering and not Mathematics. Recently I've been self-studying "Charles Chapman Pugh - Real Mathematical Analysis", and I was reminded of the old question that I've always had in my mind, but to my surprise, I never find (or can't see) this simple question ever being explicitly asked or addressed. I understand that many (if not all) of the theorems I've seen are in the form of implication: $P \implies Q$
What if both $P$ and $Q$ are true, but irrelevant/independent? Consider the following cases:
$P_1$: There are infinitely many prime numbers $\implies$
$Q_1$: The square root of 2 is irrational
$P_2$: The number $\pi$ is transcendental $\implies$
$Q_2$: Pythagorean theorem
I can guess these apparently irrelevant antecedents and consequents could make up for theorems if they are stated in an axiomatic system where all the required axioms are included. But generally speaking, shouldn't a theorem in the form of $P \implies Q$  be something that means we can 'derive' the truth of $Q$ from the truth of $P$ (given the auxiliary facts)? If so, does it mean that theorems are always in the form of entailments, not merely implications? I haven't seen this issue being discussed in the math books I've encountered, although it seems to me that it's an essential component of being a theorem.
Please guide me through, or where I can find the minimum proper terminology to talk about this issue.
Thanks.
 A: Your question is indeed interesting.
A theorem may or may not be in the form of $P \Rightarrow Q$. When it is $P \Rightarrow Q$, $P$ is usually not a tautology (i.e $P$ is not always true), otherwise that would be unuseful to mention $P$. When a $P$ is mentionned, it can be because:

*

*$P$ includes one or more variables which are also used in $Q$, and $P$ is true for some values of the variable, false for others. Such as "a prime number greater than $3$ is odd": here the variable is an integer; when it is a prime number greater than $3$, $Q$ (the number is odd) is true; and in some cases where the number is not a prime number greater than $3$, $Q$ is false.

*$P$ may be a tautology, but then the variability is the set of axioms you choose, and the theorem links some axioms to $Q$. Example, if one writes "the axiom of choice implies that every vector space has a basis", this is to compare situations where $P$ (the axiom is choice) is an axiom (with other axioms needed for the demonstration, that however are not mentioned), with situations where $P$ is not an axiom (but the other axioms are still there).

Obviously, when writing $P \Rightarrow Q$, mathematicians generally omit all the axioms that are used to prove $P \Rightarrow Q$, as well as the set of logical rules. This, depending upon the context, may be more or less sloppy. In some cases it may be mentioned that the theorem is proved in ZF, or ZFC, etc. The fact is, most usual math theorems can be proven in any usual axiom set - just because the usual axiom sets have been chosen so that they enable to prove all the basics.
Similarly, while there was a time when logic would be considered common sense and everybody more or less agreed upon a set of logic rules, logic itself can now be weakened. Cf. substructural logic. These different logic frameworks have notably found interest in computer science, because some CS concepts are in direct correspondance with them. Apart from logic specialists, these different logics are seldom mentioned; however some logic principles are more frequently mentioned, e.g. the law of excluded middle (which some logic theories do not accept) - this is the reason why a proof by contradiction is often considered less desirable than a proof that does not use contradiction.
Quite recently (beginning in the 70's), a systematic exploration of "what axioms are required to prove what" has been launched, called reverse mathematics. The linked Wikipedia page is interesting to read: it shows that some theorems require more axioms than others. For example in the weakest axiomatisation of arithmetics, "a continuous real function on $[0,1]$ is bounded" cannot be proven; nor the Jordan curve theorem (a closed, non-intersecting curve on the plane separates the plane in two regions, its interior and its exterior, that cannot be connected with a continuous path without intersecting the curve).
Your title uses entailment as opposed to implication. I would be embarrassed translating this into french, because both entailment and implication translate into implication. We could use causality in place of entailment, but that would be too strong. The nearest you can approach this idea of entailment, in maths, is to show that $P,Q \Rightarrow R$ (where $P$ and $Q$ represent at least all the axioms and logic rules used to prove $R$), and that $P$ alone does not $\Rightarrow R$. In this situation we could say that $Q$, in the context of $P$, entails $R$.
A: 
I understand that many (if not all) of the theorems I've seen are in
the form of implication: $P \implies Q$
What if both $P$ and $Q$ are true, but irrelevant/independent?

In classical logic anyway, it then seems unavoidable that the implication is true, regardless of the presence or absence of any other logical relationships between propositions $P$ and $Q$.

Using a truth table, we can verify that $(A\land B)\to (A\to B)$ is a tautology, i.e. it is always true:

Source: https://www.erpelstolz.at/gateway/TruthTable.html
Using a form of natural deduction, we can formally prove it from "first principles." (Screenshot from a freeware proof checker)

In a similar way, we can formally prove:
$~~~~~~~~~~(A\land \neg B) \to \neg (A\to B)$
$~~~~~~~~~~(\neg A\land B) \to  (A\to B)$
$~~~~~~~~~~(\neg A\land \neg B) \to  (A\to B)$
In this way, we can formally justify the usual truth table for $A\to B$:

We can also prove what is often given as the "definition" of logical implication:
$~~~~~~~~~~(A\to B)~~ \equiv  ~~\neg(A\land \neg B)$
See here.
