Editing Material conditional (section)

==Semantics==
===Truth table===
From a [[classical logic|classical]] [[semantics of logic|semantic perspective]], material implication is the [[binary operator|binary]] [[truth function]]al 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]]:
{{2-ary truth table|1|1|0|1|<math>A \to B</math>}}
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 truth]]s".
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===
{{further|Method of analytic tableaux}}
Formulas over the set of connectives <math>\{\to, \bot\}</math><ref>The [[well-formed formula]]s are:
# Each [[propositional variable]] is a formula.
# "<math>\bot</math>" is a formula.
# If <math>A</math> and <math>B</math> are formulas, so is <math>(A \to B)</math>.
# Nothing else is a formula.</ref> are called '''f-implicational'''.{{sfn|Franco|Goldsmith|Schlipf|Speckenmeyer|1999}} In [[classical logic]] the other connectives, such as <math>\neg</math> ([[negation]]), <math>\land</math> ([[logical conjunction|conjunction]]), <math>\lor</math> ([[disjunction]]) and <math>\leftrightarrow</math> ([[If and only if|equivalence]]), can be defined in terms of <math>\to</math> and <math>\bot</math> ([[False (logic)#False, negation and contradiction|falsity]]):<ref name="connective_needed">f-implicational formulas cannot express all valid formulas in [[Minimal logic|minimal]] (MPC) or [[intuitionistic logic|intuitionistic]] (IPC) propositional logic — in particular, <math>\lor</math> (disjunction) cannot be defined within it. In contrast, <math>\{\to, \lor, \bot \}</math> is a complete basis for MPC / IPC: from these, all other connectives (e.g., <math>\land, \neg, \leftrightarrow, \bot</math>) can be defined.</ref>
<math display="block">
\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)
|}

<div style="margin-left: 20px;">
{{collapse top
| title=<span style="display:block; text-align:left; margin-left: -50px; padding-left: 0;">Example: proof of <math>p \to \neg \neg p\quad</math>, by [[method of analytic tableaux]]</span>
| bg=#ffffff | fg=#000000
}}
<pre>
         F[p → ((p → ⊥) → ⊥)]
          |
         T[p]
         F[(p → ⊥) → ⊥]
          |
         T[p → ⊥]
         F[⊥]
 ┌────────┴────────┐
F[p]              T[⊥]
 |                 |
CONTRADICTION     CONTRADICTION
(T[p], F[p])      (⊥ is true)
</pre>
{{collapse bottom}}
</div>

<div style="margin-left: 20px;">
{{collapse top
| title=<span style="display:block; text-align:left; margin-left: -50px; padding-left: 0;">Example: proof of <math>\neg \neg p \to p\quad</math>, by method of analytic tableaux</span>
| bg=#ffffff | fg=#000000
}}
<pre>
         F[((p → ⊥) → ⊥) → p]
          |
         T[(p → ⊥) → ⊥]
         F[p]
 ┌────────┴────────┐
F[p → ⊥]          T[⊥]
 |                 |
T[p]            CONTRADICTION (⊥ is true)
F[⊥]
 |
CONTRADICTION (T[p], F[p])
</pre>
[[Hilbert system|Hilbert-style proofs]] can be found [[Implicational propositional calculus#An alternative axiomatization|here]] or [[Peirce's law|here]].
{{collapse bottom}}
</div>
<div style="margin-left: 20px;">
{{collapse top
| title=<span style="display:block; text-align:left; margin-left: -50px; padding-left: 0;">Example: proof of <math>(p \to q) \to ((q \to r) \to (p \to r))</math>, by method of analytic tableaux</span>
| bg=#ffffff | fg=#000000
}}
<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 system|Hilbert-style proof]] can be found [[Implicational propositional calculus#The Bernays–Tarski axiom system|here]].
{{collapse bottom}}
</div>