Not logged in. Login

Wang Algorithm Example

Let us consider the details of applying the Wang algorithm to verification of modus ponens: \(((P \implies Q) \wedge P) \implies Q\).

Here, the initial proof conjecture has this formula as the single goal, and an empty hypothesis list. Because the hypothesis list is empty, we are assuming nothing. If we can verify the goal formula in this case, the goal is indeed a tautology.

Conjecture 1

\(\texttt{[} \texttt{]} \vdash \texttt{[} ((P \implies Q) \wedge P) \implies Q \texttt{]}\)

Step 1

We only have a single formula, an implication on the goal list. So our only choice is to apply Rule 5b of the Wang algorithm.

Rule 5b: \(H \vdash G, f_1 \implies f_2 \quad \text{reduces to} \quad H, f_1 \vdash G, f_2 \)

Here, the variables of the rule work as follows.

  • \(H = \texttt{[} \texttt{]}\)
  • \(G = \texttt{[} \texttt{]}\)
  • \(f_1 = (P \implies Q) \wedge P\)
  • \(f_2 = Q\).

Applying the rule gives us a new proof conjecture.

Conjecture 1.1: \(\texttt{[} (P \implies Q) \wedge P \texttt{]} \vdash \texttt{[} Q \texttt{]} \)

If Conjecture 1.1 becomes proven, then Conjecture 1 is proven by Rule 5b.

Step 2

Looking at this conjecture, we don't have any propositions in common, so we can't apply Rule 1a and we have a composite formula on the hypothesis list, so we can't apply Rule 1b.

Our only option is to apply Rule 3a for an conjunction on the hypothesis list.

Rule 3a: \(H, f_1 \wedge f_2 \vdash G \quad \text{reduces to} \quad H, f_1, f_2 \vdash G\)

Here, the variables of rule 3a work out as follows.

  • \(H = \texttt{[} \texttt{]}\)
  • \(f_1 = P \implies Q \)
  • \(f_2 = P\).
  • \(G = \texttt{[} Q \texttt{]}\)

Applying the rule gives us our next proof conjecture.

Conjecture 1.1.1: \(\texttt{[} P \implies Q, P \texttt{]} \vdash \texttt{[} Q \texttt{]} \)

Step 3

We again cannot apply the terminating rules (1a or 1b). We recognize an implication on the hypothesis list, so we apply rule 5a.

Rule 5a: \(H, f_1 \implies f_2 \vdash G \quad \text{reduces to} \quad H, f_2 \vdash G \quad \text{and} \quad H \vdash G, f_1\)

The variables of rule 31 work out as follows.

  • \(H = \texttt{[} P \texttt{]}\)
  • \(f_1 = P \)
  • \(f_2 = Q \)
  • \(G = \texttt{[} Q \texttt{]}\)

Applying the rule gives the following pair of proof conjectures that must both be proven.

Conjecture 1.1.1.1: \(\texttt{[} P, Q \texttt{]} \vdash \texttt{[} Q \texttt{]} \)

Conjecture 1.1.1.2: \(\texttt{[} P \texttt{]} \vdash \texttt{[} Q, P \texttt{]} \)

Step 4

We look at Conjecture 1.1.1.1 and see that we have a common proposition \(Q\) in the goal and hypothesis lists.

Conjecture 1.1.1.1 is proven by Rule 1a.

Step 5

We look at Conjecture 1.1.1.2 and see that we have a common proposition \(P\) in the goal and hypothesis lists.

Conjecture 1.1.1.2 is proven by Rule 1a.

  • With conjectures 1.1.1.1 and 1.1.1.2 proven, conjecture 1.1.1 is now established by rule 5a.
  • With conjecture 1.1.1 proven, conjecture 1.1 is now established by rule 3a.
  • With conjecture 1.1 proven, conjecture 1 is now established by rule 5b.

We are done!

Updated Sat Sept. 01 2018, 18:24 by cameron.