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.

Aug 21 2020

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

1 shibai Aug 21 2020 at 14:15

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:

  1. $\langle \forall x :: P.x\rangle\land\langle \exists x :: Q.x\rangle$ (presupposto per intro di implicazione)
  2. $\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)
  3. $\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$)

GrahamKemp Aug 21 2020 at 07:03

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}$$