Conditionals: Kinds of if-then connection.
In logic there are quite a few kinds of conditionals. I will later treat some of these, but start with two remarks on standard conditionals.
The standard bivalent if-then is defined thus: (if p then q) is true iff (p) is not true or (q) is true, and (if p then q) is not true iff (p) is true and (q) is not true. This is adequate for most mathematical argumentation, and also rather close to most usages of if-then in natural language, but for some cases other kinds of if-then are useful, while also the standard definition of if-then comes with some difficulties. (See: Paradoxes of implication.)
The standard bivalent if-then corresponds to the if-then of inference, indeed provably so by what is known as the Deduction Theorem: From (if p then q) it follows that if (p) one can infer (q), and conversely if one can prove that one can infer (q) if (p) is true, then (if p then q) is true. The difference is that the if-then of inference is, besides an if-then, a rewriting rule, that permits an action, namely the inference of the conclusion if the premisses of the rule are all true.