# Justification of implication-introduction and modus ponens

Given only the definition of material implication through the truth table

``` A |  B  |  A → B
------------------
f |  f  |  t
f |  t  |  t
t |  f  |  f
t |  t  |  t
```

(where, as usual, "t" means true and "f" means false), how can one justify the implication-introduction, which is the inference rule that says that we can conclude that the implication A → B holds if we have proven B under the hypothesis A? Also, how can one justify modus ponens from the definition via truth table?

Modus ponens can be stated as: (A → B and A) ⊢ B. If you look in the truth table, every line that has `t` for both A → B and A (only the last) has `t` for B as well. Hence, there is no situation where A → B and A are true, but B is not.

As for implication introduction: proving B under hypothesis A means that there is no situation where A is true, but B is not. Hence, the third line of the truth table is irrelevant. Then the only lines that remain are where A → B has value `t`. Hence, it is always true given that B can be proven using A.

• Sorry, I am mean "implication"-introduction, which is the inference rule I describe. My question has nothing to do with quantifiers, I really don't know why I wrote "for all". Commented Sep 17, 2016 at 12:33
• @user23178 no problem, it can happen. Welcome to Philosophy.SE, by the way :)
– user2953
Commented Sep 17, 2016 at 12:34
• All four rows of the truth table hold for Wajsberg-Lukasiewicz three valued logic. But, implication introduction does NOT work for such a system. Commented Sep 19, 2016 at 2:25

If you've proven `B` from hypothesis `A`, then

`````` A |  B  |
----------
f |  f  |     may be possible
f |  t  |     may be possible
t |  f  |     definitely impossible; A is true, then B must be too!
t |  t  |     may be possible
``````

Since the third line can't happen, we really shouldn't include it in our truth tables; that line can never appear when (correctly) assigning truth values to propositions.

Therefore, the truth table becomes

`````` A |  B  |  A → B
------------------
f |  f  |  t
f |  t  |  t
t |  t  |  t
``````

and we see that A→B is identically true. So if we know `A⊨B`, we can infer `⊨A→B`.

Similarly, the relevant lines for the premise that both `A` and `A→B` are

`````` A |  B  |  A → B
------------------
f |  f  |  t       not this; we need A true
f |  t  |  t       not this; we need A true
t |  f  |  f       not this; we need A→B true
t |  t  |  t       possible
``````

and so the relevant lines of the truth table are

`````` A |  B  |  A → B
------------------
t |  t  |  t
``````

so we see `B` is identically true given the premise. We conclude that `A,A→B⊨B`.

• All four rows of your truth table hold for Wajsberg-Lukasiewicz three valued logic. But, implication introduction does NOT work for such a system. Commented Sep 19, 2016 at 2:24
• @DougSpoonwood: I don't see the relevance of such an observation to the topic of semantic entailment in two-valued logic.
– user6559
Commented Sep 19, 2016 at 7:29
• From what I've read, independence usually gets established by constructing a model where all of the axioms hold but one of them, showing that axiom independent of the others. Semantically speaking the truth tables represent equational axioms. Wajsberg-Lukasiewicz three-valued logic has all of those equations, but not the rule of conditional introduction. Thus, if axioms connect to rules of inference, it seems to me that it follows that the table can establish the independence of conditional introduction from the two-valued truth table as follows: Commented Sep 19, 2016 at 15:35
• You can prove in Polish notation contraction: CCpCpqCpq or in infix: ((p -> (p -> q)) -> (p -> q)) via conditional introduction and detachment (left as an exercise!). Now check to see if CCpCpqCpq holds for the Wajsberg-Lukasiewicz three-valued table. So, the truth table equations can hold, while CCpCpqCpq is not derivable. Detachment still holds for the Lukasiewicz-table as a valid rule of inference (exercise!). Thus, the assumption of a connection between the truth tables and conditional introduction has gotten contradicted. Commented Sep 19, 2016 at 15:45
• @DougSpoonwood: Semantic entailment is literally "forget about the rules of deduction, just look at what happens in all interpretations". (although it turns out that classical propositional logic is sound and complete with respect to semantics in two-valued boolean algebra, so in that particular case what you can prove semantically and syntactically are the same)
– user6559
Commented Sep 19, 2016 at 15:54

No can do. you're mixing truth-conditional logic and constructive logic. there are no introduction rules in the former, only truth tables.

Implication introduction corresponds to a meta-theorem in logic, called the Deduction Theorem, which states that

If Γ ∪ {A} ⊢ B, then Γ ⊢ A → B

(Where Γ is a set of sentences.) This means that if you prove B using some assumption A, then you're allowed to deduce A → B without the assumption A.

The theorem can be proved for other formal systems that don't have implication introduction, such as Hilbert system. (You can see such a proof here.)

• the proof you cite depends on a "principle" of mathematical induction. Frankly I'm not sure about the status of such principles from the logician's perspective. in any case it just moves the OP's question: what's the justification of the principle (s) of mathematical induction?
– user20153
Commented Sep 18, 2016 at 20:36

I categorically reject any way to justify implication-introduction via the truth table. In Wajsberg-Lukasiewicz three-valued logic, we the following truth-table:

``````        ->
p/q  T  N  F
T    T  N  F
N    T  T  N
F    T  T  T
``````

The two-valued truth table is contained within that truth table (look at the corners). But, from a hypothesis A and a deduction of B, we cannot conclude (A -> B) in that system.

To show modus ponens sound, you assume (p -> q) true, and p true. This entails that we need to look at the p row for T, which is

``````    ->_classical
p/q T F
T   T F
F   T T

->_classical top row
p/q T F
p   T F
``````

Now we look at where (p -> q) holds true. This corresponds to only spot where q holds true. Consequently, meta-logically, modus ponens is sound.

• The question appears to be about semantics in two-valued logic, not three-valued logic. Semantic entailment need not be the same when you change semantics.
– user6559
Commented Sep 19, 2016 at 7:35
• Although... it's worth noting that if we take "proven B under hypothesis A" to also excludes the case of `(p,q)=(N,F)`, implication-introduction is still semantically valid.
– user6559
Commented Sep 19, 2016 at 7:50

Given only the definition of material implication through the truth table, how can one justify the implication-introduction, which is the inference rule that says that we can conclude that the implication A → B holds if we have proven B under the hypothesis A? Also, how can one justify modus ponens from the definition via truth table?

You have it backwards. It is the truth table of material implication that is justified by the combined principles of:

• Excluded Middle
• Modus ponens
• Implication introduction

For a detailed development, see my recent blog posting Material Implication: If Pigs Could Fly.

Modus Ponens is a tool for tracking the preservation of meaning from the antecedent to the conclusion. For example, in the Logic of Paradox (LP), Modus Ponens is invalid since though you can’t get anything completely false from true premises, the semantics of LP doesn’t guarantee that something neither true nor false won’t follow from something true. In Classical Logic, the meaning being preserved from antecedent to consequent is truth, while in Intuitionistic Logic it is justification. It gets even more complicated that in some logics, Modus Ponens is not universally valid, but only valid when both a conditional and its antecedent are provable.

As others have noted, Implication Introduction as an inference rule corresponds to the Deduction Metatheorem (DT). It would take a bit to show this, but over Modus Ponens and substitution, these two axioms are equivalent to DT:

A→(B→A)

(A→(B→C))→((A→B)→(A→C)).

The first axiom basically allows you to prefix any formula that occurs in a sub-proof with the formula used as the assumption in said sub-proof. The second axiom allows you to prefix instances of Modus Ponens that occur within a sub-proof with the formula that is made as the assumption in that sub-proof.

For example, the two given axioms allow you to transform a derivation like

A

.

.

.

B→C

B

C

into a fully axiomatic proof. The full procedure for converting a derivation to an axiomatic proof can be found in the Wikipedia article “Hilbert System”.