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 $ℛ$ of Rules.

• The Derivability judgment is written $J_1,\dots ,J_k{⊢}_{ℛ}K$, where $J_i$ and $K$ are Basic judgments.

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

  $${\displaystyle \frac{}{J_1}\dots {\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 $ℛ$.

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

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

• The Judgment $\mathrm{\Gamma }{⊢}_{ℛ}K$ means that $K$ is Derivable from rules $ℛ\cup \mathrm{\Gamma }$.

  The Judgment ${⊢}_{ℛ}\mathrm{\Gamma }$ means that ${⊢}_{ℛ}J$ for each $J$ in $\mathrm{\Gamma }$.

• An equivalent way of defining $J_1,\dots ,J_n{⊢}_{ℛ}J$ is to say that the rule

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

  is Derivable from $ℛ$ - 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 $\mathrm{\Gamma }{⊢}_{ℛ}J$, then $\mathrm{\Gamma }{⊢}_{ℛ\cup {ℛ}^{\prime }}J$.

Structural property ​

• Reflexivity: Every judgment is a consequence of itself - $\mathrm{\Gamma },J{⊢}_{ℛ}J$. Each hypothesis justifies itself as a Conclusion.

• Weakening: If $\mathrm{\Gamma }{⊢}_{ℛ}J$, then $\mathrm{\Gamma },K{⊢}_{ℛ}J$. Entailment is not influenced by un-exercised options.

• Transitivity: If $\mathrm{\Gamma },K{⊢}_{ℛ}J$ and $\mathrm{\Gamma }{⊢}_{ℛ}K$, then $\mathrm{\Gamma }{⊢}_{ℛ}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 $\mathrm{\Gamma }{\models }_{ℛ}J$, is a weaker form of Hypothetical judgment stating that ${⊢}_{ℛ}\mathrm{\Gamma }$ implies ${⊢}_{ℛ}J$.

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

  In particular, if any of the hypotheses are not derivable relative to $ℛ$, then the judgment is vacuously true.

  • An equivalent way to define the judgment $J_1,\dots ,J_n{\models }_{ℛ}J$ is to state that the rule

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

  is admissible relative to the rules in $ℛ$.

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

• 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 $\mathrm{\Gamma }{⊢}_{ℛ}J$, then $\mathrm{\Gamma }{\models }_{ℛ}J$.

Interpretation of an admissibility evidence ​

• Evidence for admissibility can be thought of as a mathematical function transforming derivations ${▽}_1,\dots ,{▽}_n$ of the hypotheses into a derivation $▽$ 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 }_{ℛ}J$.

• Weakening: If $J$ is derivable from the original rules assuming that each of the judgments in $\mathrm{\Gamma }$ are derivable from these rules, then $J$ must also be derivable assuming that $\mathrm{\Gamma }$ and $K$ are derivable from the original rules: if $\mathrm{\Gamma }{\models }_{ℛ}J$, then $\mathrm{\Gamma },K{\models }_{ℛ}J$.

• Transitivity: If $\mathrm{\Gamma },K{\models }_{ℛ}J$ and $\mathrm{\Gamma }{\models }_{ℛ}K$, then $\mathrm{\Gamma }{\models }_{ℛ}J$. If the judgments in $\mathrm{\Gamma }$ are derivable, so is $K$, by assumption, and hence so are the judgments in $\mathrm{\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 ($\mathrm{\Gamma }$): In effect at the point where the Rule is applied.

  • Local hypothesises (${\mathrm{\Gamma }}_i$): Specific only to the Derivation of a particular Premise.

• A Hypothetical rule takes the following explicit form:

  $$\frac{\mathrm{\Gamma }{\mathrm{\Gamma }}_1⊢J_1\dots \mathrm{\Gamma }{\mathrm{\Gamma }}_n⊢J_n}{\mathrm{\Gamma }⊢J}$$

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

  The Hypothesises ${\mathrm{\Gamma }}_i$ are the Local hypothesises of the $i$th Premise or the Rule.

  • Interpretation: $J$ is a Derivable consequence of $\mathrm{\Gamma }$ if, for every Premise $i$, $J_i$ is a Derivable consequence of $\mathrm{\Gamma }$ augmented by the local hypotheses ${\mathrm{\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 $\mathrm{\Gamma }$ is often suppressed, leading to the Implicit form:

  $$\frac{{\mathrm{\Gamma }}_1⊢J_1\dots {\mathrm{\Gamma }}_n⊢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 $\mathrm{\Gamma }⊢J$ consisting of:

  • A finite set of Basic judgments $\mathrm{\Gamma }$.

  • A Basic judgment $J$.

• A set of Hypothetical rules $ℛ$ defines the strongest Formal derivability judgment that is Structural and Closed (under) Uniform rules $ℛ$.

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

  • Reflexivity:

    $${\displaystyle \frac{}{\mathrm{\Gamma },J⊢J}}$$

  • Weakening:

    $${\displaystyle \frac{\mathrm{\Gamma }⊢J}{\mathrm{\Gamma },K⊢J}}$$

  • Transitivity:

    $${\displaystyle \frac{\mathrm{\Gamma }⊢K\mathrm{\Gamma },K⊢J}{\mathrm{\Gamma }⊢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 $𝒫(\mathrm{\Gamma }⊢J)$ holds whenever $\mathrm{\Gamma }{⊢}_{ℛ}J$, one must show that $𝒫$ is closed under:

  1. The rules of $ℛ$: If $𝒫(\mathrm{\Gamma }{\mathrm{\Gamma }}_1⊢J_1)$ and \ldots and $𝒫(\mathrm{\Gamma }{\mathrm{\Gamma }}_n⊢J_n)$, then $𝒫(\mathrm{\Gamma }⊢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.

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

• 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 $ℛ$ 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 $ℛ$ 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^{\prime }$ 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:

  $$𝒴|\mathrm{\Gamma }{⊢}_{ℛ}^{𝒳}J\text{iff}\mathrm{\Gamma }{⊢}_{ℛ}^{𝒳𝒴}J$$

  where $𝒴\cap 𝒳=\varnothing$.

• Evidence for Generic derivability consists of a Generic derivation $▽$ involving the Variables $𝒳𝒴$.

  -> If the rules are Uniform, the choice of $𝒴$ does not matter.

  • Example

    Given $ℛ$ as:

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

    The Generic derivation $▽$:

    $${\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|x\text{nat}{⊢}_{ℛ}^{𝒳}\text{succ}(\text{succ}(x))\text{nat}$$

    provided $x\notin 𝒳$.

• The Generic derivability judgment enjoys the following Structural property governing the behavior of Variables, provided that $ℛ$ is Uniform.

  • Proliferation:

    If $𝒴|\mathrm{\Gamma }{⊢}_{ℛ}^{𝒳}J$, then $𝒴,y|\mathrm{\Gamma }{⊢}_{ℛ}^{𝒳}J$.

  • Renaming:

    If $𝒴,y|\mathrm{\Gamma }{⊢}_{ℛ}^{𝒳}J$, then $𝒴,y^{\prime }|[y\leftrightarrow y^{\prime }]\mathrm{\Gamma }{⊢}_{ℛ}^{𝒳}[y\leftrightarrow y^{\prime }]J$ for any $y^{\prime }\notin 𝒳𝒴$.

  • Substitution:

    If $𝒴,y|\mathrm{\Gamma }{⊢}_{ℛ}^{𝒳}J$ and $a\in ℬ[𝒳𝒴]$, then $𝒴|[a/y]\mathrm{\Gamma }{⊢}_{ℛ}^{𝒳}[a/y]J$.

• Remarks: To my understanding, $𝒳$ acts somewhat like free variables, and $𝒴$ 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:

  $$𝒱\Vert 𝒴|\mathrm{\Gamma }{⊢}_{ℛ}^{𝒰;𝒳}J\text{iff}𝒴|{\mathrm{\Gamma }}_{ℛ}^{𝒰𝒱;𝒳}J$$

  where $𝒱\cap 𝒰=\varnothing$.

• Evidence for Parametric (general) judgment consists of a Derivation $▽$ involving the symbols $𝒱$.

• Uniformity of $ℛ$ 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{𝒴{𝒴}_1|\mathrm{\Gamma }{\mathrm{\Gamma }}_1⊢J_1\dots 𝒴{𝒴}_n|\mathrm{\Gamma }{\mathrm{\Gamma }}_n⊢J_n}{𝒴|\mathrm{\Gamma }⊢J}}$$

  • Global variables: $𝒴$.

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

• Implicit form:

  $${\displaystyle \frac{{𝒴}_1|{\mathrm{\Gamma }}_1⊢J_1\dots {𝒴}_n|{\mathrm{\Gamma }}_n⊢J_n}{J}}$$

• A Generic inductive definition is an ordinary Inductive definition of a family of formal Generic (general) judgments of the form $𝒴|\mathrm{\Gamma }⊢J$.

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

  -> The latter Judgment is treated as identical to the Judgment ${𝒴}^{\prime }|\hat{\rho }(\mathrm{\Gamma })⊢\hat{\rho }(J)$ for any Renaming $\rho :𝒴\leftrightarrow {𝒴}^{\prime }$.

• If $ℛ$ is a collection of Generic rules, we write $𝒴|\mathrm{\Gamma }{⊢}_{ℛ}J$ to mean that the formal Generic (general) judgment $𝒴|\mathrm{\Gamma }⊢J$ is derivable from rules $ℛ$.

• When specialized to a set of Generic rules, the principle of Rule induction states that to show $𝒫(𝒴|\mathrm{\Gamma }⊢J)$ when $𝒴|\mathrm{\Gamma }{⊢}_{ℛ}J$, it is sufficient to show that $𝒫$ is closed under the rules $ℛ$.

  If $𝒫(𝒴{𝒴}_1|\mathrm{\Gamma }{\mathrm{\Gamma }}_1⊢J_1)\dots 𝒫(𝒴{𝒴}_n|\mathrm{\Gamma }{\mathrm{\Gamma }}_n⊢J_n)$ then $𝒫(𝒴|\mathrm{\Gamma }⊢J)$.

  • The property $𝒫$ 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.

  $$\begin{array}{ccc}& {\displaystyle \frac{}{𝒴|\mathrm{\Gamma },J⊢J}}& \text{(3.14a)}\end{array}$$$$\begin{array}{ccc}& {\displaystyle \frac{𝒴|\mathrm{\Gamma }⊢J}{𝒴|\mathrm{\Gamma },J^{\prime }⊢J}}& \text{(3.14b)}\end{array}$$$$\begin{array}{ccc}& {\displaystyle \frac{𝒴|\mathrm{\Gamma }⊢J}{𝒴,x|\mathrm{\Gamma }⊢J}}& \text{(3.14c)}\end{array}$$$$\begin{array}{ccc}& {\displaystyle \frac{𝒴,x^{\prime }|[x\leftrightarrow x^{\prime }]\mathrm{\Gamma }⊢[x\leftrightarrow x^{\prime }]J}{𝒴,x|\mathrm{\Gamma }⊢J}}& \text{(3.14d)}\end{array}$$$$\begin{array}{ccc}& {\displaystyle \frac{𝒴|\mathrm{\Gamma }⊢J𝒴|\mathrm{\Gamma },J⊢J^{\prime }}{𝒴|\mathrm{\Gamma }⊢J^{\prime }}}& \text{(3.14e)}\end{array}$$$$\begin{array}{ccc}& {\displaystyle \frac{𝒴,x|\mathrm{\Gamma }⊢Ja\in ℬ[𝒴]}{𝒴|[a/x]\mathrm{\Gamma }⊢[a/x]J}}& \text{(3.14f)}\end{array}$$

  • 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 $𝒴$.

    • Assimilate the added hypothesis $J^{\prime }$ to the global hypotheses ${\mathrm{\Gamma }}^{\prime }$.

  • 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 $𝒞$ given as follows:

Give an inductive definition of the length of a combinator defined as the number of occurrences of $𝗌$ and $𝗄$ within it.