true iff $t_1$ is false or both $t_1$ and $t_2$ are true,

-   $t_1 \supset t_2$ is false iff $t_1$ is true and $t_2$ is false,

-   $\neg t$ is true iff $t$ is false,

-   $\neg t$ is false iff $t$ is true.

Obviously, $\Gamma {\ensuremath{\vdash}}t$ is then (informally) interpreted as: for all possible substitution instances $\Gamma^*,t^*$ of $\Gamma,t$, [^2] if all terms in $\Gamma^*$ are true, then the term $t^*$ is also true.

Note that the logical connectives are “lazy”, e.g. for $t_1 \vee
t_2$ to be true it suffices that $t_1$ is true, but $t_2$ need not have a truth value at all – it may be something else: a program, a type, “undefined”, etc. This laziness allows us to omit many restrictions which would otherwise be needed in inference rules, and would thus make the system less similar to ordinary logic.

The following rules may be derived in ${\ensuremath{{\cal I}}}_s$.

  ------------------------------------------------------------------------------------------------------------------------------------------------------- ---------------------------------------------------------------------------------------------
                                                                             $                                                                                                                          $
                                                                        \supset_i:\;                                                                                                               \supset_e:\;
                                                                         \inferrule{                                                                                                                \inferrule{
                        \Gamma {\ensuremath{\vdash}}\varphi : {\ensuremath{\mathrm{Prop}}}\\ \Gamma, \varphi {\ensuremath{\vdash}}\psi                         \Gamma {\ensuremath{\vdash}}\varphi \supset \psi \\ \Gamma {\ensuremath{\vdash}}\varphi
                                                                             }{                                                                                                                         }{
                                                       \Gamma {\ensuremath{\vdash}}\varphi \supset \psi                                                                                   \Gamma {\ensuremath{\vdash}}\psi
                                                                              }                                                                                                                          }
                                                                              $                                                                                                                          $

                                                                                                                                                          

                                                                             $                                                                                                                          $
                                                                         \supset_t:\;                                                                                                              {\wedge_{i}:}\;
                                                                          \inferrule{                                                                                                                \inferrule{
         \Gamma {\ensuremath{\vdash}}\varphi : {\ensuremath{\mathrm{Prop}}}\\ \Gamma, \varphi 