Assume we have a construction sequence ending in \(\varepsilon_n\), where \(\varepsilon_n\) does not contain the symbol \(A_4\). Suppose we delete all the expressions in the construction sequence that contain \(A_4\). Show that the result is still a legal construction sequence.

Let \(C = \langle \varepsilon_1,\ldots,\varepsilon_n\rangle\) be the construction sequence. Let \(C' = \langle \varepsilon_{k_1},\ldots,\varepsilon_{k_m}\rangle\) be the same sequence but with all expressions containing \(A_4\) deleted and re-indexed. We have that \(m\geq 1\) since \(\varepsilon_n\) does not contain \(A_4\), and that \(\varepsilon_{k_m} = \varepsilon_n\)

Consider \(\varepsilon_{k_i}\) an arbitrary element in the sequence \(C'\). Since \(\varepsilon_{k_i}\) is also a member of the original construction sequence \(C\), we have the following three cases to consider.

Case 1: \(\varepsilon_{k_i}=\varepsilon_\lnot(\varepsilon_{j})\) for some \(j < k_i\)

Since \(\varepsilon_{k_i}\) contains no \(A_4\) symbol and the operation of logical negation does not add an \(A_4\) symbol, it must be that \(\varepsilon_j\) does not contain \(A_4\) either. Thus, \(\varepsilon_j\) is present in the sequence \(C'\), meaning \(\varepsilon_{k_i} = \varepsilon_\lnot(\varepsilon_{k_r})\) for some \(r < i\)

Case 2: \(\varepsilon_{k_i} = \varepsilon_\square(\varepsilon_j,\varepsilon_r)\) for some \(j,r<k_i\), where \(\square\) is one of \(\to,\leftrightarrow,\land,\lor\)

Since \(\varepsilon_{k_i}\) contains no \(A_4\) symbol, and the operation \(\varepsilon_\square(\cdot,\cdot)\) does not introduce an \(A_4\) symbol, it must be that \(\varepsilon_j\) and \(\varepsilon_r\) do not contain \(A_4\). Thus, \(\varepsilon_j\) and \(\varepsilon_r\) are present in the sequence \(C'\), meaning \(\varepsilon_{k_i} = \varepsilon_\square(\varepsilon_{k_s},\varepsilon_{k_p})\) where \(s,p < i\).

Case 3: \(\varepsilon_{k_i}\) is a sentence symbol

This case requires no further attention, we already know it does not contain \(A_4\)

From considering the arbitrary symbol \(\varepsilon_{k_i}\) from \(C\) as a member of its parent sequence \(C'\), we see that it follows the rules established for legal construction sequences. Thus, \(C'\) is a legal sequence.