Prove the soundness of propositional logic without using induction? I want to prove the soundness of propositional logic without using induction. I think I can do that via a process that's basically universal introduction (i.e., demonstrate something about an arbitrary member and infer that it applies universally). As an example of this approach I've picked a new inference rule to prove.
My questions:

*

*Is my approach valid?

*Is my proof correct?

*Is it easy to understand and follow?

*Do I need to add more/less detail?

*How else can I improve it?


Proof
We want to show that $\boxed{\dfrac{\Gamma_1 ,\,\phi\vdash\psi\quad\Gamma_2,\,\lnot\phi\vdash\psi}{\Gamma_1 ,\,\Gamma_2\vdash\psi}}\def\pa {((\Gamma_1\land\phi)\longrightarrow\psi)}
\def\pb {((\Gamma_2\land\lnot\phi)\longrightarrow\psi)}
\def\ca {((\Gamma_1\land\Gamma_2)\longrightarrow\psi)}
\def\lto {\longrightarrow} \def\val#1{V_\mathscr{I}( #1 )}
\def\pli {\text{PL-interpretation, $
$\mathscr{I}$},} \def\inp{\mathscr{I}}$ is a truth preserving inference rule without using induction. To do so we'll convert the rule to an axiom schema and show that it's valid.
Conversion Rules
Symbols

*

*"," and the "$\quad$" convert to conjunction

*"$\vdash$" and the vinculum convert to implication

*$\Gamma$, with or without subscript, is a finite set of conjoined wffs, so it's simply a wff with it's own valuation rules

Valuation of $\Gamma$

*

*$\val{\Gamma}=1$ iff, for all $\gamma\in\Gamma$, it's the case that $\val{\gamma}=1$ and $\Gamma\neq\emptyset$
Conversion

*

*$\Gamma_1 ,\,\phi\vdash\psi:= \pa$


*$\Gamma_2,\,\lnot\phi\vdash\psi:= \pb$


*$\Gamma_1 ,\,\Gamma_2\vdash\psi:= \ca$


*Putting it all together, the rule converts to - $\boxed{((\pa\land\pb)\lto\ca)}$
Proof that the axiom schema is valid

*

*Assume for reductio that $\val {((\pa\land\pb)\lto\ca)}=0$


*It follows from (1) that $\val {\ca}=0$


*It follows from (2) that $\val{\Gamma_1}=1$, $\val{\Gamma_2}=1$, and $\val{\psi}=0$


*It follows from (1) that $\val{\pa}=1$


*It follows from (3) and (4) that $\val{\phi}=0$


*It follows from (5) that $\val{\lnot\phi}=1$


*It follows from (1) that $\val{\pb}=1$


*It follows from (3) and (6) that $\val{\pb}=0$, which contradicts (7) $\boxed{}$
Example Proof
$\begin{array}{lrcll}
1.&\phi&\vdash &\phi &\text{RA}\\
2.&\phi&\vdash &\lnot\psi\lor\phi &\text{1, $\lor$I}\\
3.&\phi&\vdash &\psi\to\phi &\text{2, Abbrv}\\
4.&\phi&\vdash & (\phi\to\psi)\lor(\psi\to\phi) &\text{3, $\lor$ I}\\
5.&\lnot\phi&\vdash &\lnot\phi &\text{RA}\\
6.&\lnot\phi&\vdash &\lnot\phi\lor\psi &\text{5, $\lor$I}\\
7.&\lnot\phi&\vdash &\phi\to\psi &\text{6, Abbrv}\\
8.&\lnot\phi&\vdash & (\phi\to\psi)\lor(\psi\to\phi) &\text{7, $\lor$ I}\\
9.&\emptyset &\vdash & (\phi\to\psi)\lor(\psi\to\phi) &\text{4, 8 New Rule}\\
\end{array}$
 A: It's easier to use Heyting algebra lattice model to understand the usual induction proof on the height of derivations of soundness in both intuitionistic and classical logic. And every Boolean algebra is a Heyting algebra which is also distributive.

In mathematics, a Heyting algebra (also known as pseudo-Boolean algebra) is a bounded lattice (with join and meet operations written ∨ and ∧ and with least element 0 and greatest element 1) equipped with a binary operation a → b of implication such that (c ∧ a) ≤ b is equivalent to c ≤ (a → b).

In the link there's a lattice diagram, every natural deduction rule of each connective can be checked to preserve the order of such lattice according to the lattice formation definitions. But you still need to climb up the lattice for an arbitrary derivation with finite steps. But this height in the lattice doesn't correspond to the entities or terms of the domain of discourse of such a structure, so you cannot invoke "universal introduction" as a natural deduction inference rule. Back in territory with your valuation function, this height complexity corresponds to  the individual step of your proof which is not an entity of its domain of discourse (thus no universal introduction applicable here), so induction seems necessary here.
