Mostrando $\langle \forall x:: P.x \rangle \land \langle \exists x:: Q.x \rangle \implies \langle \exists y: P.y : Q.y \rangle $ è un teorema.
Una possibile dimostrazione utilizzando un sistema di deduzione naturale come Fitch non è difficile. Ma vorrei dimostrarlo usando la logica equazionale. Questo sistema utilizza regole comuni di logica proposizionale come DeMorgan, ecc ... e regole di logica predicativa usate in libri come:
- Un approccio logico alla matematica discreta (David Gries).
- Il libro completo può essere trovato qui: https://link.springer.com/book/10.1007/978-1-4757-3837-7
- Elenco delle regole a pagina 503.
- Programmazione negli anni '90 (Edward Cohen).
La mia dimostrazione inizia come segue:
Presumo valga l'antecedente $$\langle \forall x:: P.x \rangle \land \langle \exists x:: Q.x \rangle$$ e prova a raggiungere $$\langle \exists x:: P.x \land Q.x \rangle$$
Prova tentata:
$$ \begin{align*} & \langle \forall x:: P.x \rangle \land \langle \exists x:: Q.x \rangle\\ \implies & \{\text{Instantiation } (\forall)\}\\ & P.a \land \langle \exists x:: Q.x \rangle \\ \equiv & \{\text{Distributivity of} \land \text{over} \exists \} \\ & \langle \exists x:: P.a \land Q.x \rangle \end{align*} $$
Ovviamente la dimostrazione non è completa. Qualcuno sa se questa prova è possibile in questo contesto?
Risposte
Quando si crea una prova formale per un'implicazione logica, è utile ragionarci prima intuitivamente. Questo può anche aiutare a rivelare se una prova parziale su cui stai lavorando porta a un vicolo cieco. Ad esempio, la tua prova parziale si legge intuitivamente come:
Cado $x$ avere proprietà $P.x$ e ce ne sono alcuni $x$ con proprietà $Q.x$, allora ce ne devono essere alcuni $x$ con proprietà $P.x\land Q.x$: anzi, lascia $a$ essere un oggetto arbitrario, allora sappiamo che ha proprietà $P.a$. Poiché ce ne sono alcuni$x$ con proprietà $Q.x$, possiamo concludere che ce ne sono alcuni $x$ con $P.a\land Q.x$... ma adesso cosa?
Ciò rivela che probabilmente non era l'idea migliore per istanziare prima il quantificatore universale, ma piuttosto il quantificatore esistenziale:
Cado $x$ avere proprietà $P.x$ e ce ne sono alcuni $x$ con proprietà $Q.x$, allora ce ne devono essere alcuni $x$ con la proprietà $P.x\land Q.x$: anzi, diciamo l'oggetto con proprietà $Q$ è chiamato $a$ (così che $Q.a$), quindi da allora $x$ avere proprietà $P.x$, quindi soprattutto $a$ deve avere proprietà $P.a$. Combinando questo con il fatto che$a$ ha proprietà $Q.a$, possiamo concludere che $a$ ha proprietà $P.a\land Q.a$. In particolare, ce ne sono alcuni $x$ con $P.x\land Q.x$.
Scriverlo formalmente usando la deduzione naturale sarebbe simile a questo:
- $\langle \forall x :: P.x\rangle\land\langle \exists x :: Q.x\rangle$ (presupposto per intro di implicazione)
- $\langle \exists x :: Q.x\rangle$(congiunzione elim, 1)
2.1$Q.a$(ipotesi di eliminazione esistenziale)
2.2$\langle \forall x :: P.x\rangle$(congiunzione elim, 1)
2.3$P.a$(universal elim, 2.2)
2.4$P.a\land Q.a$(congiunzione intro, 2.1, 2.3)
2.5$\langle \exists x :: P.x\land Q.x\rangle$ (introduzione esistenziale, 2.4) - $\langle \exists x :: P.x\land Q.x\rangle$ (elim esistenziale, 2, 2.1-2.5)
da cui concludiamo $\langle \forall x :: P.x\rangle\land\langle \exists x :: Q.x\rangle \implies \langle \exists x :: P.x\land Q.x\rangle$ implicitamente intro su 1-3.
Questo argomento guida come produrre un argomento assiomatico. Il trucco principale in questo caso è che un'introduzione esistenziale viene elusa ragionando per avvolgere l'intero argomento nel quantificatore esistenziale. Puoi quindi ragionare nell'ambito di un quantificatore esistenziale proprio come se non ci fosse.
(antecedente) $\langle \forall x :: P.x\rangle\land\langle\exists x :: Q.x\rangle$
$\equiv$ $\langle \forall y :: P.y\rangle\land\langle\exists x :: Q.x\rangle$ (cambio di variabili)
$\equiv$ $\langle \exists x :: \langle \forall y :: P.y\rangle \land Q.x\rangle$ (distributività di $\land$ al di sopra di $\exists$; questo racchiude l'intera affermazione$\exists$)
$\implies$ $\langle \exists x :: P.x \land Q.x \rangle$ (istanziazione di $\forall$ a $x$)
Il trucco sarebbe quello di istanziare specificamente al testimone per l'esistenza.
$${\langle\forall x::P.x\rangle\land\langle\exists x::Q.x\rangle\\\Downarrow~\\\langle\exists x:Q.x:P.x\rangle\land\langle\exists x::Q.x\rangle}$$