Predicated needed for proof using structural induction

Question

I have a set, $F$, of boolean formulas defined inductively as follows:

$X_{i} \in F, \: \forall i \in \mathbb{N} \: \text{(variables)}\\ A \in F \implies \neg A \in F\\ A, B \in F \implies A \land B \in F\\ A, B \in F \implies A \lor B \in F$

I also have the mutually recursive functions $T$, $N: F \rightarrow F$ where:

$T(A \land B) = T(A) \land T(B)\\ T(A \lor B) = T(A) \lor T(B)\\ T(\neg A) = N(A)\\ T(X_{i}) = X_{i}\\ \:\\ N(A \land B) = N(A) \lor N(B)\\ N(A \lor B) = N(A) \land N(B)\\ N(\neg A) = T(A)\\ N(X_{i}) = \neg X_{i}$

I need to show, using structural induction on the definition of $F$, that $\forall A \in F$:

$T(A) \iff A$ "and has negation only on variables"

The suggestion is to define a stronger predicate that also makes a statement about $N$. I cannot seem to come up with a suitable predicate and I am not entirely sure what the qualification "and has negation only on variables" means. Structural induction itself is not a problem.

Any advice is appreciated.

EDIT:

Later, I realized that the qualification "has negation only on variables" must mean "has negation only on arguments to $T$ and $N$" and not the "variables" $X_{i}$.

Answer 1

$T$ is a transformation with the property that :

for all boolean formula $A \in \mathcal F$, $T(A) \leftrightarrow A$ and $T(A)$ has all the negation signs "pushed inside", i.e. in front of boolean variables $X_i$.

Basis of induction : $A = X_i$

$T(A)=T(X_i)=X_i$, by definition of $T$. Thus, $T(A)$ has all negation signs (there are none) in front of variables and $T(A)=X_i \leftrightarrow X_i=A$.

Induction step : the induction is on the number of connectives of $A$.

($1$) $A = \lnot B$; thus : $T(A)=T(\lnot B)=N(B)$.

Now we have to consider four sub-cases :

($1_{atomic}$) : $B = X_i$.

$T(A)=N(B)=N(X_i)=\lnot X_i$ and so : $T(A)=\lnot X_i$ has all the negation signs in front of variables.

But $T(A) = \lnot X_i \leftrightarrow \lnot B=A$ and we are done.

($1_{\lnot}$) : $B = \lnot C$.

$T(A)=N(B)=N(\lnot C)=T(C)$; $C$ has two connectives less than $A$ and thus the induction hypotheses apply, i.e. $T(C) \leftrightarrow C$ and $T(C)$ has all the negation signs "pushed inside".

Now, $A=\lnot B=\lnot \lnot C \leftrightarrow C$ and : $T(A)=T(C)$ and so : $T(A) \leftrightarrow C \leftrightarrow A$ and $T(A)$ (i.e. $T(C)$) has all negation signs in front of variables.

($1_{\land}$) : $B = C \land D$.

$T(A)=N(B)=N(C \land D)=N(C) \lor N(D)$ and $N(C)=T(\lnot C)$ and $N(D)=T(\lnot D)$. But $C$ and $D$ has two conncetives less than $A$ and thus the induction hypotheses apply to both $\lnot C$ and $\lnot D$, i.e. $T(\lnot C) \leftrightarrow \lnot C$ and $T(\lnot C)$ has all the negation signs "pushed inside", and the same for $T(\lnot D)$.

Thus $T(A)=N(B)=T(\lnot C) \lor T(\lnot D) \leftrightarrow \lnot C \lor \lnot D$ and $T(A)$ has all negation signs in front of variables, because so are $T(\lnot C)$ and $T(\lnot D)$ and the $\lor$ connective does not introduce any new negation sign.

But $T(A)=T(\lnot C) \lor T(\lnot D) \leftrightarrow \lnot C \lor \lnot D \leftrightarrow \lnot(C \land D) \leftrightarrow \lnot B=A$, and it's done.

($1_{\lor}$) : $B = C \lor D$.

Similar to ($1_{\land}$).

In the same way we can manage the other cases needed to complete the induction step :

($2$) $A = C \land D$.

($3$) $A = C \lor D$.