previous up next
Go backward to B.3 General Strategies
Go up to B Proving Propositions
Go forward to B.5 Deriving New Knowledge
 RISC-Linz logo

B.4 Decomposing the Goal

In a proof situation
K
G
where the goal G is not an atomic formula, the usual strategy is to decompose the proof into subproofs in a way that is determined by the outermost quantifier respectively connective of G.

Proposition 141 (Decomposition of Universal Quantifications) For proving with knowledge K the goal forall x: G, it suffices to prove G[x <- a] where a is an object constant that does not appear in K and not in G.
K
forall x: G
~~>
K
G[x <- a]
(a not in K union {G})

In the proof of a universal formula we thus replace the variable by a constant about which no assumptions have been made yet. This may be indicated in a natural language proof in a very verbose form as

We have to prove (forall x: G). We take an arbitrary (but fixed) constant a and show G[x <- a].

Usually, we choose instead of a some name that indicates the name of the corresponding variable, e.g., x. Even more frequently, we simply chose x as the name of the constant provided that x does not appear freely in K or G. We then simply write

We have to prove (forall x: G). We take arbitrary x and show G.
or even shorter
We have to prove (forall x: G). Take arbitrary x. Then ...(proof of G).
However, we have to understand that x now represents an arbitrary (but fixed) constant. Allmost all proofs in this document use this style, see for instance the proof of Proposition Function Composition or the proof of Proposition Differences.

Frequently also the indirect method is applied in such a situation. Instead of proving (forall x: G) we assume (~forall x: G), i.e., (exists x: ~G) and proceed to derive a contradiction with the help of a constant a such that G holds (see Proposition Existential Knowledge):

K
forall x: G
~~>
K union {exists x: ~G}
F(alse)
~~>
K union {~G[x <- a]}
F(alse)

This is typically indicated as

We have to prove (forall x: G). Assume ~G for some x. Then ... (derivation of a contradiction with additional knowledge ~G).
In this formulation, x now represents a constant for the rest of the proof.

Proposition 142 (Decomposition of Existential Quantifications) For proving with knowledge K the goal exists x: G, it suffices to prove G[x <- T] for some term T.
K
exists x: G
~~>
K
G[x <- T]

An existential proof requires creativity. We have to find a  witness (Zeugen), i.e., a value for x that makes G true. This value can be only constructed from those function and object constants about which we have some knowledge in K such that we can proceed to prove G.

In natural language, such a proof is usually indicated as

We have to prove (exists x: G). We prove G[x <- T].

or, if x occurs multiple times in G, shorter as

We have to prove (exists x: G). Take a := T. We prove G[x <- a].

where a is an object constant that does not appear in K and for which we assume the additional knowledge a = T. Even shorter, we may write

We have to prove (exists x: G). Take x := T. We then have ...(proof of G with additional knowledge x = T).

This is possible if x does not occur freely in K.

For examples, see the proof of Proposition Density of Rationals or the proof of the existence of a factorization into prime numbers.

The indirect method may be applied by assuming (~exists x: G), i.e., (forall x: ~G) and deriving a contradiction, see Proposition Universal Knowledge:

K
exists x: G
~~>
K union {forall x: ~G}
F(alse)
.

This is usually indicated as follows:

We have to prove (exists x: G). Assume (forall x: ~G). Then ... (derivation of a contradiction with additional knowledge (forall x: ~G)).

Proposition 143 (Decomposition of Equivalences) For proving with knowledge K the goal G0 <=> G1, it suffices to prove both G0 => G1 and G1 => G0:
K
G0 <=> G1
~~>
K
G0 => G1
K
G1 => G0

An equivalence is shown by proving the implication "from left to right" and "from right to left", sometimes denoted as

We have to prove G0 <=> G1:

If we have to show G0 <=> G1 <=> G2, i.e., (G0 <=> G1) /\  (G1 <=> G0), it suffices to "traverse the circle", i.e., to show (G0 => G1) /\  (G1 => G2) /\  (G2 => G0) (and analogously for an arbitrary number of equivalences).

Examples are shown in the proofs of Proposition Equality and Subset and of Proposition Relation Laws.

Proposition 144 (Decomposition of Implications) For proving with knowledge K the goal G0 => G1, it suffices to prove G1 with additional knowledge G0:
K
G0 => G1
~~>
K union {G0}
G1

Almost every proof contains applications of above rule indicated as

We have to show G0 => G1. Assume G0. Then ...(proof of G1 with additional knowledge G0).

Because of (G0 => G1) iff (~G1 => ~G0), an alternative is to apply the rule

K
G0 => G1
~~>
K union {~G1}
~G0
indicated as
We have to show G0 => G1. Assume ~G1. Then ...(proof of ~G0 with additional knowledge ~G1).

Because of ~(G0 => G1) iff (G0 /\  ~G1), the indirect method yields

K
G0 => G1
~~>
K union {G0 /\  ~G1}
F(alse)
which is typically indicated as
We have to show G0 => G1. Assume G0 /\  ~G1. Then we have ... (derivation of a contradiction).

Examples are given in the proofs of Proposition Equality and of the Second Peano Law.

Proposition 145 (Decomposition of Conjunctions) For proving with knowledge K the goal G0 /\  G1, it suffices to prove both G0 and G1:
K
G0 /\  G1
~~>
K
G0
K
G1

A conjunction is shown by showing both conjuncts in turn:

We have to show G0 /\  G1.
  1. ...(proof of G0).
  2. ...(proof of G1).

Because of ~(G0 /\  G1) iff ~G0 \/ ~G1, the indirect method leads to

K
G0 /\  G1
~~>
K union {~G0 \/ ~G1}
F(alse)
~~>
K union ~G0
F(alse)
K union ~G1
F(alse)
applying the technique of "case distinction":
We have to prove G0 /\  G1.
  1. Assume ~G0. Then ...(derivation of contradiction with additional assumption ~G0).
  2. Assume ~G1. Then ...(derivation of contradiction with additional assumption ~G1).

Examples of proofs of conjunctions are given for Proposition Function Composition for the existence of a factorization into prime numbers.

Proposition 146 (Decomposition of Disjunctions) For proving with knowledge K the goal G0 \/ G1, it suffices to prove G1 with additional knowledge ~G0.
K
G0 \/ G1
~~>
K union ~G0
G1

This rule is a consequence of "(G0 \/ G1) iff (~G0 => G1)" such that the same techniques can be applied as for the decomposition of implications:

We have to show G0 \/ G1. Assume ~G0. Then ...(proof of G1).

Of course, the roles of G0 and G1 can be inverted.

Frequently, in a particular proof situation, the additional assumption is not required and one simply says

We have to show G0 \/ G1. We have ...(proof of G0 or of G1).

Proposition 147 (Explicitly Defined Predicates) For proving an atomic formula p(a0, ..., an-1) where p is predicate explicitly defined as
p(x0, ..., xn-1) : <=> G,
and a0, ..., an-1 are terms, it suffices to prove G[x0 <- a0, ..., xn-1 <- an-1]:
K union {forall x0, ..., xn-1: p(x0, ..., xn-1) <=> G}
p(a0, ..., an-1)
~~>
K union {forall x0, ..., xn-1: p(x0, ..., xn-1) <=> G}
G[x0 <- a0, ..., xn-1 <- an-1]

We may thus just insert the definition of a predicate into a goal formula:

We have to prove p(a0, ..., an-1). By definition of p, it suffices to prove G[x0 <- a0, ..., xn-1 <- an-1].

The proofs of Proposition Equality and Subset and of Proposition Function Composition show applications of above rule.

Proposition 148 (Explicitly Defined Functions) For proving the goal F[x <- G(a0, ..., an-1)] where f is a function explicitly defined as
G(x0, ..., xn-1) := T,
it suffices to prove G[x <- T[x0 <- a0, ..., xn-1 <- an-1]] (for some terms T, a0, ..., an-1):
K union {forall x0, ..., xn-1: G(x0, ..., xn-1) = T}
G[x <- G(a0, ..., an-1)]
~~>
K union {forall x0, ..., xn-1: G(x0, ..., xn-1) = T}
G[x <- T[x0 <- a0, ..., xn-1 <- an-1]]

Above rule simply tells us that, if a goal contains an elementary term with an explicitly defined function, we are allowed to "insert the definition" of the function:

We have to prove F[x <- G(a0, ..., an-1)]. By definition of G, it suffices to prove G[x <- T[x0 <- a0, ..., xn-1 <- an-1]].

Examples are given by the proofs of Proposition Function Composition and of Proposition Quotient.

Author: Wolfgang Schreiner
Last Modification: October 4, 1999
previous up next