# How does one know if $A \implies B$ (an implication) is true without knowing if $B$ (the consequent is true) is true?

This might be a weird question but I was trying to distinguish the difference between an implication and modus ponens. I think the distinction is clear in my head (but I have something missing), modus ponens is just a rule of inference that produces more true statement based on $A$ and $A \implies B$. An implication is a truth function that when given statements with truth values, i.e. the truth values of $A \implies B$ can be known only from the truth values of $A$ and $B$ (no other info is needed). It can be easily evaluated by looking up the truth table. These make sense. However, I reached a confusion/contradiction in the model of how I thought logic (and mathematics!) worked. It seems to me that according to modus ponens we need to know already the value of the implication $A \implies B$ before we can known if $B$ is true. However, according to the table to evaluate the truth function we need the values of both $A$ and $B$. So it seems like a chicken and egg problem. How is it actually possible to know $A \implies B$ without knowing $B$? It seems odd to me. I do understand however, how the inference is suppose to work. Since we know the output of the function (=implication) and one of its inputs, then it should be trivial, to know the other input because of the way the truth table for implication is defined. I think that part makes sense. However, what I don't understand is how in practice we are able to know $A \implies B$ is true in the first.

I think the main issue I had is that in my head what I thought is that for $A \implies B$ to be known to be true, we actually proceeded to apply rules of inference to our statements and then reached $B$. Thats I think how I thought I did maths in practice. I started with $A$ and applied valid maths rules and inference rules until I reached $B$. Thus, it seems that I never actually used the truth functional implication to do any maths, only maths facts that produced step by step another maths step until the final $B$ was produced. I assume there must be some confusion in how I thought mathematics worked, so I wanted to clarify, does someone know where my confusion is?

What does a "maths step" even mean? I thought it was modus ponens but now I realized I need to know $A \implies B$ for that to be true but that can't be true because that's what I am trying to figure out how to get the truth value of in the first place to be able to even use modus ponens.

In the end it all seems to boil down to, how do we actually conclude $A \implies B$ is true in a proof?

I always thought that we started with $A$, the just mechanically moved from $A$ to the next step and the next step until $A$ arrived at $B$ and then at that point we'd know $B$ was true. Is that not correct? I'm not sure if what I am asking is what a "step" means in mathematics. It seems like it because I would have thought intuitively that a series of steps like that must be a set of implications OR alternatively a series of steps of Modus Ponens. Regardless, it seems to me I understand what the difference between a modus ponens and implications are but I can't seem how to figure out how an implication is even known to be true in the first place without resulting in circular logic.

How does one know if $A \implies B$ (an implication) is true without knowing if $B$ (the consequent is true) is true?

my apologies I wasn't quite sure how to compress my question.

• One doesn't: if B is false and A is true then the whole implication is false. In any other case the implication is true. – DonAntonio Dec 21 '17 at 21:11
• @DonAntonio I thought the whole point of a proof is to know if $B$ is true. I guess I am wonder, I have a statement $A$ and want to know if $B$ is true. I'd go and find out if $A \implies B$ right? How does one do that and what does that mean? – Pinocchio Dec 21 '17 at 21:13
• Without looking at your question body, I can only say the answer for the question in the title is "to know $A$ is false". – GNUSupporter 8964民主女神 地下教會 Dec 21 '17 at 21:13
• @GNUSupporter I guess the assumption is that $A$ is true. The point is to understand how one figures out if $A \implies B$ is true in the first place for us to be able to use modus ponens. It can't be that we use modus ponens to figure out if $A \implies B$ is true. Thats sort of the point I believe in my confusion. – Pinocchio Dec 21 '17 at 21:14
• Right. You need to have other rules that can transform $A$ to $B$. The rule might not need to be $A \implies B$ itself. You might have a rule $A \implies C$ and a rule $C \implies B$. – Kenny Lau Dec 21 '17 at 21:19

Consider the following statements:

$A$: Adam lives in Boston; $B$: Adam lives in Massachusetts.

You've never met Adam before, and you have no idea whether statements $A$ or $B$ are true. But you do know that the statement $A \Rightarrow B$ is true. If I now presented to you a way to prove that Adam lived in Boston, you could reasonably conclude that he lives in Massachusetts.

I assume you would agree with a statement like "If it rains, the streets get wet', right?

Now, before you agreed to the truth of that conditional, did you look out the window to see if right now it is raining or not, and whether right now the streets are getting wet or not? No, clearly not.

Yes, it is true that we often come to the truth of conditionals based on empirical evidence, i.e. presumably on a bunch of cases where we observe the antecedent is true and the consequent also true ... and also not seeing cases where the antecedent is true and the consequent false. Such conditionals are established by non-deductive reasoning though, but inductive generalizations or other such reasoning. So, there is no circularity of reasoning here.

Also, some conditionals are simply asserted as part of some definition or axiom, so in that case any observations of ay statements actually being true or false aren't used at all.

Furthermore, conditionals are often part of universal statements. The 'if it rains, the streets get wet' can in fact be seen as such as well: it is really a universal claim about any place and any time. So it is really the universal we are either establishing on the basis of many observations, or are simply asserting as an axiom, and so there we are certainly not establishing the truth of that universal conditional on a single observation as to whether the antecedent and consequent are true or false.

Finally, once conditionals are established, we can just use them, without having to worry whether the antecedent is actually true or false, or whether the consequent is true or false. So, in practice, there is really no chicken-and-egg problem here.

(*) Example of an implication: If a snack contains sugar, then it will be sweet.

Modus ponens tells us that start with the premise (*), and we also know that a snack contains sugar, then we can assert that the snack will be sweet.

The way you thought mathematics work, or rather informal theorem proving, is how it works. Classical propositional logic is a small fragment of the reasoning tools used by typical informal arguments, and, more generally, a semantic approach to logic does not match the proof process well, hence proof theory.

There are two broad approaches to understanding (formal) logic: a syntactic or proof-theoretic approach and a semantic or model-theoretic approach.

Using truth tables and truth functionals is a semantic approach. Here we interpret the syntactic formulas into mathematical objects, and then whether the "truth" of a proposition becomes a property of the mathematical object it is interpreted as. For example, we can interpret the propositions $A$ and $B$ as subsets $[\![A]\!]$ and $[\![B]\!]$ of a set $X$. Asking if $A\lor B$ is "true" becomes the statement that $[\![A]\!]\cup[\![B]\!]=X$. Note how this has nothing to do with whether $A$ or $B$ are philosophically "true". The interpretation of the statement is just asking whether the union of two sets is equal to another. Proving or disproving this statement will typically be done informally, but could be done formally, e.g. with Zermelo-Fraenkel set theory in this case. Of course, we can't exactly use the same approach to prove this semantic statement. This leads to the other approach: proof theory.

A different way to understand what's happening in logic is to give rules. Here the syntactic formulas just stay syntax. Instead we give rules that transform these formulas, and we call certain formulas axioms. Theorems are then any formulas we can get by applying the rules to the axioms. This is much more like the "mechanical" process you allude to. Indeed, this is what theorem proving programs do. The philosophical idea is that axioms are supposed to stand for things that are "true", and the rules are supposed to "preserve truth", but it is all just symbol pushing. It makes no difference to the rules whether the formulas are true or not or even if they are contradictory. For typical logics, from a proof theoretic standpoint, all inconsistency means is that every formula can be reached from the axioms by the rules. (Semantically, inconsistency usually means there is no model. In other approaches to semantics, it may mean there are only "trivial" models.) The actual proof is then the sequence of (valid) rule applications and is called a derivation.

The proof system that is typically first presented to students is a Hilbert-style proof system. This is a bit of a shame as Hilbert-style proof systems aren't very human friendly to work in. Other proof systems include natural deduction and the sequent calculus. Personally, I like to use natural deduction through a Curry-Howard lens. This leads to proofs having a compact, simple representation that makes symbol manipulation easy. (The connections to computation also provide a lot of intuition if one is familiar with functional programming.) For example, a use of modus ponens corresponds just to function application. (From this perspective, the lack of human-friendliness of Hilbert-style proof systems is more evident as they correspond to combinatory logic which is very unpleasant to program in.) Natural deduction proofs (as the name might suggest) were intended to be closer to how informal proofs flowed. Once you have a decent amount of experience with informal proofs and with systems like natural deduction, it's actually pretty easy to "read out" even the fine-grained logical structure of an informal proof as a derivation in a natural deduction-like system.

The syntactic approach provides a straightforward answer to your concerns about needing to know the truth value of $B$ to know the truth value of $A\Rightarrow B$ to use modus ponens. Modus ponens is a rule of inference, it simply states that if we have a derivation of $A$ (i.e. a sequence of valid rule applications) and a derivation of $A\Rightarrow B$, then we can make a derivation of $B$. Deriving $A\Rightarrow B$ need not (and typically will not) require already having a derivation of $B$. In practice, the rules are usually formulated to work on conditional formulas. Often these are written like e.g. $\varphi,\psi\vdash\chi$ (though this notation is used in a variety of different but related ways) which is intuitively supposed to stand for "it is provable that $\chi$ is true if $\varphi$ and $\psi$ are true", but, again, is just syntax that will be manipulated. The intuitive reading is only justified if the rules and axioms allow it to be. Using conditional formulas makes it much easier to include assumptions, and it also makes formulating the rules significantly simpler.

Finally, these two approaches to logic are different. It is not at all clear a priori that they lead to the same notion of "truth". The soundness and completeness (meta-)theorems, e.g. the ones for FOL, (and the stronger notion of an internal logic which gets into categorical semantics) are what connect them. But soundness and completeness theorems are (meta-)theorems which must be proven for a given proof system and semantics. It's not always possible to prove both (though usually a violation of soundness means you've done something very wrong). In the syntactic approach, a proof is a derivation and so checking truth tables is just a non sequitur. Even if the truth tables show that a formula is a tautology, that doesn't actually provide you with a derivation, and so is of no use syntactically. The (meta-logical) proof of completeness of a natural deduction system for classical propositional logic with respect to truth tables, say, needs to actually show how to build a natural deduction derivation given a formula and a truth table showing the formula is valid. It is apparently pretty common for the syntactic and semantic approaches to logic to be significantly conflated or at least not clearly separated, but this leads to a lot of confusion. (For example, if one thought that a proof was checking truth tables, then soundness and completeness don't even make sense or seem completely trivial.)

The example of truth tables and propositional logic hides most of the complexity of actual mathematics, which involves variables and quantifiers. So, rather than looking at somewhat artificial examples in propositional logic, we can look at more natural examples from actual mathematics. Here is a better example of an implication that we can prove to be true, although we don't know whether the hypothesis is true or false:

If $n$ is an even natural number then $n^2$ is an even natural number.

Proof: If $n$ is an even natural number, then $n = 2m$ for some natural number $m$. Then $n^2 = 4m^2 = 2(2m^2)$, so $n^2$ is also even.

In this case, we cannot say whether "$n$ is an even natural number" is true or false - we have no specific value for $n$. Instead we are proving a fact about all natural numbers simultaneously (namely, that if they are even, then so is their square). To prove this kind of statement, we "assume the hypothesis and prove the conclusion" - we assume that we are presented with some otherwise unknown even number $n$, and prove that $n^2$ must also be even.

The starting points, underneath it all, are definitions. The definition of an "even number" allows us to state that if $n$ is an even natural number then $n = 2m$ for some natural number $m$. This is already an implication statement, but we do not "prove" it separately because it is simply the definition of "even". In a sense, the proof above simply proves a more complicated implication by combining together simpler implications that were already known.

So how could we apply modus ponens in an argument using our theorem? If we prove separately that some particular number $C$ is even, we can apply modus ponens and our theorem to show that $C^2$ is also even. We would need to derive "$C$ is even" separately, of course.

We can actually prove that the implication $A\implies B$ is true knowing only that $A$ is false and nothing at all about $B$.

The only property of material implication that we require is that, if you assume $P$ and can subsequently derive $Q$ then you can infer $P \implies Q$. (Some restrictions apply.)

Theorem:

$\neg A \implies [A\implies B]$

Proof:

1. Suppose $\neg A$

2. Suppose $A$

3. Suppose (to the contrary) that $\neg B$

4. Join (2) and (1) to obtain the contradiction $A \land \neg A$

5. Conclude that $\neg \neg B$ from (3) and (4).

6. Remove the double negation from (5) to obtain $B$.

7. Conclude that $A\implies B$ from (2) and (6).

8. Conclude, as required, that $\neg A \implies [A\implies B]$ from (1) and (7).

Likewise, we can also prove:

$A \land B \implies [A\implies B]$

$A \land \neg B \implies \neg [A \implies B]\space$ (requires detachment rule as well)

In this way, we can justify the usual truth table for material implication.

Follow-up: Another approach: I have proven that $[A\implies B] \iff \neg [A \land \neg B]$ using detachment and deduction rules. It is often simply stated as a definition leaving many beginners scratching their heads. $\neg A \implies [A \implies B]$ is a corollary. See "If Pigs Could Fly," new today at my math blog.