Hypothetical Judgements

The hypothetical judgment codifies the rules of expressing the validity of a conclusion conditional on the validity of one or more hypotheses. There are two forms of hypothetical judgement that differ acording to the sense in which the conclusion is conditional on the hypotheses. One is stable under extension with more rule while ther other is not.

TL; DR: Given a set of inference rules, a rule is derivable if the conclusion of the rule can be derived from its premises using only the other rules. A rule is admissible if the conclusion holds whenever the premises hold.

Derivability

Let $\cal R$ be a set of rules. We define the derivability judgement, denoted as $J_1,\cdots,J_k \vdash_{\cal R} K$, where each $J_i$ and $K$ are basic judgements, to mean that we may derive $K$ from the expansion $\mathcal{R} \cup \{J_1,\cdots,J_k\}$ of rules $\cal R$ with the axioms $J_1,\cdots,J_k$, which we treat as “temporary axioms” as they are augmented.

Formalizaed: We use $\Gamma$ or $\Delta$ to denote a finite set of basic judgements, and write $\mathcal{R} \cup \Gamma$ for the expansion of $\cal R$ with an axiom corresponding to each judgement in $\Gamma$. $\Gamma \vdash_{\cal R} K$ means that $K$ is derivable from rules $\mathcal{R} \cup \Gamma$, and the judgement $\vdash_{\cal R} \Gamma$ means that $\vdash_{\cal R} J, \forall J \in \Gamma$, i.e., by temporarily treating $J$ as axiom in $\cal R$ (the most significant trait).

Consider the following judgement:

$$ a \quad \mathsf{nat} \vdash_{\cal R} \mathsf{succ}(\mathsf{succ}(a)) \quad \mathsf{nat}, $$

where $\cal R$ is the rules for natural number definition.

Theorem (stability / redundancy): $\Gamma \vdash_{\cal R} J$ means that $\Gamma \vdash_{\cal R \cup R'} J$, as $J$ is derivable from $\Gamma \cup \cal R$ and $\cal R \cup \Gamma \subseteq R' \cup R \cup \Gamma$.

Admissibility

Admissibility is a weakened form of derivability, written as $\Gamma \vDash_{\cal R} J$, meaning that the conclusion $J$ is derivable from rules $\cal R$ when the assumptions $\Gamma$ are all derivable from rules $\cal R$, and if any of the hypotheses are not derivable from $\cal R$, then the judgement is vacuously true. For example, consider the following judgement:

$$ \mathsf{succ}(a) \space \mathsf{even} \vDash_{\cal R} a \space \mathsf{odd}. $$

w.r.t. $\cal R$ as

Bildschirmfoto 2023-04-29 um 11.50.29 AM.png

*: This is somehow like the ex falso quodlibet rule in classical logic, which is unstable if we add more axioms.

Admissibility is not stable if we add more rules into $\cal R$. However, we have the following theorem.

Theorem. $\Gamma \vdash_{\cal R} J$ implies $\Gamma \vDash_{\cal R} J$ whilst the converse fails to hold.

Apparently, $\mathsf{succ}(0) \space \mathsf{even} \nvdash_{\cal R} 0 \space \mathsf{odd}$ because adding $\mathsf{succ}(0) \space \mathsf{even}$ as one of the axioms in $\cal R$ gives no deriviation of the RHS, but $\mathsf{succ}(0) \space \mathsf{even} \vDash_{\cal R} 0 \space \mathsf{odd}$ because the hypothesis is simply false (vacuously true for the conclusion).

Note: If $r$ is admissible w.r.t. $\cal R$, then $\vdash_{\cal R, r} J \Leftrightarrow \vdash_{\cal R} J$.