MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  wi Unicode version

Syntax Definition wi 4
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-1 6, ax-2 7, ax-3 8, and ax-mp 5), the ?Error: T. ^^ This math symbol is not active (i.e. was not declared in this scope). biconditional (df-bi 179), the constant true (df-tru 1329), and the ?Error: F. ^^ This math symbol is not active (i.e. was not declared in this scope). constant false (df-fal 1330), 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: (( -> )<-> ) (truimtru 1354), ?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). (( -> )<-> ) (truimfal 1355), (( -> )<-> ) ?Error: F. -> F. ) <-> T. ) ^^ This math symbol is not active (i.e. was not declared in this scope). (falimtru 1356), and (( -> )<-> ) (falimfal 1357). 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-bi 179), ?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-an 362), and \/ (df-or 361).

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.21i 126). 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-1 6.

Colors of variables: wff set class
  Copyright terms: Public domain W3C validator