Cosa significa "provare"?

Question

Cosa significa "provare"?

Sto usando i seguenti esempi per comprendere i casi generali. Non so come articolare le mie domande nel caso generale. Mi chiedevo a quali livelli vengono dichiarati i seguenti, come vengono formulati i seguenti e quali differenze e relazioni ci sono tra loro:

1. Prova una formula $p$. Significa dimostrare$ \vdash p$ (o $\models p$?), e quindi convertire l'attività in 3 di seguito? (Potrei averlo chiesto in qualche commento, e qualcuno potrebbe aver risposto dimostrando$p$ significa dimostrare $\vdash p$, ma non riesco a trovare i commenti.)

2. Dimostra se $\phi$, poi $\psi$. Che significa provare:$\phi \to \psi$, $\phi \vdash \psi$, o $\phi \models \psi$e quindi convertire l'attività in 1 sopra o 3 sotto?

3. Dimostralo $\phi \vdash \psi$.

   • Significa derivare $\phi \vdash \psi$, utilizzando le regole di inferenza e gli assiomi in un dato sistema di dimostrazione (ad es. calcolo sequenziale)?

   • O tratta $\phi \vdash \psi$ come formula in una lingua a un livello superiore rispetto alla lingua che contiene $\phi$ e $\psi$e dimostrare $\vdash (\phi \vdash \psi)$ applicando un dato sistema di dimostrazione (ad es. calcolo sequenziale) a questo linguaggio di livello superiore?

4. Dimostra se $\phi' \vdash \psi'$, poi $\phi \vdash \psi$.

   • Significa derivare $\phi \vdash \psi$, usando $\phi' \vdash \psi'$, e le regole di inferenza e gli assiomi in un dato sistema di dimostrazione (ad es. calcolo sequenziale)?

   • O tratta $\phi' \vdash \psi'$ e $\phi \vdash \psi$ come formule in una lingua a un livello superiore rispetto alla lingua che contiene $\phi$, $\psi$, $\phi'$ e $\psi'$e dimostrare $(\phi' \vdash \psi') \vdash (\phi \vdash \psi)$ applicando un dato sistema di dimostrazione (ad es. calcolo sequenziale) a questo linguaggio di livello superiore?

5. e 6. Considerare la sostituzione $\vdash$ con $\models$ in 3 e 4

Qualcosa di correlato: ho chiesto :

"Dimostrabile" o "disprovabile" si applica solo a formule, non a "inferenza" o "derivazione" come $∃𝑥𝑅𝑥⊢∀𝑦𝑅𝑦$? Possiamo riscrivere$∃𝑥𝑅𝑥⊢∀𝑦𝑅𝑦$ come formula, in modo che sia derivabile (quasi) se e solo se la formula corrispondente è dimostrabile?

Lemontree ha risposto :

"Provable" significa "derivabile senza premesse", cioè, la provabilità è una proprietà delle formule mentre la derivabilità è una proprietà delle inferenze in generale. Quello che stai cercando è probabilmente il teorema di deduzione noto anche come teorema di import-export, che lo afferma$𝐴_1,…,𝐴_𝑛⊢𝐵$ se e solo se $⊢(𝐴_1∧…∧𝐴_𝑛)→𝐵$. Quindi, con$∃𝑥𝑅(𝑥)⊬∀𝑦𝑅(𝑦)$ ce l'abbiamo $⊬∃𝑥𝑅(𝑥)→∀𝑦𝑅(𝑦)$, cioè la formula $∃𝑥𝑅(𝑥)→∀𝑦𝑅(𝑦)$ non è dimostrabile.

Immagino che le mie domande sopra siano una cosa del metalinguaggio , o teoria della prova, e io ne so poco. Allo stesso tempo, mi chiedevo anche come vengono formulate le tecniche di dimostrazione nella logica matematica? , che potrebbe essere parte della teoria della dimostrazione?

Grazie.

Answer 1

"Dimostrare" in matematica significa scrivere una prova di un'affermazione nel contesto di una teoria matematica. Una dimostrazione sarà un "argomento" che parte dagli assiomi della teoria e dei precedenti risultati provati e si conclude con l'affermazione da dimostrare che utilizza passaggi deduttivi "corretti" logici (cioè un argomento valido ).

Nella logica abbiamo il concetto di derivazione, ovvero il modello matematico formale di una dimostrazione nel contesto di un calcolo logico, ad esempio la deduzione naturale .

I passaggi logici deduttivi sono solitamente formalizzati attraverso regole di inferenza , che sono gli elementi costitutivi di base del sistema di prova , noto anche come "calcolo logico".

Cercando di seguire il libro di testo di Ebbinghaus, il simbolo $\vDash$è un'espressione meta-linguaggio usata nel contesto semantico con diversi utilizzi: affiancata a destra da una formula abbrevia “è valido” (pagina 35); tra il nome di un insieme di formule e una formula abbreviata "è una conseguenza di" (pagina 33).

Infine, affiancato dal nome di un'interpretazione e da una formula abbrevia "è vero sotto l'interpretazione".

Non fa parte del linguaggio formale del calcolo: è usato per esprimere le proprietà delle formule del calcolo; nel contesto del calcolo proposizionale , leggiamo espressione "$⊨ A ∨ ¬A$"come" formula ... è una tautologia ", cioè è una formula valida di calcolo proposizionale.

Possiamo provare (nella meta-teoria) quella formula $A ∨ ¬A$è una tautologia che utilizza il metodo della tavola di verità (questa "dimostrazione" è una dimostrazione matematica e non una derivazione nel calcolo).

Simile per il simbolo $\vdash$ (vedi definizione pagina 61).

Dopo Ebbinghaus, $\varphi \to \varphi$ è una formula cioè un'espressione del linguaggio formale che leggiamo: “se $\varphi$, poi $\varphi$".

Possiamo facilmente derivarlo nel sistema di dimostrazione e simbolizziamo l'esistenza di una tale derivazione con $\vdash \varphi \to \varphi$ che ancora una volta non è una formula del linguaggio formale ma un'espressione del meta-linguaggio che abbrevia l'affermazione: “c'è una derivazione di ....” e la leggiamo (come da risposta al tuo post precedente): “formula. .. è derivabile (nel calcolo) ".

Sfortunatamente, in alcune formulazioni di ND e Sequent Calculus il simbolo $\vdash$fa parte del linguaggio formale, nel qual caso possiamo avere problemi ad usarlo anche nella meta-teoria .

Infine, dobbiamo considerare il Teorema di correttezza e completezza , un meta-teorema che vale sia per il calcolo proposizionale che per quello dei predicati (vedere pagina 70 e pagina 75) che dice in poche parole:

"$\vdash \text { iff } \vDash$".

Questo teorema esprime una proprietà del calcolo e della sua semantica. Lo dimostriamo in un modo matematico "standard".

Come detto sopra, possiamo usare la tabella della verità per dimostrarlo $A ∨ ¬A$ è una tautologia ($⊨ A ∨ ¬A$) e quindi utilizzare completezza per dimostrare $⊢ A ∨ ¬A$.

In questo modo, utilizziamo un argomento (tabella di verità) per provare una proprietà "semantica" di una certa formula e quindi utilizziamo un meta-teorema (Completezza) per provare una seconda proprietà della stessa formula: l'esistenza di una derivazione nella sistema di prova corrispondente.

Questo è il succo dei due simboli onnipresenti .