Definition: Linear Independence
edit
In the language of first-order logic , the set of functions
{
f
1
,
f
2
,
.
.
.
,
f
N
}
{\displaystyle \{f_{1},f_{2},...,f_{N}\}\,}
is linearly independent , over the interval
Ω
{\displaystyle \Omega \,}
in
R
{\displaystyle \mathbb {R} }
, iff :
∀
α
.
[
[
α
∈
R
n
.
α
≠
0
]
→
[
∃
x
∈
Ω
.
¬
P
(
α
,
x
)
]
]
{\displaystyle \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
(
α
,
x
)
≡
∑
i
=
1
n
α
i
f
i
(
x
)
=
0
{\displaystyle P({\boldsymbol {\alpha }},x)\,\equiv \,\sum _{i=1}^{n}\alpha _{i}\,f_{i}(x)=0}
. Expressed in disjunctive normal form the above definition reads:
L
I
(
Ω
)
≡
∀
α
.
[
α
∉
R
n
∨
α
=
0
∨
∃
x
∈
Ω
.
¬
P
(
α
,
x
)
]
{\displaystyle 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
L
I
(
Ω
)
{\displaystyle LI(\Omega )\!}
represents the words occurring before the iff .
Theorem: The Wronskian and Linear Independence
edit
∀
Ω
.
[
∃
y
∈
Ω
.
W
(
y
)
≠
0
→
L
I
(
Ω
)
]
{\displaystyle \forall \Omega .\,{\Big [}\,\exists y\in \Omega .\,W(y)\neq 0\,\to \,LI(\Omega )\,{\Big ]}}
,
i.e.,
∀
Ω
.
[
∀
y
.
[
y
∉
Ω
∨
W
(
y
)
=
0
]
∨
L
I
(
Ω
)
]
{\displaystyle \forall \Omega .\,{\bigg [}\,\forall y.\,{\Big [}\,y\notin \Omega \,\lor \,W(y)=0\,{\Big ]}\lor LI(\Omega )\,{\bigg ]}}
.
(I)
A
⊢
{\displaystyle \vdash }
A p ≡ q
(¬R)
⊢
{\displaystyle \vdash }
¬A, A
(CR)
⊢
{\displaystyle \vdash }
A
∨
{\displaystyle \lor }
¬A
A typical rule is:
Γ
⊢
Σ
Γ
,
α
⊢
Σ
α
,
Γ
⊢
Σ
{\displaystyle {\frac {\Gamma \vdash \Sigma }{\begin{matrix}\Gamma ,\alpha \vdash \Sigma &\alpha ,\Gamma \vdash \Sigma \end{matrix}}}}
This indicates that if we can deduce
Σ
{\displaystyle \Sigma }
from
Γ
{\displaystyle \Gamma }
, we can also deduce it from
Γ
{\displaystyle \Gamma }
together with
α
.
{\displaystyle \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:
Γ
⊢
{\displaystyle \vdash }
A
∨
{\displaystyle \lor }
B, Δ
Γ
⊢
{\displaystyle \vdash }
B
∨
{\displaystyle \lor }
A, Δ
Good
(
1
2
)
{\displaystyle \left({\frac {1}{2}}\right)}