User:Ben Spinozoan/Wronskian&Independence

Proof

• 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 }}.\,{\Big [}{\boldsymbol {\alpha }}\in \mathbb {R} ^{n}\land \,{\boldsymbol {\alpha }}\neq 0\,\to \,\exists x\in \Omega \,.^{\neg }P({\boldsymbol {\alpha }},x){\Big ]}$, where $P({\boldsymbol {\alpha }},x)\equiv {\Bigg [}\sum _{i=1}^{n}\alpha _{i}\,f_{i}(x)=0{\Bigg ]}$.

Expressed in disjunctive normal form (DNF) 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 ]}$,

where $LI(\Omega )$ is shorthand for the statement occurring immediately before the iff (note that negation of $LI(\Omega )$ gives the correct statement for linear dependence).

• The text of our theorem "If the Wronskian is non-zero at some point in an interval, then the functions are linearly independent on the interval", now translates as

$\exists y\in \Omega .\;W(y)\neq 0\,\to \,LI(\Omega )$,

or, in DNF,

$(1)\quad \forall {\boldsymbol {\alpha }}.\,{\bigg [}\,\forall y.\,{\Big [}\,y\notin \Omega \,\lor \,W(y)=0\,{\Big ]}\lor \,{\boldsymbol {\alpha }}\notin \mathbb {R} ^{n}\,\lor \,{\boldsymbol {\alpha }}=0\,\lor \,\exists x\in \Omega \,.^{\neg }P({\boldsymbol {\alpha }},x)\,{\bigg ]}$,

where $W(y)$ is the value of the Wronskian at the point $y$.

• The following statement summarizes the situation when Cramer's rule is applied to the linear system associated with the Wronskian:

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

or,

$(2)\quad \forall {\boldsymbol {\alpha }}.\,{\bigg [}\,\forall x.\,{\Big [}\,x\notin \Omega \,\lor \;W(x)=0\;\lor \,^{\neg }\!P({\boldsymbol {\alpha }},x)\,{\Big ]}\lor \,{\boldsymbol {\alpha }}\notin \mathbb {R} ^{n}\,\lor \,{\boldsymbol {\alpha }}=0\;{\bigg ]}$.

• In first-order logic, the statement $\forall x.\,{\big [}A(x)\lor B(x){\big ]}$, entails the statement $\forall x.A(x)\lor \exists y.B(y)$. Consequently, statement (2) entails statement (1), and the theorem is proved.