Part I, Chapter 1: Fundamentals, Section 1.2

§ 1.2) Panel Sequence Theorem

It is now possible to define our first theorem. Panel P1 containing a finite
subset of elements e1...et, 1≤t≤m, implies a final panel Pm.

1.2.1) Proof:

By the Axiom of Extension (§ 1.1.4) we have a set of elements defined by the property that each en+1 follows sequentially from en, where 1≤n≤t, on the set of well-formed formulae e1 to et.

Lemma 1:

1. Given e1, and e1 ⊃ e2, therefore e2. (modus ponens)
2. en-1 ⊃ en
3. et ⊃ et+1
4. e1, e2, ..., et, et+1,...,em-1 ⊢ em ▮.

This is true by the Deduction Theorem of the propositional calculus.

Now, given Pn = {e1, e2, ..., et}, let us define Pn+1 = {et+1, et+2, ..., es}, s ≤ m-1.

Let us write x as a variable that takes on values e1,..., et and satisfies the conditions for Pn. Then the definition of Pn becomes a predicate Pn(x) and all et in Pn can be written as the statement: ∀xPn(x).

Now, given Lemma 1:

1. Pn(et) ⊃ Pn+1(et+1)
   

So:

1. ∀x1Pn(x1) ⊃ ∀x2Pn+1(x2); x2 = {et+1, et+2, ..., es}
2. ∴ Pn(x1) ⊃ Pn+1(x2)
3. ∴ Pn(x1) ⊃ Pn+1(x2) ⊃... Pm-1(xm-1) ⊢ Pm(xm) ▮.

1.2.2) Corollary to the Panel Sequence Theorem.

Given t=m, the Axiom of Completion implies P1 = Pm.
That is, the panel containing all elements e1...em contained within L is
the the only and final panel. Let us call this the Identity Panel PI.

1.2.2.1) Proof:

1. ∀x1P1(x1) ⊃ ∀x2Pn+1(x2)
2. x1= e1, e2..., em = xm
   
3. ∀xmP1(xm) ⊃ ∀xmP2(xm+1) . ⊃ f (Axiom of Completion, §1.1.5)
   
4. ∀xmP1(xm) ⊃ ∀xmP2(xm+1) . ⊃ f . ⊃ ∀xmP1(xm) = ∀xmPm(xm)
5. ∴ P1=Pm
6. ⊢P1(xm) : PI ▮.

1.2.3) Summary

Having proved that Pn+1 necessarily follows from Pn, we arrive at the logical conclusion that if we are to assume that the set of et is orderly, then having exhausted all e1...et within Pn, one must continue on to Pn+1 until one has reached Pm. Essentially, if the elements are finite and ordered, then the panels must also be finite and ordered.