"Show that if $A$ is a formula provable without use of substitution axioms, nonlogical axioms, identity axioms, equality axioms, and the $\exists$ introduction rule, then $A$ is a tautology."
I'm thinking it should be shown that since any truth valuation which preserves the remaining axioms and rules evaluates $A$ as true, a must be true by virtue of $\lor$ and $\lnot$, but unsure of how I can show that this means $A$ is a tautology. (Or that a contraction arises if we see that $A$ must be true by virtue of something other than the empty sequence of formulas) I thought perhaps the prenex form of something provable from those axioms and rules would only have a matrix, and that this would only be true of a tautology, but I'm not convinced this is the case.
The logical axioms of the system are :
1) the propositional axioms : $\lnot A \lor A$
2) the substitution axioms : $A[x/a] \to \exists x A$
3) the identity axioms : $x=x$
4) the equality axioms : $x=y \to fx=fy$ and $x=y \to (Px \to Py)$, etc.
The rules of inference are the four propositional rules, like : $\dfrac {A}{B \lor A}$, and the $\exists$-Introduction rule.
If we consider the sub-system obtained from it removing 2),3),4) and the quantifier rule, we have that every propositional axiom is obviously a tautology [page 21] and the propositional rules of inference are sound, i.e. they preserve truth [page 21].
This means that if a formula $\mathscr A$ is provable in the sub-system above, without non-logical axioms, then $\mathscr A$ will be true in every truth valuation $\text V$ such that $\text V$ satisfies the propositional axioms.
But every valuation $\text V$ satisfies the propositional axioms, and thus, $\text V (\mathscr A) = \text T$, for every $\text V$, i.e. $\mathscr A$ is a tautology.
Obviously, we can formalize the argument above with a proof by induction, but the gist of the proof is the same :
(i) axioms are tautologies;
(ii) at step $i$ in the derivation of formula $\mathscr A$, the formula $\mathscr A_i$ is a direct consequence of premises (that, by Induction Hypotheses are tautologies) by way of one of the propositional rules that preserve truth. Thus, $\mathscr A_i$ is a tautology.