Doppia quantificazione

[marco2132k]

Ciao. Ho un dubbio stupidissimo. Mi sto chiedendo se la formula (non alludo a nulla di "formale"; non so nulla di logica)
\[
\tag {1}\label{eqn:prima} \left(\forall x\ldotp x\in S\implies\mathscr{P}x\right)\land\left(\forall y\ldotp y\in T\implies\mathscr{Q}y\right)
\] sia logicamente equivalente a
\[
\tag {2}\label{eqn:seconda} \forall x\ldotp x\in S\implies\left(\forall y\ldotp y\in T\implies\mathscr{P}x\land\mathscr{Q}y\right)
\]

Se \( x\in S \) è vera, allora, che preso \( y\in T \) valga il prodotto dei due predicati, è altrettanto vera; poi, quanto si assuma la \( \ref{eqn:seconda} \), le \( \left(\forall x\ldotp x\in S\implies\mathscr{P}x\right) \) e \( \left(\forall y\ldotp y\in T\implies\mathscr{Q}y\right) \) valgono ancora? Non lo so. Siano \( x\in S \) e \( y\in T \); allora vale il prodotto dei due predicati; ergo \( \ref{eqn:prima} \)? Così però ho dimostrato che la
\[
\tag{3}\label{eqn:terza} \forall x\ldotp\forall y\ldotp\left(x\in S\land y\in T\right)\implies\mathscr{P}x\land\mathscr{Q}y
\] è equivalente a \( \ref{eqn:seconda} \) (come l'analogo per le funzioni), e non che \( \ref{eqn:prima}\iff\ref{eqn:seconda} \).

[ot]La cosa mi serve per una dimostrazione di algebra lineare. In pratica non ho capito come convenga appellarsi al principio di induzione in un certo caso. Ma mi interessa anche di suo.[/ot]

[gugo82]

Scusa, ma che devi dimostrare?
Intendo, qual è il problema di AL da cui sei partito?

[marco2132k]

La cardinalità di un insieme di vettori linearmente indipendenti è non maggiore di quella di un insieme di generatori (mi interessa il caso di uno spazio finitamente generato, appunto).

Mi interessava capire, in questi termini formali, l'enunciato. La dimostraizone del fatto che ogni spazio finitamente generato ammette una base è molto simile (o degli altri risultati classici), ma il procedimento "ricorsivo" che è quello che in questa dimostrazione non sono mai riuscito a formalizzarmi, si riduce elegantemente ad una dimostrazione per induzione.

Ossia (l'ho copiata velocemente da un mio quaderno, mi pare giusta, ma non ho controllato proprio tutti i passaggi). Se \( V \) è uno spazio fintamente generato da \( \left\{v_1,\dots,v_n\right\} \), allora esiste un \( k\leqq n \) tale che \( v_1,\dots,v_k \) è una base di \( V \). Non riporto la dimostrazione mainstream e ti rimando al Lang, dove sono sicuro che ci sia [strike]in quella forma[/strike] in una forma più o meno simile, tanto per rendere l'idea. Sopra intendo dire che la cosa può essere fatta per induzione sul numero di generatori: se è vero che per \( n \) generatori il mio claim regge, e \( V \) è uno spazio \( (n+1) \)-generato, allora ammettere che per nessun \( k\leqq n \) da un suo insieme di generatori si possa estrarre una base è contraddittorio per il fatto che, se \( V=\langle w_1,\dots,w_n,w_{n+1}\rangle \), sarà anche
\[ \alpha_i^{-1}\sum_{j\neq i}\alpha_jv_j=v_i\in\langle v_1,\dots,\hat{v_i},\dots,v_{k+1}\rangle \] per un qualche generatore \( v_i \). \( \square \)

Ecco, cercavo di fare una cosa simile per la dimostrazione del "lemma di scambio".

Però questa è una cosa di geometria che non avrei voluto postare, perché penso di riuscirci senza troppi problemi una volta che mi sia tolto il dubbio per cui ho aperto questa discussione.

edit. Corrette alcune imprecisioni.

[Indrjo Dedej]

"2132k":
non so nulla di logica

Sarebbe l'ora di rimediare un pochino.

[marco2132k]

[ot]Prima o poi lo faccio, giuro (anche perché a unipd c'è un solo corso in tre anni, da quello che ho capito; quindi penso che in ogni caso mi dovrò vedere da solo qualcosa - tra un po')[/ot]

[Indrjo Dedej]

Facciamo che ci arrivi tu: ti ricordo che (lo saprai già perché l'avrai usato un sacco di volte, senza accorgertene) vale:
\[P \Rightarrow (Q \Rightarrow R) \equiv (P \land Q) \Rightarrow R\,.\]
In termini più familiari a te: se io devo dimostrare un teorema della forma \[Q \Rightarrow R\] avendo una proposizione \(P\) vera (perché è un assioma oppure un teorema già dimostrato) che faccio? \(P\) finisce tra le ipotesi insieme a \(Q\) e quello che faccio alla fine è \[(P \land Q) \Rightarrow R\,.\]

[caulacau]

"Indrjo Dedej":Facciamo che ci arrivi tu: ti ricordo che (lo saprai già perché l'avrai usato un sacco di volte, senza accorgertene) vale:
\[P \Rightarrow (Q \Rightarrow R) \equiv (P \land Q) \Rightarrow R\,.\]
In termini più familiari a te: se io devo dimostrare un teorema della forma \[Q \Rightarrow R\] avendo una proposizione \(P\) vera (perché è un assioma oppure un teorema già dimostrato) che faccio? \(P\) finisce tra le ipotesi insieme a \(Q\) e quello che faccio alla fine è \[(P \land Q) \Rightarrow R\,.\]

Questo non è esatto: il motivo per cui le due espressioni booleane sono uguali è che hanno le stesse tavol di verità:

a = BooleanTable[
 Implies[p, Implies[q, r]],
 {p, q, r}
 ]
b = BooleanTable[
 Implies[And[p, q], r],
 {p, q, r}
 ]

E se ora provi a controllare se per caso [inline]a == b[/inline] la risposta è sì.

Comunque complimenti, hai appena scoperto le categorie monoidali chiuse.

[Indrjo Dedej]

Infatti io uso $\equiv$ per dire che hanno le stesse tavole di verità.
Categories, categories everywhere!

[marco2132k]

Sul fatto che \( ((P\land Q)\implies R) \) abbia la stessa tavola di verità di \( (P\implies(Q\implies R)) \) ci sono. Ma non mi sembra vero ciò che chiedo in op:

"marco2132k":la formula
\[ \left(\forall x\ldotp x\in S\implies\mathscr{P}x\right)\land\left(\forall y\ldotp y\in T\implies\mathscr{Q}y\right) \] è logicamente equivalente a
\[ \forall x\ldotp x\in S\implies\left(\forall y\ldotp y\in T\implies\mathscr{P}x\land\mathscr{Q}y\right) \]

o sbaglio?