Q:

Mathematical Logic Shoenfield chapter 1 question 5

I'm working through Mathematical Logic by Joseph Shoenfield. I have finished reading chapter 1 and I'm stuck on exercise 5. The question reads
Let $T$ be a thoery with no non-logical symbols and no non logical axioms a) Show that $\neg \neg(x=x) \vee \neg(x=x)$ is a theorem of $T$ non provable without propositional axioms. [hint: let $f$ be a mapping from the set of formulas to the set of truth values such that $f(A) = \textbf{T}$ for $A$ an atomic formula; $f(\neg A) = \textbf{F}$; $f(A \vee B) = f(B)$; $f(\exists xA) = \textbf{T}$. Show that if $A$ is provable without propositional axioms then $f(A) = \textbf{T}$ 
My intuition tells me to use induction on the length of $A$ starting with $A$ being an atomic formula and building up from there. I ran into trouble though because what if you had a proof of a formula that looked like $\neg C \exists xD A$ where C, D and A are formulas. How would you apply f to that? I believe this satisfies Shoenfields definition of a proof on page 5. I'm really unfamiliar with how proofs in logic go and all of my attempts seemed to trivialize the problem. Any help is much appreciated.
Here's a link to a pdf of the book
https://kupdf.com/download/joseph-r-shoenfield-1967-mathematical-logic_58df8baadc0d6036298970da_pdf

A:

The proof is by induction on the lenght of the proof, considering that we have to exclude propositional axioms.
1st step) we have to check that all axioms (except for the propositional ones) are T with the proposed interpretation.
For $x=x$, it' Ok, and also for the other identity axioms, because they are made of atoms and $f(A)=$ T for $A$ atomic.
For the substitution axioms, we are Ok, because $f(\exists x A)=$ T, irrespective of the truth-value of $A$.
2nd step) we have to check that the inference rules are sound, i.e. they produce true conclusions from true premises :

Expansion Rule. Infer $B \lor A$ from $A$.

If $f(A)=$ T, then $f(B \lor A)=f(A)=$ T.

Contraction Rule. Infer $A$ from $A \lor A$. Similar.
Associative Rule. Infer $(A \lor B) \lor C$ from $(A \lor (B \lor C)$. Similar.
Cut Rule. Infer $B \lor C$ from $A \lor B$ and $\lnot A \lor C$.

We have $f(A \lor B)=f(B)=$ T and $f(\lnot A \lor C)=f(C)=$ T; thus $f(B \lor C)=f(C)=$ T.

$\exists$-Introduction Rule. If $x$ is not free in $B$, infer $\exists x A \to B$ from $A \to B$.

We have that $A \to B$ is $\lnot A \lor B$. Thus, $f(A \to B)=f(B)=$ T. And so, $f(\lnot \exists x A \lor B)=f(B)=$ T.
This conclude the proof that if a formula $\varphi$ is provable without propositional axioms, then $f(\varphi)=$ T.
But $f(¬¬(x=x) \lor ¬(x=x))=f(¬(x=x))=$ F, and thus it is not derivable with the said limitation.

