Description: If and are wff's, so is or " implies
." Part of the recursive definition of
a wff. The resulting wff
is (interpreted as) false when is true and is false; it is
true otherwise. Think of the truth table for an OR gate with input
connected through an inverter. After we define the axioms of
propositional calculus (ax-16, ax-27, ax-38, and ax-mp5), the
?Error:
T.
^^
This math symbol is not active (i.e. was not declared in this scope).
biconditional (df-bi179), the constant true (df-tru1329), and the
?Error:
F.
^^
This math symbol is not active (i.e. was not declared in this scope).
constant false (df-fal1330), we will be able to prove these truth
?Error:
T. -> T. ) <-> T. )
^^
This math symbol is not active (i.e. was not declared in this scope).
table values: ((->)<->) (truimtru1354),
?Error:
T. -> F. ) <-> F. )
^^
This math symbol is not active (i.e. was not declared in this scope).
?Error:
F. -> T. ) <-> T. )
^^
This math symbol is not active (i.e. was not declared in this scope).
((->)<->) (truimfal1355), ((->)<->)
?Error:
F. -> F. ) <-> T. )
^^
This math symbol is not active (i.e. was not declared in this scope).
(falimtru1356), and ((->)<->) (falimfal1357). These
?Error:
T. -> T. ) <-> T. )
^^
This math symbol is not active (i.e. was not declared in this scope).
have straightforward meanings, for example, ((->)<->)
?Error:
T. -> T.
^^
This math symbol is not active (i.e. was not declared in this scope).
?Error:
T.
^^
This math symbol is not active (i.e. was not declared in this scope).
just means "the value of -> is ".
The left-hand wff is called the antecedent, and the right-hand wff is
called the consequent. In the case of , the
middle may be informally called either an
antecedent or part of the
?Error:
<->
^^^
This math symbol is not active (i.e. was not declared in this scope).
consequent depending on context. Contrast with <-> (df-bi179),
?Error:
/\
^^
This math symbol is not active (i.e. was not declared in this scope).
?Error:
\/
^^
This math symbol is not active (i.e. was not declared in this scope).
/\ (df-an362), and \/ (df-or361).
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 made of
green
cheese that implies that 5=7" (because the moon is not actually made
of
green cheese). A contradiction implies anything (pm2.21i126). In short,
material implication has a very specific technical definition, and
misunderstandings of it are sometimes called "paradoxes of logical
implication."
Hypotheses
Ref
Expression
wph
wps
Assertion
Ref
Expression
wi
This syntax is primitive. The first axiom using it is ax-16.