User:Ben Spinozoan/Leftovers

Definition: Linear Independence

In the language of first-order logic, the set of functions $\{f_{1},f_{2},...,f_{N}\}\,$ is linearly independent, over the interval $\Omega \,$ in $\mathbb {R}$, iff:

$\forall {\boldsymbol {\alpha }}.\,{\bigg [}{\Big [}\,{\boldsymbol {\alpha }}\in \mathbb {R} ^{n}.\,{\boldsymbol {\alpha }}\neq 0\,{\Big ]}\to \,{\Big [}\,\exists x\in \Omega \,.^{\neg }P({\boldsymbol {\alpha }},x){\Big ]}{\bigg ]}$,

where $P({\boldsymbol {\alpha }},x)\,\equiv \,\sum _{i=1}^{n}\alpha _{i}\,f_{i}(x)=0$. Expressed in disjunctive normal form the above definition reads:

$LI(\Omega )\,\equiv \;\forall {\boldsymbol {\alpha }}.\,{\Big [}\,{\boldsymbol {\alpha }}\notin \mathbb {R} ^{n}\lor \,{\boldsymbol {\alpha }}=0\,\lor \,\exists x\in \Omega \,.^{\neg }P({\boldsymbol {\alpha }},x){\Big ]}$,

in which $LI(\Omega )\!$ represents the words occurring before the iff.

Theorem: The Wronskian and Linear Independence

$\forall \Omega .\,{\Big [}\,\exists y\in \Omega .\,W(y)\neq 0\,\to \,LI(\Omega )\,{\Big ]}$,

i.e.,

$\forall \Omega .\,{\bigg [}\,\forall y.\,{\Big [}\,y\notin \Omega \,\lor \,W(y)=0\,{\Big ]}\lor LI(\Omega )\,{\bigg ]}$.

Proof

	(I)
A$\vdash$A p ≡ q
	(¬R)
$\vdash$¬A, A
	(CR)
$\vdash$ A$\lor$¬A

A typical rule is:

${\frac {\Gamma \vdash \Sigma }{\begin{matrix}\Gamma ,\alpha \vdash \Sigma &\alpha ,\Gamma \vdash \Sigma \end{matrix}}}$

This indicates that if we can deduce $\Sigma$ from $\Gamma$, we can also deduce it from $\Gamma$ together with $\alpha .$

However, one can make syntactic reasoning more convenient by introducing lemmas, i.e. predefined schemes for achieving certain standard derivations. As an example one could show that the following is a legal transformation:

Γ $\vdash$A$\lor$B, Δ

Γ $\vdash$B$\lor$A, Δ

Good $\left({\frac {1}{2}}\right)$