Is there a logical system capturing these subtleties about implication? I am teaching an introduction to proof course.  The truth table for implication is always extremely difficult for students to understand.  It feels, to me, that the truth table is an imperfect reflection of the true meaning of implication.
We want $p \implies q$ to be true if and only if we can start with $p$ as a hypothesis and deduce $q$ as a conclusion using a valid argument.  If no such valid argument exists, then we want $p \implies q$ to be false.
Clearly if $p$ is a true statement and $q$ is a false statement, then there can be no valid argument which presumes $p$ and deduces $q$.  This row of the truth table is clear.
Each other row is less clear.
We can invent examples
$F \implies F$:  Let $p$ be the statement that $2<1$ and $q$ be the statement that $3<2$.  If we presume $2<1$, then by adding one to both sides we may conclude that $3<2$.  Clearly a false premise can lead us (via a valid argument) to a false conclusion.
$F \implies T$:  Let $p$ be the statement that $2<1$ and let $q$ be the statement that $0<1$.  If we presume that $2<1$, then since $0<2$ it follows by transitivity that $0<1$.  This is a valid argument starting with a false statement and deriving a true statement.  A false premise can lead us, via a valid argument, to a true conclusion "by accident".
$T \implies T$:  If $p$ is the statement that $1<2$ and $q$ is the statement that $2<3$, then we can presume $p$ and deduce $q$ by adding one to both sides of the inequality.
However, there are other cases where it is less clear.  A famous one is "If 1+1 = 1, then I am the pope".  Although Bertrand Russell had a clever reply to this one, it really isn't clear that a valid argument can start with the premise $1+1=1$ and conclude with "I am the pope".  Absent actually producing such an argument, it seems that the validity of $(F \implies T) = T$ is in jeopardy here.
Is there a system of logic which captures these subtleties?
I am imagining a system in which arguments are "first class objects" which we can quantify over.  An argument can be judged valid or invalid.  In such a system we might define $(p \implies q) := \exists A \in \textrm{Arguments}(p,q): \textrm{valid}(A)$.
 A: Couple of comments:

*

*In the first paragraph you talk about a truth-table for implication, and so you must be talking about the truth-functional operator called material implication ... However, in the second paragraph you talk about the validity of arguments, and so there you are talking about logical implication.  Please note that, while intimately connected, these are different notions: the material implication is a truth-functional operator, and it is a symbol with which you can create formal logic statements. Logical implication, on the other hand, is about logic statements. It does not have a truth-table, since it is not a truth-functional connective.


*Now, the rest of your post seems to indicate that you are really concerned about the truth-table for the material implication, so let's focus on that. OK, so the meaning of the material implication is closest to what we would consider an 'if ... then ...' statement, and indeed we will often use the material implication to capture these English conditionals.  But yes, this never seems to be quite a perfect match. Indeed, see The Paradox of Material Implication for further discussion to what extent the material conditional captures English 'if ... then ..' statements ... and whether the English conditional is even a truth-functional connective itself.


*OK, so what to do?  We could try and use a different logic system, e.g. a system where $F \to F$, $F \to T$, and $T \to T$ are said to be unknown. I am not sure if you really want to go there with your students in an introductory logic course though. But, if you want to stick to good old classic truth-functional logic, and need to convince our students why the truth-table for the material implication is defined as it is, see here and here.
A: Your introductory paragraph

I am teaching an introduction to proof course. The truth table for
implication is always extremely difficult for students to understand.
It feels, to me, that the truth table is an imperfect reflection of
the true meaning of implication.

suggests that what you want you are really interested in is teaching your students how to read and write mathematical proofs.
I agree that the truth table for implication is indeed confusing. I think that starting a "proofs" course with formal logic makes it very hard to teach what matters: mastering abstraction by learning how precise definitions capture concepts that you are already familiar with in an informal way, and how to "prove" theorems starting from those axiom.
In my courses I try to tell my students that a proof is an argument that convinces me that they have convinced themselves of some assertion with good reasons. (I don't need to be convinced since I know a proof. They may not think they need a proof for something they find "obvious". So they have to tell my why it's obvious.) Proofs should be written in English, with as few formal logical symbols as possible.
So my answer to your question about teaching proofs by finding a formal system that better matches intuition than do truth tables is "don't".
Good luck.
A: This runs into some very subtle logical problems.
First of all, for any statement $P$, we can consider the statement $\top \implies P$ ($\top$ being the logical symbol for "true").
If we want $\top \implies P$ and $P$ to be logically equivalent, then we see that $P$ is true exactly when $\top \implies P$ is true, which is in turn true exactly when $P$ is provable from premise $\top$, which is in turn true exactly when $P$ is provable.
So in your theory, a statement should be true if and only if it is provable.
However, if you're using any kind of "nice theory" as a foundation, you have run straight into Tarski's Theorem on the Undefinability of Truth.
So clearly we cannot use the ordinary rules of logic (or even constructive logic).
I think your arguments about a false statement implying any statement display a misunderstanding of what falsity actually means. A false statement can be understood as a statement $P$ such that for all statements $Q$, $P \implies Q$.
In the theory of Peano Arithmetic, it turns out that for any statement $P$, one can show that $0 = 1 \implies P$. One can do this without even permitting negation to be used in logic at all. So if "I am the pope" can be stated at all in Heyting arithmetic, it can be proved from the premise $0 = 1$.
In set theory, if one wished to get rid of negation, one could simply pick the statement $\forall x \forall y (x \in y)$ to stand in for "false". This is because for any statement $P$, one can show $[\forall x \forall y (x \in y)] \implies P$.
Once one has a "falsy" statement (a statement which implies all other statements), label this statement as $\bot$. Then automatically has the rule $\bot \implies P$ for all $P$, since this is part of the definition of a "falsy" statement. And one can then define $\neg P$ to mean $P \implies \bot$.
This procedure then gives the full theory including negation.
A: There are quite a lot of such logics, to the point that I think it's difficult to make a self-contained answer, but I think it's worth mentioning one particular topic: while intuitionistic logic is often the first mentioned in a context like this, I think it's worthwhile to focus instead on the less-common relevance logic(s). Very roughly, in relevance logic we want to require some actual meaningful connection between hypothesis and conclusion, and in my opinion this ultimately winds up being even more extreme than inutitionism's rejection of the excluded middle. In general, there is a "resource sensitivity" present in relevance logic which isn't present in intuitionistic logic and which seems well-suited to capturing the sorts of issues you raise.
(For what it's worth, my own foundational interest in relevance logic is rather limited but a rare positive note is provided by the difficulty of adequately treating Curry's paradox.)
The SEP article is a decent introduction to the topic (and as usual has a very rich bibliography); additionally, if you don't mind the weight I strongly recommend perusing the implication-related sections of Humberstone's epic tome The Connectives.

Of course, leaping all the way to relevance logic is a bit extreme, and there are other things one could do instead. For example, I quite like modal logic(s), which let us distinguish between "$A\rightarrow B$" and "$A\rightarrow B$ necessarily," the latter of which can bring in a lot of nuance (and this is reflected in the relative complexity of the semantics of modal logics as opposed to classical logic). But relevance logic is in my opinion less well-known than it should be, so I've erred on the side of emphasizing it here.
A: Classical logic and material implication are truly up to the job. When students understand some of the basic methods of proof (e.g. proof by contradiction, etc.) they should be able to understand a derivation of each line of the truth table using a simplified form of natural deduction. See my blog posting on this topic. Here is a formal proof deriving the lines 3-4 (the source of the supposed controversy  where the antecedent in false):
Some may protest that material implication drops the ball when the antecedent is false. How, they ask, can an implication be true if the antecedent is false? This is certainly not the case in natural language, they argue. But why not? In daily discourse, when the antecedent is false, little thought is usually given the truth value of the implication itself. In this case, however, the implication cannot in either case be used to infer anything about the consequent. AFAICT no inconsistency would arise by having the implication being true in this case. And it would be consistent with classical logic. (See links above.)
A: The truth-table definition of classical implication is indeed counter-intuitive.
One thing you could do is pick a three-valued logic and ask the students to come up with and defend a particular truth table for $\to$ in this three-valued logic as an exercise.
For example, you could start with the logic of paradox, so both $t$ and $b$ are designated truth values and consider possible truth tables for a new connective $\to$.

One way you can motivate it is by looking at two inference rules that you want, implication introduction and modus ponens.
$$ \frac{A}{B \to A} \;\; \text{is implication introduction} $$
$$ \frac{A \;\;\text{and}\;\; A \to B}{B} \;\; \text{is modus ponens} $$
There are two binary connectives that are consistent with these inference rules. One is implication, and the other sends $A \to B$ to the truth value of $B$. The connective that ignores its left argument seems unsatisfying, so implication is what we're left with.
