\( \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".