Substituting statement form (well formed formula) for statement letter (propositional variable) in tautology My question is about propositional calculus. Assume we are given statement forms $A,B$ and statement letter $a$. The word $C$ arises from substituting statement form $B$ for every occurence of statement letter $a$ in statement form $A$. I want to prove that $C$ is a statement form and moreover if $A$ is a tautology, then so is $C$.
I suppose this should be done using some form of structural induction. This is one theorem I know, which results from my definition of statement form:
If $\mathcal{F}$ is a set consisting of words such that


*

*All statement letters belong to $\mathcal{F}$

*If $A,B\in \mathcal{F}$, then $(\neg A),(A\wedge B),(A\vee B), (A\rightarrow B),(A\leftrightarrow B\in\mathcal{F})$.


, then all statement forms belong to $\mathcal{F}$.
However I don't know how to apply it here.
Besides I'm not quite sure if I understand correctly the concept of tautology. This is how I understand it:
If we denote the set of statement letters by $\sigma$, then we can extend an arbitrary function $v_0:\sigma\rightarrow\{T,F\}$, to a unique function $v:\mathcal{F}_0\rightarrow\{T,F\}$ on the set $\mathcal{F}_0$ of all statement forms in such way that whenever we have a statement forms $A,B$ the values $v(\neg A),v(A\wedge B),v(A\vee B),v(A\rightarrow B),v(A\leftrightarrow B)$ agree with the corresponding truth tables. And we say that $A$ is a tautology iff for all functions $v_0$, $v(A)=T$. Is my understanding correct here?
 A: Your understanding of tautology is correct. The two important things to note about it in this case are 1) for any propositional variable $a$ and assignment $v_0:\sigma\to\{T,F\}$, there is another assignment $v'_0 : \sigma\to\{T,F\}$ which differs from $v_0$ only for $a$, and 2) from $v_0$, $v:\mathcal F\to\{T,F\}$ is defined structurally recursively so $v(A)$ for some formula $A$ depends only on the truth value of $A$'s direct subformulas and not on their structure, e.g. $v(A\land B)$ depends only on $v(A)$ and $v(B)$ and not (directly) on the structure of $A$ and $B$.
Since the set of well-formed formulas is inductively defined, we have a structural induction rule which states: for any (meta-logical) property $P$ of well-formed formulas if we want to show that $P$ holds for all well-formed formulas, then it suffices to show that $P$ holds for propositional variables and for each case of top level connective where we are allowed to assume $P$ holds for the direct subformulas in those cases. For example, one case would be showing that $P(A\land B)$ holds for arbitrary formulas $A$ and $B$ for which we can assume $P(A)$ and $P(B)$ hold.
Write $A[C/a]$ for the substitution of the formula $C$ for the propositional variable $a$ in the formula $A$. This can be defined by structural recursion as follow: $b[C/a] =\begin{cases}C, &\text{if } b = a\\b, &\text{if }b\neq a\end{cases}$, $(\neg A)[C/a]=\neg(A[C/a])$, and $(A\circ B)[C/a]=A[C/a]\circ B[C/a]$ where $\circ$ stands for any binary connective. It is easy to see (but you should spell it out yourself) that all the cases for showing that $A[C/a]$ is a well-formed formula (given $A$ and $C$ are) are trivial except for the propositional case. For $b[C/a]$, either $b\neq a$ in which case $b[C/a]=b$ and is a well-formed formula by definition, or $b=a$ and $b[C/a]=C$ which is well-formed by assumption. Next, we show that $A[C/a]$ is a tautology whenever $A$ is, i.e. that if for all $v_0:\sigma\to\{T,F\}$, $v(A)=T$, then for all $v_0:\sigma\to\{T,F\}$, $v(A[C/a])=T$. The idea is to show that, given any $v_0:\sigma\to\{T,F\}$, if we define $v'_0$ as $v_0$ except $v'_0(a)=v(C)$, then $v'(A)=v'(A[C/a])$. This can be proven by structural induction and again every case is trivial except the propositional variable case. We need to show $v'(b)=v'(b[C/a])$ for a propositional variable $b$. If $b\neq a$ then $b[C/a]=b$ and this is trivial. If $b=a$ then $b[C/a]=C$ and we get $v'(b)=v'(C)$ which is true by definition of $v'$. We need a small lemma first to complete the proof. Namely, that if the propositional variable $a$ does not occur in the formula $A$, then $v(A)=v'(A)$ where $v_0$ and $v'_0$ differ only on $a$. This can be proven itself by a very easy structural induction. We now prove almost the result. If $C$ does not contain $a$ and $A$ is a tautology, then $A[C/a]$ is a tautology. For any $v_0$, define $v'$ as above, then we have $T=v'(A)=v'(A[C/a])=v(A[C/a])$. The first equality is because $A$ is a tautology. The second is by the previous result. Finally, the third is by the lemma because $A[C/a]$ does not contain $a$. To get the general result, simply write $A[C/a]$ as $A[z/a][C/z]$ where $z$ is a propositional variable that does not occur in $A$ or $C$. (You can use structural induction to prove that $A[z/a][C/z]=A[C/a]$.)
An algebraic perspective can organize this a bit. The set of well-formed formulas with propositional variables in $\sigma$ is the (absolutely) free algebra with operators $\neg$, $\land$, $\lor$, $\to$, and $\leftrightarrow$ generated from the set $\sigma$. An algebra for this signature is a set $X$ and interpretations for each of the operators, e.g. $\neg_X : X \to X$ and $\land_X : X\times X \to X$. A homomorphism $h$ of an algebra $X$ to an algebra $Y$ is a function $X\to Y$ such that $h(\neg_X x)=\neg_Y h(x)$ and $h(x\circ_X x')=h(x)\circ_Y h(x')$ where $\circ$ stands for each of the binary operators. Write $T(\sigma)$ for the (free) algebra of well-formed formulas generated from $\sigma$. What makes it a free algebra is the following property (which fully characterizes it): given an algebra $X$ and any (arbitrary) function $f_0:\sigma \to X$, then there is a unique homomorphism $f:T(\sigma)\to X$ such that $f$ agrees with $f_0$ on $\sigma$. We have the algebra $\mathbb B=\{T,F\}$ equipped with the usual Boolean interpretation of the operators. A valuation $v$ is the unique homomorphism $T(\sigma)\to\mathbb B$ induced by the function $v_0:\sigma\to\mathbb B$. If $a\notin\sigma$ and $C\in T(\sigma)$, then $\_[C/a]:T(\sigma\cup\{a\})\to T(\sigma)$ is the unique homomorphism determined by the function $\sigma\cup\{a\}\to T(\sigma)$ that is the identity except that it maps $a$ to $C$.
A: Consider any sequence which shows that a string is a tautology.  Now, consider the same sequence, but instead of the letter you will substitute with a statement form, you put in the formula instead for every occurrence of that letter in the sequence.  Since, the formula substituted is a statement form, each step in the sequence remains valid.  The resultant formula at the end of the sequence consists of the desired substitution, and thus we have a similar sequence which shows it a statement form.
For example, say we have a sequence like 
A 
B
C 
(A$\land$B)
((A$\land$B)$\lor$C).  
Now say we substitute B with ((A$\land$B)$\lor$C).  Then the resultant sequence, substituting each B with ((A$\land$B)$\lor$C) is 
A 
((A$\land$B)$\lor$C) 
C 
(A$\land$((A$\land$B)$\lor$C)) 
((A$\land$((A$\land$B)$\lor$C))$\lor$C)
I think your definition of tautology works.  For all consistent truth values assigned to the letters of the statement form, a tautology is true.  Since any substitution for a letter is a statement form, and all statement forms compute to either true or false, and such substitution happens uniformly throughout the statement form, it follows that a substitution will yield a tautology.  Substitution will also take a contradiction and yield a contradiction.  Substitution in infix notation begins to run into problems if you drop parentheses, but the definition of a statement form and the definition of a substitution prohibits doing such.  Substitution doesn't have the same sorts of problems with parentheses in prefix or postfix notational schemes.
