I have a formal language (basically language of first order logic) in which Wffs are defined by following.
String $A$ is a Wff if it satisfies one of:
- $A$ is atomic
- $A \equiv (\lnot B)$ and $B$ is a Wff
- $A \equiv (B \implies C)$ and $B$ and $C$ are Wffs
- $A \equiv ((\forall x) B)$ and $B$ is a Wff in which $x$ appears free and $(\forall x)$ does not appear in $B$.
I've defined (recursively) a function which returns the "depth" of a Wff so that I can do metalogical induction on this depth or complexity.
- If $A$ is atomic the $D(A) = 0$
- If $A \equiv (\lnot B)$ then $D(A) = D(B) + 1$
- If $A \equiv (B \implies C)$ then $D(A) = \text{max}(D(B), D(C)) + 1$
- If $A \equiv ((\forall x) B)$ then $D(A) = D(B) + 1$
Finally, I've recursively defined some functions that return a sort of parse tree for a Wff $A$. The idea is I want an object (this parse tree) which contains all sub-Wffs of $A$ along with a unique identifier for each sub-Wff. In this case the unique identifier is a tuple of numbers, the first specifying the depth of the sub Wff and the latter specifying the "branch number" for the subWff. The function $C(A)$ extracts the decedents of $A$ within this parse tree structure.
- If $A$ is atomic then $C(A) = \emptyset$
- If $A \equiv (\lnot B)$ then $C(A) = \{(B, 1, 1, \lnot)\} \cup C_{+1, +0}(B)$
- If $A \equiv (B\implies C)$ then $C(A) = \{(B, 1, 1, \implies_L), (C, 1, b+1, \implies_R\} \cup C_{+1, +0}(B) \cup C_{+1, +b}(C)$ with $b$ the maximum branch number appearing in $C(B)$ (or $b=1$ if $C(B)$ is empty).
- If $A \equiv ((\forall x) B)$ then $C(A) = \{(B, 1, 1, \forall x)\} \cup C_{+1, +0}(B)$.
The notation $C_{+n, +m}(B)$ indicates the set $C(B)$ where all depth numbers have been incremented up by $n$ and all branch numbers have been incremented up by $m$.
The total parse tree for $A$ is
$$ T(A) = \{(A, 0, 1, \text{Wff})\} \cup C(A) $$
I've already proven that all (depth, branch) tuples in $T(A)$ are unique. I include the symbols and connectives such as $\lnot$ and $\implies$ in $T(A)$ so that I could in principle recreate the Wff $A$ from $T(A)$. Though I don't think this is needed for what follows.
Question
I am trying to prove that if Wff $P$ appears in $T(A)$ with depth/branch tuple $(n, m)$ that one of the following holds:
- $P \equiv A$
- $(\lnot P)$ appears in $T(A)$ at $(n-1, m)$
- $(P \implies B)$ appears in $T(A)$ at $(n-1, m)$
- $(B \implies P)$ appears in $T(A)$ at $(n-1, m-k)$ with $k$ the maximum branch number in $C(B)$ (with possible off-by-one error here..)
- $((\forall x) P$ appears in $T(A)$ at $(n-1, m)$ for some variable $x$
I'm having a hard time proving this... I think I may still be a few steps away. I think one route that might be effective would be to first prove sort of the inverse, that is things like:
- If $(\lnot P)$ appears at $(n, m)$ then $P$ appears at $(n+1, m)$
I could then use this combined with uniqueness to prove my desired "parenthood" result. I'm having a surprisingly difficult time proving this one also. My definitions feel a little unwieldy.
To that end, I'd appreciate any help in proving these results or refining my definitions to make the proofs easier.
One final note, my goal with this is to come up with a proof of the replacement theorem which states that if $P \equiv Q$ then $A \iff A[Q/P]$ where $A[Q/P]$ loosely notates the replacement of $P$ by $Q$ in the Wff $A$. I'm going through all of the rigor here to more clearly define the replacement of $P$ by $Q$ especially in cases in which $P$ may appear multiple times in $A$.