Description: If ph and ps are wff's, so is ( ph -> ps ) or " ph implies
ps ". Part of the recursive definition of a wff. The resulting wff
is (interpreted as) false when ph is true and ps is false; it is
true otherwise. Think of the truth table for an OR gate with input ph
connected through an inverter. After we state the axioms of propositional
calculus ( ax-1 , ax-2 , ax-3 , and ax-mp ) and define the
biconditional ( df-bi ), the constant true T. ( df-tru ), and the
constant false F. ( df-fal ), we will be able to prove these truth
table values: ( ( T. -> T. ) <-> T. ) ( truimtru ),
( ( T. -> F. ) <-> F. ) ( truimfal ), ( ( F. -> T. ) <-> T. )
( falimtru ), and ( ( F. -> F. ) <-> T. ) ( falimfal ). These
have straightforward meanings, for example, ( ( T. -> T. ) <-> T. )
just means "the value of ( T. -> T. ) is T. ".

The left-hand wff is called the antecedent, and the right-hand wff is
called the consequent. In the case of ( ph -> ( ps -> ch ) ) , the
middle ps may be informally called either an antecedent or part of the
consequent depending on context. Contrast with <-> ( df-bi ),
/\ ( df-an ), and \/ ( df-or ).

This is called "material implication" and the arrow is usually read as
"implies". However, material implication is not identical to the meaning
of "implies" in natural language. For example, the word "implies" may
suggest a causal relationship in natural language. Material implication
does not require any causal relationship. Also, note that in material
implication, if the consequent is true then the wff is always true (even
if the antecedent is false). Thus, if "implies" means material
implication, it is true that "if the moon is made of green cheese that
implies that 5=5" (because 5=5). Similarly, if the antecedent is false,
the wff is always true. Thus, it is true that, "if the moon is made of
green cheese that implies that 5=7" (because the moon is not actually made
of green cheese). A contradiction implies anything ( pm2.21i ). In
short, material implication has a very specific technical definition, and
misunderstandings of it are sometimes called "paradoxes of logical
implication".