Using logical implication to analyse mathematics I've read the answers here and here, and have the following view. Please correct me any misunderstandings.

*

*In a truth table, each row (truth value assignment) corresponds to an 'interpretation'.


*A compound statement is called a tautology when it is true under all interpretations.


*Let $P \models Q$ stand strictly for purely logical implication. We say that $P$ logically implies $Q$ when in all those interpretations/rows where $P$ is true, $Q$ is also true. For example, $(P \land Q) \models (P \lor Q).$
Clearly, if $P \models Q,$ then $P \to Q$ is always true under all interpretations, i.e., it will be a tautology, because in every interpretation where $P$ is true, $Q$ is also true, and therefore we don't have the case of $P$ true and $Q$ false.


*Let $P {\implies} Q$ stand strictly for mathematical implication. When we say that $P {\implies} Q,$ we are saying that given our mathematics axioms and definitions, if $P=1,$ then $Q=1.$
Now, $(P,Q)=(1,1)$ is just one row out of many rows in the truth table for the statement $P\to Q,$ so corresponds to one of many possible interpretations. In this one interpretation, we can say that $P \to Q$ is true, since both components are. $P {\implies} Q$ applies only to this particular interpretation/row that our mathematics system has yielded us; we have not said anything about the truth value of $P \to Q$ under any other interpretation in the truth table.
It could be that there is some other interpretation of $P$ and $Q$ where $P \to Q$ is false, for example, if $P=1,Q=0.$ The other interpretations could evaluate $P$ and $Q$ differently than our math axioms and definitions, and assign different combination of truth values to them (by evaluating their component statements differently). Still, in mathematical implication, all that we have is just one interpretation.
And this means that in general, $P {\implies} Q$ (mathematical implication) is not a tautology, because we have only one interpretation to talk of in mathematical implication, and to claim that $P {\implies} Q$ is a tautology is to assert that we know $P \to Q$ to be true under all interpretations, which we don't.
 A: 
in mathematical implication, all that we have is just one interpretation.

There is actually no single ‘interpretation’ in mathematics; I will elaborate further down.

*

*

When we say that $P {\implies} Q,$ we are saying that  if $P=1,$ then $Q=1.$



*

$(P,Q)=(1,1)$ is just one row out of many rows in the truth table



*

$P {\implies} Q$ applies only to this particular interpretation/row

Sentence #2 is inaccurate: $(P,Q)=(1,1)$ generally corresponds to multiple rows of $(P{\implies}Q)$'s truth table, because $P$ and $Q$ are generally compound statements.
Moreover, $(P {\implies} Q)$ corresponds not just to $(P,Q)=(1,1),$ but also to $(P,Q)=(0,0)$ and $(0,1).$ (So, sentence #3 is wrong and contradicts sentence #1.)
Everything else that you've written in this new answer is technically correct. However, these comments from that second link are pertinent:


@medium_o The book that you are using is dealing with propositional logic (no “for each” and “there exists”), whereas mathematical reasoning is pretty much predicate logic (full of “for each” and “there exists”). For example, in mathematics, $\Big(P(x){\implies}Q(x)\Big)$ generally actually means $\forall x\Big(P(x){\implies}Q(x)\Big).$ I suggest keeping propositional logic and mathematics in separate compartments for the time being.




@medium_o  "Can we have a simple example of a mathematical $P{\implies}Q$ whose truth table I could verify simply myself as not being a tautology" $\quad$ Truth tables are not really applicable when doing mathematics, for example, $\text“\sin^2 x +\cos^2 x=1\text”$ is universally true but not a tautology, as its skeletal form is just $P,$ and its truth table only has 2 rows, the 1st True while the 2nd False.


In mathematics, when we write $$|x|=3 \implies x=\pm3,\tag1$$ what we actually mean is “for each number $x,\;|x|=3 \implies x=\pm3\text”$ or, symbolically, $$\forall x\;\big(|x|=3 \implies x=\pm3\big).\tag2$$ In predicate logic, we can symbolise this sentence (i.e., proposition) as $$\forall x\;\big(A(x)\to B(x)\big).\tag3$$ Now, $A(x)$ is true if $x=3i,$ but false is $x=2.$ But since a sentence is either true or false, $A(x)$ is not a sentence. Neither is $B(x).$ Neither is $(1).$ They are called predicates (i.e., propositional functions).
However, $(2)$ is a sentence. In real analysis (interpretation #1), it is certainly true; in complex analysis (interpretation #2), it is certainly false.
If one insists on constructing truth tables (even though we have already chosen one interpretation and aren't at all investigating tautological truth), then sentence $(2)$ can be symbolised simply as $P.$ Its truth table has $2$ rows, and reveals that it is not a tautology. This is not surprising, because mathematical theorems are not self-evident truths, which is basically what tautologies are.
Propositional logic is not equipped to handle mathematics.
A: Disclaimer: I am not a real logician and probably a bit naive. But I tried my best to help you. Logic and foundations are subtle, much more so than a truth table! The essence of my post is just, that you should program a little bit in Lean to truly understand how logic works. Here is a book and here is an online editor. Have fun!! :)
The first part of my post is all about syntax. I.e. I will describe how the implication arrow works in formal logic. In formal logic you manipulate strings of symbols according to some preformulated rules. But I will motivate the rules through their intended semantic though. In the second part I will speak about truth tables.
I believe the best way to understand the implication arrow is to understand its introduction and elimination rules in formal logic. Truth tables are a particularly bad at explaining the meaning of implication, and I remember that I was really confused in my first semesters too. The reason why truth tables are so bad is, that intutively the meaning of $\varphi \to \phi$ is that we have a method of converting evidence for $\varphi$ into evidence that $\phi$ is true. In order to prove $\varphi \to \phi$ you start with an arbitrary proof $\varphi$ and construct from it (together with the other axioms and rules of your formal or informal logical system) a proof of $\phi$. In particular this means that $\varphi$ and $\phi$ are in some way related.
There is a formal system for mathematics, called the calulus of inductive constructions, which nicely captures this feature of implication in informal mathematics. You can try it out by programming a little bit in a proof assistant like Lean or Coq. There is even an online editor for Lean and there is the introductory book Theorem proving in Lean. I will try to explain the main idea.
When you are doing mathematics, you often are in the situation that you have some variables from which you know of which kind there are. For example when you try to prove that $\forall n:\mathbb N, \forall m: \mathbb N, n + m \geq n$ you will start like this: "Assume $n$ and $m$ are any two natural numbers. Then...". And in the "Then..." part you will just assume that $n$ and $m$ are indeed natural numbers and work with them accordingly. To capture this feature of ordinary mathematics the calculus of construction has the concept of a context. In a context you put the things that you assume at a given point in your proof. This includes assumptions such as: "Assume I am given an arbitrary proof $p$ of $\varphi$". With this it should be possible for you to understand the rules for implication in the calculus of constructions. Logicians (by which I mean type theorists) write $M:\varphi$ to mean that $M$ is a proof of $\varphi$.

*

*First the implication introduction rule. To prove $\varphi \to \phi$ you need to start with an arbitrary proof $p:\varphi$ and produce from it some proof term $Q:\phi$. You may have some other variables floating around, so we write $\Gamma$ for an arbitrary additional list of variable declarations. The rule now goes is follows. Whenever you where able to derive that $\Gamma, p: \varphi \vdash Q: \phi$ then you may also conclude that $\Gamma \vdash \lambda p.Q : \varphi \to \phi$. It is important to note that $p$ is a symbol which stands in for an arbitrary proof of $\varphi$. It is a placeholder in the more complicated expression $Q$ waiting to be replaced by an actual concrete proof of $\varphi$. This means $p$ must be a variable! The little $\lambda$ is just a way to denote that $p$ is now bounded in the expression. When you happen to get an actual proof $P: \varphi$, then you get a valid proof of $\phi$ by replacing all occurences of the placeholder $p$ in the proof $Q$ by the proof $P$. Logicians will denote the resulting string by $Q[P/p]$.


*The elimination rule is easier. It states that if you have $\Gamma \vdash M:\varphi \to \phi$ and if you have additionally $\Gamma\vdash N: \varphi$ then you should be able to get a proof of $\phi$ in the context $\Gamma$. This is denoted by $\Gamma \vdash M\,N:\phi$. In logic the rule is often called modus ponens.
If this is to complicated, then you can also work proof irrelevant. Look for a Gentzen style natural deduction system online. This will explain you much better why the rules of logic are what they are than any truth table can.
For any real example you need to know many rules of logic, and not just one. Let me try it anyway. You can ignore the following example if it confuses you. I just want to give a taste of how a formal deductive system could operate.
Assume you have a symbol $\mathbb N$ which you want to stand for the natural numbers and you have also symbols which represent zero, addition, the successor function, etc.. Assume you want to prove something about the natural numbers. The way you always start is introducing your symbols and formulating axioms. For example you can do something like this in my made up formal language.
declare N : Set
declare 0 : N
declare S : N → N

Next we need some axioms. Those should be sentences whose interpretation we believe to be true for the natural numbers. Remember that we will interpret $0$ as zero and $S$ as the successor function which adds $1$ to numbers. Here is a reasonable axioms:
declare ax1 : ∀n:N, ∀m:N, (S n = S m) → n = m

How can we now use it to prove another statement such as the one below?
  ⊢ ? : ∀n:N,∀m:N,S(S n) = S (S m) → n = m 

The $\mathtt{?}$ symbol indicates a proof of the proposition which we do not yet know. We like the statement to be true without assumptions, that is in an empty context. This is the reason why the space to the left of the $\vdash$ symbol is empty. Well, clearly we should assume that we have two numbers and a proof of the statement and see what we can do. That is we need to solve the following problem.
 n : N, m : N, p : S(S n) = S(S m) ⊢ ?? : n = m 

Well, we have our axiom, so the judgement below is valid.
 ⊢ ax1 : ∀a:N, ∀b:N, S a = S b → a = b

Now we have to use another rule of logic wich I haven't told you about. If we have a proof of some $\mathtt{\forall}$ quantified statement, than we may specialize it to instances of what is quantified over. All this to say that the following sequents are valid.
n : N, m : N ⊢ ax1 (S n) (S m) : S (S n) = S (S m) → S n = S m
n : N, m : N ⊢ ax1 n m : S n = S m → n = m

We can weaken the context, which is another logical rule. We get that the following sequents are valid.
n : N, m : N, p : S(S n) = S(S m) ⊢ ax1 (S n) (S m) : S (S n) = S (S m) → S n = S m
n : N, m : N, p : S(S n) = S(S m) ⊢ ax1 n m : S n = S m → n = m

Weakening just means that we add assumptions which are not necessary to derive a consequence. Now we may use the implication elimination rule for the first time. We can derive that
n : N, m : N, p : S(S n) = S(S m) ⊢ (ax1 (S n) (S m)) p : S n = S m

and using it again we finally get
n : N, m : N, p : S(S n) = S(S m) ⊢ (ax1 n m) ((ax1 (S n) (S m)) p) : n = m

Now the final step is of course an implication introduction. We have
n : N, m : N ⊢ λp . (ax1 n m) ((ax1 (S n) (S m)) p) : S(S n) = S(S m) → n = m

Now in a final final step we would use the introduction rule for the forall quantifier, but we do not need to do that now. What I want to get accross is that logic is divided into two parts. There is a formal system where you write down symbols and specify a collection of strings of symbols which you considere to be well formed propositions and predicates (predicates are propositions which have free variables). Then there is a deductive system which tells you which propositions are provable from the axioms.
The second part of logic is semantic. You like to have a model in which you can give meaning to the formal symbols and strings of such of your language. In our example, the model are natural numbers $\mathbb N$. It does not really matter if you define them in a wider context of set theory, or if you just imagine them in your head. THe only thing that is important is that you are able to translate propositions of the formal language into statements about your imagined model, and that you are convinced that the interpretation of the axioms are true in the model and that the logic is sound with respect to your model. Logicians write $\mathbb N \vDash \phi$ as a shorthand for the believe that the interpretation of the string $\phi$ is a true statement about the model $\mathbb N$. For example the translation of the axiom $\mathtt{\forall n:N, \forall m:N, (S n = S m \to n = m)}$ into our mental model of the natural numbers is the statement that the successor function is injective. This is something we believe to be true, and thus we write:
\begin{align}
\mathbb N \vDash \mathtt{\forall n:N, \forall m:N, (S n = S m \to n = m)}
\end{align}
But what does it mean exactly that the successor function is injective. Well it means that for all natural numbers $n$ and $m$ if $Sn = Sm$ then $n = m$. But this does not really explain implication, does it? We have just replaced the symbol $\to$ by the word then in our model. Some think a solution to this problem is to assign "truth" values to the predicates and compute the truth value of the composte predicates by means of truth tables. But the reality is that, while it works well for propositional calculus without quantifiers (because there everything is computable and if something is provable or not can be decided by an algorithm) it doesn't make much sense as soon as infinite domains and quantifiers enter the game. You do need to have an a priori notion of what the logical connectives mean in your head, there is no way aroud it. Explaining $\forall n:N, \phi(n)$ by stating it means that for all $n$ the proposition $\phi(n)$ holds is not much more than a translation and only makes sense if the language construct "for all n something is true" makes sense for you. For me the essence of implication lies in its introduction and elimination rules. For me $\phi \to \psi$ means that if you come around with a way to validate $\phi$, then I will be able to convince you that $\psi$ is also a thing. For some other people $\phi \to \psi$ is equivalent to $\psi \vee \neg \phi$ and it means that $\psi$ is true or $\neg \phi$ is false. The last thing I want to emphazise is that $\phi \to \psi$ and $\psi \vee \neg \phi$ are not equivalent in intuitionistic logic, and in consequence truth table semantic doesn't really work there. This is in my opinion in accordance with the intuition of many people. Students are always very confused when $\phi \to \psi$ is explained via truth tables (much more so than they are when the same is done for the logical connectives $\vee$ and $\wedge$), and I believe that the reason is not that the intuition of many people is wrong, but that classical mathematics falsely identifies $\phi\to \psi$ with $\psi \vee \neg \phi$.
