Material conditional

The material conditional (also known as material implication) is a binary operation commonly used in logic. When the conditional symbol <math>\to</math> is interpreted as material implication, a formula <math> P \to Q</math> is true unless <math>P</math> is true and <math>Q</math> is false.

Material implication is used in all the basic systems of classical logic as well as some nonclassical logics. It is assumed as a model of correct conditional reasoning within mathematics and serves as the basis for commands in many programming languages. However, many logics replace material implication with other operators such as the strict conditional and the variably strict conditional. Due to the paradoxes of material implication and related problems, material implication is not generally considered a viable analysis of conditional sentences in natural language.

Notation

In logic and related fields, the material conditional is customarily notated with an infix operator <math>\to</math> (). The material conditional is also notated using the infixes <math>\supset</math> and <math>\Rightarrow</math> ( and respectively). In the prefixed Polish notation, conditionals are notated as <math>Cpq</math>. In a conditional formula <math>p\to q</math>, the subformula <math>p</math> is referred to as the antecedent and <math>q</math> is termed the consequent of the conditional. Conditional statements may be nested such that the antecedent or the consequent may themselves be conditional statements, as in the formula <math>(p\to q)\to(r\to s)</math>.

History

In Arithmetices Principia: Nova Methodo Exposita (1889), Peano expressed the proposition "If <math>A</math>, then <math>B</math>" as <math>A</math> Ɔ <math>B</math> with the symbol Ɔ, which is the opposite of C. He also expressed the proposition <math>A\supset B</math> as <math>A</math> Ɔ <math>B</math>. Hilbert expressed the proposition "If A, then B" as <math>A\to B</math> in 1918. Russell followed Peano in his Principia Mathematica (1910–1913), in which he expressed the proposition "If A, then B" as <math>A\supset B</math>. Following Russell, Gentzen expressed the proposition "If A, then B" as <math>A\supset B</math>. Heyting expressed the proposition "If A, then B" as <math>A\supset B</math> at first but later came to express it as <math>A\to B</math> with a right-pointing arrow. Bourbaki expressed the proposition "If A, then B" as <math>A \Rightarrow B</math> in 1954.

Semantics

Truth table

From a classical semantic perspective, material implication is the binary truth functional operator which returns "true" unless its first argument is true and its second argument is false. This semantics can be shown graphically in the following truth table:

One can also consider the equivalence <math>A \to B \equiv \neg (A \land \neg B) \equiv \neg A \lor B</math>.

The conditionals <math>(A \to B)</math> where the antecedent <math>A</math> is false, are called "vacuous truths".

Examples are ...

... with <math>B</math> false: "If Marie Curie is a sister of Galileo Galilei, then Galileo Galilei is a brother of Marie Curie."
... with <math>B</math> true: "If Marie Curie is a sister of Galileo Galilei, then Marie Curie has a sibling."

Analytic tableaux

Formulas over the set of connectives <math>\{\to, \bot\}</math> are called f-implicational. In classical logic the other connectives, such as <math>\neg</math> (negation), <math>\land</math> (conjunction), <math>\lor</math> (disjunction) and <math>\leftrightarrow</math> (equivalence), can be defined in terms of <math>\to</math> and <math>\bot</math> (falsity):

\begin{align}

\neg A & \quad \overset{\text{def{=} \quad A \to \bot \\

A \land B & \quad \overset{\text{def{=} \quad (A \to (B \to \bot)) \to \bot \\

A \lor B & \quad \overset{\text{def{=} \quad (A \to \bot) \to B \\

A \leftrightarrow B & \quad \overset{\text{def{=} \quad \{(A \to B) \to [(B \to A) \to \bot]\} \to \bot \\

\end{align}

</math>

The validity of f-implicational formulas can be semantically established by the method of analytic tableaux. The logical rules are

:{| style="border: none; border-spacing: 1px; border-collapse: separate;"

| style="vertical-align: top;" | <math>\frac{\boldsymbol{\mathsf{T(A \to B)}{\boldsymbol{\mathsf{F(A)

\quad \mid \quad \boldsymbol{\mathsf{T(B)}</math> || valign="top" | <math>\frac{\boldsymbol{\mathsf{F(A \to B)}{\begin{array}{c} \boldsymbol{\mathsf{T(A) \\ \boldsymbol{\mathsf{F(B)\end{array</math>

|colspan="2" | <math>\boldsymbol{\mathsf{T(\bot)</math> : Close the branch (contradiction)<br/><math>\boldsymbol{\mathsf{F(\bot)</math> : Do nothing (since it just asserts no contradiction)

<pre>

F[p → ((p → ⊥) → ⊥)]

T[p]

F[(p → ⊥) → ⊥]

T[p → ⊥]

F[⊥]

┌────────┴────────┐

F[p] T[⊥]

| |

CONTRADICTION CONTRADICTION

(T[p], F[p]) (⊥ is true)

</pre>

</div>

<pre>

F[((p → ⊥) → ⊥) → p]

T[(p → ⊥) → ⊥]

F[p]

┌────────┴────────┐

F[p → ⊥] T[⊥]

| |

T[p] CONTRADICTION (⊥ is true)

F[⊥]

CONTRADICTION (T[p], F[p])

</pre>

Hilbert-style proofs can be found here or here.

</div>

<pre>

1. F[(p → q) → ((q → r) → (p → r))]

| // from 1

2. T[p → q]

3. F[(q → r) → (p → r)]

| // from 3

4. T[q → r]

5. F[p → r]

| // from 5

6. T[p]

7. F[r]

┌────────┴────────┐ // from 2

8a. F[p] 8b. T[q]

X ┌────────┴────────┐ // from 4

9a. F[q] 9b. T[r]

X X

</pre>

A Hilbert-style proof can be found here.

</div>

Syntactical properties

The semantic definition by truth tables does not permit the examination of structurally identical propositional forms in various logical systems, where different properties may be demonstrated. The language considered here is restricted to f-implicational formulas.

Consider the following (candidate) natural deduction rules.

{| class="wikitable"

|valign="top"| Implication Introduction (<math>\to</math>I)

If assuming <math>A</math> one can derive <math>B</math>, then one can conclude <math>A \to B</math>.

<math>

\frac{\begin{array}{c}

[A] \\

\vdots \\

\end{array{A \to B}</math> (<math>\to</math>I)

<math>[A]</math> is an assumption that is discharged when applying the rule.

|valign="top"| Implication Elimination (<math>\to</math>E)

This rule corresponds to modus ponens.

<math>\frac{A \to B \quad A}{B}</math> (<math>\to</math>E)

<math>\frac{A \quad A \to B}{B}</math> (<math>\to</math>E)

|valign="top"| Double Negation Elimination (<math>\neg\neg</math>E)

<math>

\frac{\begin{array}{c}

(A \to \bot) \to \bot \\

\end{array{A}</math> (<math>\neg\neg</math>E)

|valign="top"| Falsum Elimination (<math>\bot</math>E)

From falsum (<math>\bot</math>) one can derive any formula.<br/>(ex falso quodlibet)

<math>\frac{\bot}{A}</math> (<math>\bot</math>E)

Minimal logic: By limiting the natural deduction rules to Implication Introduction (<math>\to</math>I) and Implication Elimination (<math>\to</math>E), one obtains (the implicational fragment of)