Proof of validity of tautology in first order logic Every first-order logic formula which has a tautological shape in propositional logic is a valid formula. Is it possible to give  a formal proof for the above?
 A: The only way I can make sense of "tautological shape" is to suppose a formula $\psi$ is of the form: $$\psi = \alpha[\phi_1 / p_1, \dots,\phi_n/p_n]$$
where $/$ denotes substitution (adequately defined), for some first-order formulas $\phi_i$ and a propositional tautology $\alpha$ in the variables $p_i$.
Now let $\mathcal M$ be a structure for $\psi$ and let $v: {\sf Var} \to \mathcal M$ be an assignment of variables, both arbitrary.
The crux is to define the boolean interpretation $v': \{p_1,\dots,p_n\} \to \{T,F\}$ by: $$v'(p_i) = \begin{cases}T&\text{ if $\mathcal M,v \models \phi_i$}\\F&\text{ if $\mathcal M, v \not\models \phi_i$}\end{cases}$$
and subsequently demonstrate by induction on the complexity of propositional formulas $\beta$ in the symbols $p_i$ that: $$v'(\beta) = T \iff \mathcal M,v\models \beta[\phi_i/p_i]$$
Having established this equivalence, since $\alpha$ is a tautology, we conclude that $\mathcal M,v \models \psi$ for all structures $\mathcal M$ and assignments $v$; that is, $\psi$ is valid.
A: You might want to have a look at any proper proof of Herbrand's Theorem. There, $\forall \vec{y}\exists \vec{x}\phi_{qf}(\vec{x},\vec{y})$ sentences are transformed into a finite quantifier-free disjunction $\phi_{qf}(\vec{c_x},\vec{t_{1}})\vee\dots\vee\phi_{qf}(\vec{c_x},\vec{t_{n}})$; this disjunction, interpreted as a formula in propositional logic (!), is a tautology if and only if the original sentence was already valid.
The proof of this will contain some justification about the part where the quantifier-free disjunction is interpreted as a propositional formula. Basically, this should be straightforward. You define an injective mapping which assigns propositional variables to atoms such that exactly thos atoms which are syntactically equivalent are assigned the same variables. Then you do some argumentation based on the semantics of first-order and propositional logic; basically, these semantics should coincide for the "propositional" part of first-order logic.
