\( \& \)-riflessione implicita e \( \& \)-riflessione esplicita

[marco2132k]

\( \newcommand{\sand}{\mathrel{\&}} \)Voglio introdurre un connettivo \( \& \) tra le proposizioni in maniera tale che, dato un contesto \( \Gamma \), valga l'equazione definitoria
\[
\text{\( \Gamma\vdash A\sand B \) se e solo se \( \Gamma\vdash A \) e \( \Gamma\vdash B \)}
\] per ogni proposizioni \( A \) e \( B \).

Mi si dice che in una direzione posso dare la regola
\[
\frac{\Gamma\vdash A\qquad \Gamma\vdash B}{\Gamma\vdash A\sand B}
\] mentre nell'altra non si può semplicemente mettere due regole da chiamare assieme \( {\sand} \)-riflessione implicita come
\[
\frac{\Gamma\vdash A\sand B}{\Gamma\vdash A}\qquad\frac{\Gamma\vdash A\sand B}{\Gamma\vdash B}
\] perché tale \( {\sand} \)-riflessione implicita "non è una definizione induttiva".

È più opportuno, si dice, prendere come regola la \( {\sand} \)-riflessione esplicita, e cioè
\[
\frac{A\vdash \Delta}{A\sand B\vdash \Delta}\qquad\frac{B\vdash \Delta}{A\sand B\vdash \Delta}\,\text{.}
\] Questa regola è stata ottenuta da \( \& \)-riflessione implicita e dalla regola di composizione, che non riporto.

Quindi: perché \( \& \)-riflessione implicita non va bene? Perché "non è induttiva"? Che significa che una definizione è "induttiva"? La preferenza per \( {\sand} \)-riflessione esplicita viene motivata intuitivamente facendo presente che richiederla come regola sarebbe come dire al robot che stiamo istruendo che ogniqualvolta si trova nella posizione \( A\sand B \) può dedurre \( A \) e può dedurre \( B \), "senza però specificare quando sarà in quella situazione".

[megas_archon]

\( \newcommand{\sand}{\mathrel{\&}} \)Per dirla semplice, in una deduzione devi implicare una e una sola conseguenza a partire da alcune premesse. Se scrivessi la &-riflessione implicita avresti una cosa tipo
\[\frac{\Gamma\vdash A\sand B}{\Gamma\vdash A\qquad \Gamma\vdash B}\]
che non sapresti "attaccare" a un'altra deduzione/giudizio/quelchel'è (da che lato? Cioè assumendo quale dei due rami?)

Per dirla in maniera più formale, una deduzione è un albero: devi sempre sapere dov'è la radice e dove si attaccano i rami, e le foglie sono (per definizione) gli assiomi. La &-riflessione esplicita non dà questo problema, perché è una regola di indebolimento delle assunzioni: da \(A\vdash \Delta\) deduci \(A \sand B \vdash \Delta\).

[marco2132k]

\( \newcommand{\sand}{\mathrel{\&}} \)

"megas_archon": Per dirla in maniera più formale, una deduzione è un albero: devi sempre sapere dov'è la radice e dove si attaccano i rami, e le foglie sono (per definizione) gli assiomi. La &-riflessione esplicita non dà questo problema, perché è una regola di indebolimento delle assunzioni: da \(A\vdash \Delta\) deduci \(A \sand B \vdash \Delta\).

Mm, ma la deduzione naturale intuizionista e classica ha la \( {\sand} \)-riflessione implicita come regola.

Leggendo un po' penso di aver capito il problema. A lezione abbiamo chiamato invertibile una regola
\[
\frac{\Gamma_1 \vdash \nabla_1\quad \Gamma_1\vdash \nabla_2\quad\cdots\quad \Gamma_n\vdash \nabla_n}{\Delta\vdash B}
\] tale che le regole
\[
\frac{\Delta\vdash B}{\Gamma_1 \vdash \nabla_1}\qquad \frac{\Delta\vdash B}{\Gamma_2 \vdash \nabla_2}\qquad\cdots\qquad \frac{\Delta\vdash B}{\Gamma_n \vdash \nabla_n}
\] siano ammissibili. Ora, se assumiamo le regole
\[
\frac{\Gamma\vdash A\qquad \Gamma\vdash B}{\Gamma\vdash A\sand B}\qquad \frac{\Gamma\vdash A\sand B}{\Gamma\vdash A}\qquad\frac{\Gamma\vdash A\sand B}{\Gamma\vdash B}
\] capita che la prima è invertibile, ma le seconde due no, perché se lo fossero avremmo
\[
\frac{\displaystyle\frac{\Gamma\vdash A}{\Gamma\vdash A\sand \bot}}{\Gamma\vdash \bot}\rightsquigarrow \frac{{}\vdash \top}{{}\vdash \bot}
\] che non penso vada bene.

Invece le regole
\[
\frac{A\vdash \Delta}{A\sand B\vdash \Delta}\qquad\frac{B\vdash \Delta}{A\sand B\vdash \Delta}
\] dovrebbero essere invertibili, ma nn mi ricordo come si dimostra.