previous up next
Go backward to 2.2.4 Disjunctions
Go up to 2.2 Propositional Logic
Go forward to 2.2.6 Equivalences
RISC-Linz logo

2.2.5 Implications

If A and B are formulas, then
(A => B)
is a formula.

Alternative Forms  An implication A => B is often also expressed as

The last line denotes the input syntax of the Logic Evaluator.

Definition 9 (Semantics of Implication) Let A and B be formulas. The meaning of A => B is defined by the following truth table:
A B A => B
false false true
false true true
true false false
true true true

In other words, A => B is false if and only if A is true and B is false. 

Please note that an implication is always true if its premise is false. This may appear strange at first glance, because it makes sentences like "if 2 is odd, then 3 is even" true. However, by an implication we actually want to express the fact "if the premise holds, then also the conclusion holds", i.e.,

This behavior is also expressed by the first of the following laws.

Proposition 9 (Implicative Laws) For all formulas A and B, we have
A => B iff ~A \/ B
A => B iff ~B => ~A
~(A => B) iff A /\  ~B.

Because of the first law, the implication A => B is frequently defined just as a syntactic abbreviation for ~A \/ B.

Operational Interpretation  In the Logic Evaluator, an implication is represented by an object of the Java type

public final class Implies implements Formula
  private Formula formula0;
  private Formula formula1;

  public Implies(Formula _formula0, Formula _formula1)
    formula0 = _formula0;
    formula1 = _formula1;

  public boolean eval() throws EvalException
    if (formula0.eval())
      if (formula1.eval())
        return true;
        return false;
      return true;
The Java expression (new Implies(A, B)).eval() computes the truth value of A => B. As one can see, if A evaluates to false, the result is immediately true, i.e., the truth value of B does not matter any more. Only if A evaluates to true, also B is evaluated; the result is false only if A is true and B is false.
Author: Wolfgang Schreiner
Last Modification: October 4, 1999

previous up next