Chapter 3 hypothetical and general judgments

• A Hypothetical judgment expresses an Entailment between one or more Hypothesises and a Conclusion.

  -> Two forms of Entailment:

  • Derivability.

  • Admissibility.

    -> Both differ in that Derivability is Stable under extension with new rules, but Admissibility is not.

• A General judgment expresses the Universality or Genericity of a Judgment.

  -> Two forms of General judgment:

  • Generic (general) judgment.

    The generic judgment expresses generality with respect to all substitution instances for variables in a judgment.

  • Parametric (general) judgment.

    The parametric judgment expresses generality with respect to renamings of symbols.

Hypothetical judgments ​

• The Hypothetical judgment arranges the rules for expressing the Validity of a Conclusion conditional on the Validity of one or more Hypothesises.

• There are two forms of Hypothetical judgments:

  -> Differ according to the sense in which the Conclusion is conditional on the Hypothesises.

  -> One is stable under extension with more rules, and the other is not.

Derivability ​

• Consider a given set $\mathcal{R}$ of Rules.

• The Derivability judgment is written $J_1,\dots,J_k \vdash_\mathcal{R} K$, where $J_i$ and $K$ are Basic judgments.

• Such a Derivability judgment means that we may derive $K$ from the Expansion $\mathcal{R} \cup \{J_1, \dots, J_k\}$ of the rules $\mathcal{R}$ with the Axioms:

  $$\displaystyle\frac{}{J_1} \quad \dots \quad \displaystyle\frac{}{J_k}$$

  • The Hypothesises, or Antecedents, of the judgment, $J_1, \dots , J_k$ as "temporary axioms".
  • The Conclusion, or Consequents are derived by composing rules in $\mathcal{R}$.

• A set of finite Basic judgments is usually denoted as a capital Greek letter, such as $\Gamma$ or $\Delta$.

• $\mathcal{R}\cup \Gamma$ is taken to mean the Expansion of $\mathcal{R}$ with additional axioms with judgments in $\Gamma$ as the Consequents.

• The Judgment $\Gamma \vdash_{\mathcal{R}} K$ means that $K$ is Derivable from rules $\mathcal{R} \cup \Gamma$.

  The Judgment $\vdash_\mathcal{R} \Gamma$ means that $\vdash_\mathcal{R} J$ for each $J$ in $\Gamma$.

• An equivalent way of defining $J_1, \dots, J_n \vdash_\mathcal{R} J$ is to say that the rule

  $$\displaystyle\frac{J_1\ \dots\ J_n}{J}$$

  is Derivable from $\mathcal{R}$ - there is a derivation of $J$ composed of the rules in $R$ augmented by treating $J_1, \dots , J_n$ as axioms.

• Derivability is Stable under extension with new rules.

Stability ​

Theorem. If $\Gamma \vdash_\mathcal{R} J$, then $\Gamma \vdash_{\mathcal{R}\cup\mathcal{R}'} J$.

Structural property ​

• Reflexivity: Every judgment is a consequence of itself - $\Gamma, J \vdash_\mathcal{R} J$. Each hypothesis justifies itself as a Conclusion.
• Weakening: If $\Gamma \vdash_\mathcal{R} J$, then $\Gamma, K \vdash_\mathcal{R} J$. Entailment is not influenced by un-exercised options.
• Transitivity: If $\Gamma, K \vdash_\mathcal{R} J$ and $\Gamma \vdash_\mathcal{R} K$, then $\Gamma \vdash_\mathcal{R} J$. If we replace an axiom by a derivation of it, the result is a derivation of its consequent without that hypothesis.

Admissibility ​

• Admissibility, usually written as $\Gamma \models_\mathcal{R} J$, is a weaker form of Hypothetical judgment stating that $\vdash_\mathcal{R} \Gamma$ implies $\vdash_\mathcal{R} J$.

  That is, the conclusion $J$ is derivable from rules $\mathcal{R}$ when the assumptions $\Gamma$ are all derivable from rules $\mathcal{R}$.

  In particular, if any of the hypotheses are not derivable relative to $\mathcal{R}$, then the judgment is vacuously true.

  • An equivalent way to define the judgment $J_1, \dots , J_n \models_\mathcal{R} J$ is to state that the rule

  $$\displaystyle\frac{J_1\ \dots\ J_n}{J}$$

  is admissible relative to the rules in $\mathcal{R}$.

  Given any derivations of $J_1, \dots, J_n$ using the rules in $\mathcal{R}$, we may build a derivation of $J$ using the rules in $\mathcal{R}$.

• Example

  The Admissibility judgment

  $$\text{succ}(a)\ \text{even} \models a\ \text{odd}$$

  is valid.

  Reason: Any derivation of $\text{succ}(a)\ \text{even}$ from rules must contain a sub-derivation of $a\ \text{odd}$ from the same rules, which justifies the conclusion.

Unstability ​

• The admissibility judgment is not stable under extension to the rules.

• Counterexample

  If we enrich the original rules:

  $$\displaystyle\frac{}{\text{zero}\ \text{even}}$$

  $$\displaystyle\frac{n\ \text{even}}{ \text{succ}(n)\ \text{odd}}$$

  $$\displaystyle\frac{n\ \text{odd}}{\text{succ}(n)\ \text{even}}$$

  with the following rule:

  $$\displaystyle\frac{}{\text{succ}(\text{zero})\ \text{even}}$$

  Then the rule $\text{succ}(a)\ \text{even} \models a\ \text{odd}$ is Inadmissible.

Derivability as a stronger judgment than Admissibility ​

Theorem. If $\Gamma \vdash_\mathcal{R} J$, then $\Gamma \models_\mathcal{R} J$.

Interpretation of an admissibility evidence ​

• Evidence for admissibility can be thought of as a mathematical function transforming derivations $\triangledown_1, \dots, \triangledown_n$ of the hypotheses into a derivation $\triangledown$ of the consequent.

Structural property (admissibility) ​

• Reflexivity: If $J$ is derivable from the original rules, then $J$ is derivable from the original rules: $J \models_\mathcal{R} J$.
• Weakening: If $J$ is derivable from the original rules assuming that each of the judgments in $\Gamma$ are derivable from these rules, then $J$ must also be derivable assuming that $\Gamma$ and $K$ are derivable from the original rules: if $\Gamma \models_\mathcal{R} J$, then $\Gamma, K \models_\mathcal{R} J$.
• Transitivity: If $\Gamma, K \models_\mathcal{R} J$ and $\Gamma \models_\mathcal{R} K$, then $\Gamma \models_\mathcal{R} J$. If the judgments in $\Gamma$ are derivable, so is $K$, by assumption, and hence so are the judgments in $\Gamma, K$, and hence so is $J$.

Hypothetical inductive definitions ​

• Hypothetical inductive definitions enrich standard Inductive definitions by allowing rules where the Premises and Conclusions are Derivability judgments.

• This structure introduces two types of hypotheses:

  • Global hypothesises ($\Gamma$): In effect at the point where the Rule is applied.
  • Local hypothesises ($\Gamma_i$): Specific only to the Derivation of a particular Premise.

• A Hypothetical rule takes the following explicit form:

  $$\frac{\Gamma\ \Gamma_1 \vdash J_1 \quad \dots \quad \Gamma\ \Gamma_n \vdash J_n}{\Gamma \vdash J}$$

  The Hypothesises $\Gamma$ are the Global hypothesises of the Rule.

  The Hypothesises $\Gamma_i$ are the Local hypothesises of the $i$th Premise or the Rule.

  • Interpretation: $J$ is a Derivable consequence of $\Gamma$ if, for every Premise $i$, $J_i$ is a Derivable consequence of $\Gamma$ augmented by the local hypotheses $\Gamma_i$.
  • Context switch: Deriving a Premise involves a "context switch" where the Global hypothesises are extended by the Local hypothesises of that Premise.

Uniformity & Implicit form ​

• Rules in a Hypothetical inductive definition must be Uniform, meaning they apply in all global Contexts.

• Because of this Uniformity, the global Context $\Gamma$ is often suppressed, leading to the Implicit form:

  $$\frac{\Gamma_1 \vdash J_1 \quad \dots \quad \Gamma_n \vdash J_n}{J}$$

  -> Implicit understanding: The rule applies for any choice of Global hypothesises.

Structurality of judgments ​

• A Hypothetical inductive definition -> An ordinary Inductive definition of a Formal derivability judgment $\Gamma \vdash J$ consisting of:

  • A finite set of Basic judgments $\Gamma$.
  • A Basic judgment $J$.

• A set of Hypothetical rules $\mathcal{R}$ defines the strongest Formal derivability judgment that is Structural and Closed (under) Uniform rules $\mathcal{R}$.

• Structurality means that the Formal derivability judgment must be closed under the following rules:

  • Reflexivity:

    $$\displaystyle\frac{}{\Gamma, J \vdash J}$$

  • Weakening:

    $$\displaystyle\frac{\Gamma \vdash J}{\Gamma, K \vdash J}$$

  • Transitivity:

    $$\displaystyle\frac{\Gamma \vdash K \quad \Gamma, K \vdash J}{\Gamma \vdash J}$$

Hypothetical rule induction ​

• The principle of Hypothetical rule induction is simply standard Rule induction applied to the Formal derivability judgment.

• To show that a property $\mathcal{P}(\Gamma \vdash J)$ holds whenever $\Gamma \vdash_{\mathcal{R}} J$, one must show that $\mathcal{P}$ is closed under:

  1. The rules of $\mathcal{R}$: If $\mathcal{P}(\Gamma\ \Gamma_1 \vdash J_1)$ and \ldots and $\mathcal{P}(\Gamma\ \Gamma_n \vdash J_n)$, then $\mathcal{P}(\Gamma \vdash J)$.
  2. The structural rules: The property must be preserved under Reflexivity, Weakening, and Transitivity.

• In practice, rather than proving the structural steps explicitly during induction, we typically prove that the structural rules are Admissible.

  • If rules are Uniform, Weakening and Transitivity are usually clearly admissible.
  • Reflexivity is usually postulated explicitly as a rule.

General judgments ​

• General judgments codify the Rules for handling Variables in a Judgment.

• Variable: An unknown, ranging over a specified set of objects.

• A Generic (general) judgment states that a Judgment holds for any choice of objects replacing designated variables in the judgment.

• A Parametric (general) judgments codify the handling of Symbolic parameters, expressing generality over any choice of Fresh renamings of designated Symbols of a Judgment.

• $\Gamma^{\mathcal{U};\mathcal{X}}_\mathcal{R}J$ - $J$ is Derivable from $\Gamma$ according to Rules $\mathcal{R}$, with objects consisting of Abstract binding tree (ABT)s over Symbols $\mathcal{U}$ and Variables $\mathcal{X}$.

• The concept of Uniformity of a Rule must be extended to require that rules be:

  • Closed under renaming and substitution for Variables.

  • Closed under renaming for Symbolic parameters.

    Formally:

  • If $\mathcal{R}$ is a set of rules containing a Free variable $x$ of Sort $s$, then it must also contain all possible substitution instances of Abstract binding tree (ABT)s $a$ of Sort $s$ for $x$, including those that contain other Free variables.

  • If $\mathcal{R}$ contains Rules with a Symbolic parameter $u$, then it must contain all instances of that rule obtained by renaming $u$ of a sort to any $u'$ of the same Sort.

    -> Ruling out:

  • Stating a rule for a variable, without also stating it for all instances of that variable.

  • Stating a rule for a parameter without stating it for all possible renamings of that parameter.

Generic derivability ​

• Generic derivability judgment is defined by:

  $$\mathcal{Y}\ \vert \ \Gamma \vdash^\mathcal{X}_\mathcal{R}\ J\quad \text{iff} \quad \Gamma \vdash^{\mathcal{X}\mathcal{Y}}_\mathcal{R}J$$

  where $\mathcal{Y} \cap \mathcal{X} = \emptyset$.

• Evidence for Generic derivability consists of a Generic derivation $\triangledown$ involving the Variables $\mathcal{X}\mathcal{Y}$.

  -> If the rules are Uniform, the choice of $\mathcal{Y}$ does not matter.

  • Example

    Given $\mathcal{R}$ as:

    $$\displaystyle\frac{}{\text{zero}\ \text{nat}}$$

    $$\displaystyle\frac{x\ \text{nat}}{\text{succ}(x)\ \text{nat}}$$

    The Generic derivation $\triangledown$:

    $$\displaystyle\frac{\displaystyle\frac{\displaystyle\frac{}{x\ \text{nat}}}{\text{succ}(x)\ \text{nat}}}{\text{succ}(\text{succ}(x))\ \text{nat}}$$

    is Evidence for the Judgment:

    $$x \ \vert \ x\ \text{nat} \vdash^{\mathcal{X}}_\mathcal{R}\ \text{succ}(\text{succ}(x))\ \text{nat}$$

    provided $x \notin \mathcal{X}$.

• The Generic derivability judgment enjoys the following Structural property governing the behavior of Variables, provided that $\mathcal{R}$ is Uniform.

  • Proliferation:

    If $\mathcal{Y}\ \vert \ \Gamma \vdash^\mathcal{X}_\mathcal{R}\ J$, then $\mathcal{Y}, y\ \vert \ \Gamma \vdash^\mathcal{X}_\mathcal{R} J$.

  • Renaming:

    If $\mathcal{Y}, y\ \vert \ \Gamma \vdash^\mathcal{X}_\mathcal{R} J$, then $\mathcal{Y}, y'\ \vert \ [y \leftrightarrow y']\Gamma \vdash^\mathcal{X}_\mathcal{R}[y \leftrightarrow y']J$ for any $y' \notin \mathcal{XY}$.

  • Substitution:

    If $\mathcal{Y}, y\ \vert \ \Gamma \vdash^\mathcal{X}_\mathcal{R} J$ and $a \in \mathcal{B}[\mathcal{XY}]$, then $\mathcal{Y}\ \vert \ [a/y]\Gamma \vdash^\mathcal{X}_\mathcal{R}[a/y]J$.

• Remarks: To my understanding, $\mathcal{X}$ acts somewhat like free variables, and $\mathcal{Y}$ acts somewhat like bound variables.

Parametric derivability ​

• Parametric (general) judgment is defined analogously like Generic (general) judgment, albeit by generalizing over Symbolic parameters, rather than Variables.

• Parametric (general) judgment is defined by:

  $$\mathcal{V} \ \Vert \ \mathcal{Y}\ \vert \ \Gamma \vdash^{\mathcal{U};\mathcal{X}}_{\mathcal{R}}\ J \quad \text{iff} \quad \mathcal{Y}\ \vert \ \Gamma^{\mathcal{UV};\mathcal{X}}_\mathcal{R}\ J$$

  where $\mathcal{V} \cap \mathcal{U} = \emptyset$.

• Evidence for Parametric (general) judgment consists of a Derivation $\triangledown$ involving the symbols $\mathcal{V}$.

• Uniformity of $\mathcal{R}$ ensures that any choice of parameter names is as good as any other. Derivability is Stable under Renaming.

Generic inductive definitions ​

• A Generic inductive definition admits Generic inductive definition in the Premises of rules.

  -> Augmenting the variables & the rules within those Premises.

• A Generic rule has the form:

  $$\displaystyle\frac{\mathcal{Y}\ \mathcal{Y}_1\ \vert \ \Gamma\ \Gamma_1 \vdash J_1 \quad \dots \quad \mathcal{Y}\ \mathcal{Y}_n\ \vert \ \Gamma\ \Gamma_n\vdash J_n}{\mathcal{Y}\ \vert \ \Gamma \vdash J}$$

  • Global variables: $\mathcal{Y}$.
  • For each $1 \le i \le n$, Local variables of the $i$th Premise: $\mathcal{Y}_i$.

• Implicit form:

  $$\displaystyle\frac{\mathcal{Y}_1\ \vert \ \Gamma_1 \vdash J_1 \quad \dots \quad \mathcal{Y}_n\ \vert \ \Gamma_n \vdash J_n}{J}$$

• A Generic inductive definition is an ordinary Inductive definition of a family of formal Generic (general) judgments of the form $\mathcal{Y}\ \vert \ \Gamma \vdash J$.

  Formal Generic (general) judgments are identified up to Renaming of Variables.

  -> The latter Judgment is treated as identical to the Judgment $\mathcal{Y}'\ \vert \ \hat{\rho}(\Gamma) \vdash \hat{\rho}(J)$ for any Renaming $\rho : \mathcal{Y} \leftrightarrow \mathcal{Y}'$.

• If $\mathcal{R}$ is a collection of Generic rules, we write $\mathcal{Y}\ \vert \ \Gamma \vdash_{\mathcal{R}} J$ to mean that the formal Generic (general) judgment $\mathcal{Y}\ \vert \ \Gamma \vdash J$ is derivable from rules $\mathcal{R}$.

• When specialized to a set of Generic rules, the principle of Rule induction states that to show $\mathcal{P}(\mathcal{Y}\ \vert \ \Gamma \vdash J)$ when $\mathcal{Y}\ \vert \Gamma \vdash_{\mathcal{R}} J$, it is sufficient to show that $\mathcal{P}$ is closed under the rules $\mathcal{R}$.

  If $\mathcal{P}(\mathcal{Y}\ \mathcal{Y}_1\ \vert \ \Gamma\ \Gamma_1 \vdash J_1)\ \dots\ \mathcal{P}(\mathcal{Y}\ \mathcal{Y}_n\ \vert \ \Gamma\ \Gamma_n \vdash J_n)$ then $\mathcal{P}(\mathcal{Y}\ \vert \ \Gamma \vdash J)$.

  • The property $\mathcal{P}$ must respect Renamings of the Variables in a formal Generic (general) judgment.

• To ensure that a Formal generic judgment behaves like a Generic (general) judgment, the Structural rules are Admissible.

  $$\displaystyle\frac{}{\mathcal{Y}\ \vert \ \Gamma, J \vdash J} \tag{3.14a}$$

  $$\displaystyle\frac{\mathcal{Y}\ \vert \ \Gamma \vdash J}{\mathcal{Y}\ \vert \ \Gamma, J' \vdash J} \tag{3.14b}$$

  $$\displaystyle\frac{\mathcal{Y}\ \vert \ \Gamma \vdash J}{\mathcal{Y}, x\ \vert \ \Gamma \vdash J} \tag{3.14c}$$

  $$\displaystyle\frac{\mathcal{Y}, x'\ \vert \ [x\leftrightarrow x']\Gamma \vdash [x \leftrightarrow x']J}{\mathcal{Y}, x\ \vert \ \Gamma \vdash J} \tag{3.14d}$$

  $$\displaystyle\frac{\mathcal{Y}\ \vert \ \Gamma\vdash J\quad \mathcal{Y}\ \vert \ \Gamma, J \vdash J'}{\mathcal{Y}\ \vert \ \Gamma \vdash J'} \tag{3.14e}$$

  $$\displaystyle\frac{\mathcal{Y}, x\ \vert \ \Gamma \vdash J \quad a \in \mathcal{B}[\mathcal{Y}]}{\mathcal{Y}\ \vert \ [a/x]\Gamma \vdash [a/x]J} \tag{3.14f}$$

  • The Admissibility of rule (3.14a) is in practice ensured by explicitly including it.

  • The Admissibility of rules (3.14b) and (3.14c) is assured if each of the generic rules is Uniform because we may:

    • Assimilate the added variable $x$ to the global variables $\mathcal{Y}$.
    • Assimilate the added hypothesis $J'$ to the global hypotheses $\Gamma'$.

  • The Admissibility of rule (3.14d) is ensured by the identification convention for the formal generic judgment.

  • Rule (3.14f) must be verified explicitly for each inductive definition.

• Parametric inductive definition is similar to generic inductive definition.

Notes ​

• Foundational roots

  • The concepts of entailment and generality are central to logic and programming languages.
  • Harper's formulation builds specifically on the work of Martin-Lof (1983, 1987) and Avron (1991).

• Contrast with AUTOMATH & LF

  • Unified Concept: Systems like AUTOMATH and the LF Logical Framework consolidate hypothetical and general reasoning into a single concept.
  • Arbitrary Nesting: These systems allow for arbitrarily nested combinations of judgments (e.g., judgments about judgments).

• Harper's distinction

  • Restricted structure: Unlike LF, PFPL considers only general hypothetical judgments over basic judgment forms. It separates the machinery of entailment from the basic judgments.
  • Explicitly introduces symbols and variables, which were not present in the previous accounts (Martin-Lof/Avron).

• Why symbols matter (Parametric Judgments)

  • Parametric judgments are necessary to specify languages that allow the dynamic creation of "new" objects.

Exercise ​

Exercise 3.1 ​

Problem statement. Combinators are inductively defined by the rule set $\mathcal{C}$ given as follows:

$$\displaystyle \frac{}{\mathsf{s} \ \text{comb}} \quad \tag{3.15a}$$

$$\displaystyle\frac{}{\mathsf{k}\ \text{comb}} \quad \tag{3.15b}$$

$$\displaystyle \frac{a_1 \text{ comb} \quad a_2 \text{ comb}}{\mathsf{ap}(a_1; a_2) \text{ comb}} \quad \tag{3.15c}$$

Give an inductive definition of the length of a combinator defined as the number of occurrences of $\mathsf{s}$ and $\mathsf{k}$ within it.