Il calcolo sequenziale ha assioma?
Gli assiomi sono regole di inferenza senza supposizioni o non regole di inferenza?
Ho sentito che il calcolo sequenziale non ha assiomi, è vero?
p69 in §6. Riepilogo ed esempio in IV. Un calcolo sequenziale nella logica matematica di Ebbinghaus, riassume le regole di inferenza nel calcolo sequenziale (si chiama deduzione naturale fuori dal libro?) Per il linguaggio del primo ordine. C'è qualche assioma?
(Assm) è un assioma? È$\phi \in \Gamma$ considerato un presupposto di esso?
È ($\equiv$) un assioma?
Risposte
(Non troppo) Risposta breve. Sì, le regole$(Assm)$ e $(\equiv)$sono assiomi. Per assioma qui (e in molti libri di testo come la Proof Theory di Takeuti citata da MauroALLEGRANZA) si intende una regola di inferenza senza premesse . In questo senso, ogni sistema di dimostrazione necessita almeno di una regola di assiomi, altrimenti non c'è possibilità di costruire una derivazione: senza assiomi, da cosa si può iniziare una derivazione in cima all'albero? Detto diversamente, questo è l'unico modo per evitare un regresso infinito .
A proposito, la regola $(Assm)$ significa che se si assume $\varphi$ (il $\varphi \in \Gamma$) poi $\varphi$ tiene (l'ultimo $\varphi$nel seguito). Così,$(Assm)$ è un impegno minimo, se non ce l'hai non puoi dire niente.
Abbiamo bisogno $(Assm)$ anche in un linguaggio puramente logico senza il simbolo di identità $\equiv$. Ovviamente, quando estendi il linguaggio con altri simboli, inevitabilmente hai bisogno di altri assiomi per trattare quel simbolo e dargli un significato. Ad esempio, l'assioma$(\equiv)$ esprime la riflessività dell'identità.
Quando senti che il calcolo sequenziale non ha alcun assioma, è inteso che non è necessario nessun assioma oltre a quello minimo$(Assm)$, almeno in una lingua puramente priva del simbolo di identità $\equiv$. Questa è la principale differenza con altri calcoli di prova come il sistema di Hilbert , dove ci sono molti assiomi anche per un linguaggio puramente logico senza il simbolo di identità.
Prima digressione: cos'è un calcolo sequenziale? Il calcolo definito nella logica matematica di Ebbinghaus è più un ibrido tra il calcolo sequenziale e la deduzione naturale, che un puro calcolo sequenziale.
Un calcolo sequenziale "puro" è un sistema di prova che manipola sequenti (cioè sequenze finite o multinsiemi di formule) o coppie di sequenti ed è caratterizzato dal fatto che non ci sono regole di eliminazione (un connettivo o quantificatore non può scomparire muovendosi da una premessa a conclusione di una regola di inferenza) tranne la regola di taglio, che è comunque ammissibile, cioè "superflua" (tutto ciò che è derivabile nel calcolo successivo può essere derivato senza utilizzare la regola di taglio). Una presentazione standard del calcolo sequenziale è data sulla pagina di Wikipedia (vedi il sistema LK ).
Perché il calcolo di Ebbinghaus non si adatta completamente a questo quadro? A causa delle regole$(PC)$ e $(Ctr)$, che sono regole di eliminazione (una formula nelle premesse scompare nella conclusione) e non sono "superflue": se le escludete dal sistema, allora non potete provare tutte le formule valide nella logica classica.
Comunque, tornando alla tua domanda principale, non cambia nulla: l'assioma $(Assm)$ è necessario sia nel calcolo sequenziale "puro" che nel calcolo di Ebbinghaus.
Seconda digressione: esistono assiomi nella deduzione naturale? Sì,$(Assm)$è richiesto anche nella deduzione naturale e, come nel calcolo successivo, è l'unico assioma richiesto, almeno in un linguaggio logico puro senza il simbolo di identità. Sotto questo aspetto il mio punto di vista è diverso da quello di MauroALLEGRANZA. Ci sono molte presentazioni differenti ma equivalenti di deduzione naturale (quella che manipola formule in derivazioni ad albero, quella che manipola sequenti, sistema in stile Fitch), in alcune di esse la presenza di$(Assm)$ è un po 'nascosto, ma è ancora lì.
Nella presentazione della deduzione naturale che manipola le formule in derivazioni ad albero (vedi qui per un'introduzione delicata), c'è una regola speciale come punto di partenza per la costruzione di dimostrazioni. Si chiama regola di assunzione e assomiglia a questo, per qualsiasi formula$\varphi$:
$$\tag{1}\varphi$$
Ciò significa che in qualsiasi momento siamo liberi di assumere semplicemente qualsiasi formula, $\varphi$. L'unica formula$\varphi$ costituisce una dimostrazione di una riga, e il modo di leggere questa dimostrazione è il seguente: assumendo $\varphi$, abbiamo dimostrato $\varphi$.
Questo è esattamente lo stesso significato della regola $(Assm)$nel calcolo successivo. In effetti, la regola dei presupposti$(1)$nella deduzione naturale può essere visto come un assioma, nel senso di una regola di inferenza senza premesse. Ciò è evidente nella presentazione in sequenza della deduzione naturale (vedere qui e qui per una spiegazione informale di questa presentazione), dove la regola di assunzione$(1)$ diventa esattamente la regola $(Assm)$ (Sequenza di Ebbbinghaus $\Gamma \ \varphi$ è più comunemente indicato con $\Gamma \vdash \varphi$).
Come nel calcolo sequent, puoi sentire che la deduzione naturale non ha alcun assioma, ma dovrebbe essere inteso che non è necessario alcun assioma oltre a quello minimo$(Assm)$, almeno in una lingua puramente priva del simbolo di identità $\equiv$.
Ciò che è comune in tutte le diverse presentazioni della deduzione naturale è che per ogni connettivo e quantificatore ci sono regole di introduzione (che introducono un nuovo connettivo o quantificatore che si sposta dalle loro premesse alla loro conclusione) e regole di eliminazione (che scartano un connettivo o quantificatore che si muove da le loro premesse alla loro conclusione).
Il calcolo di Ebbinghaus non è un sistema di deduzione naturale perché non ci sono regole di eliminazione per i connettivi $\lor$ e il quantificatore $\exists$, ma le regole $(PC)$ e $(Ctr)$ possono essere considerate regole di eliminazione e non ci sono regole di introduzione per il connettivo $\lnot$.