Valuation Spaces and Relativisation: The Lambda Calculus Example

1. Introduction

Abstraction logic is designed to combine two features:

1. a single mathematical universe \(\univ\), as in first-order logic;
2. general binders, as in higher-order logic.

The issue we are concerned with in this article is this:

Variables of non-zero arity range over proper operations.
In full models, they range over all operations.
This is usually the intended semantics, but it is not always the semantics we want.
Sometimes, we want to constrain which operations are allowed via a valuation space,
as we show using the untyped lambda calculus as an example.

The lambda-calculus example suggests the following approximate relationship between valuation spaces and relativisation:

Valuation spaces are external relativisation.
Relativisation is internalised valuation-space control.

2. Values, operations, operators, and templates

Abstraction logic starts with one universe \(\univ\) of values. An \(n\)-ary operation on \(\univ\) is a function

\[ \univ^n \to \univ. \]

A nullary operation is just a value. An operator is one level up: it takes operations as inputs and returns a value. Operators have shapes, recording the arities of the operations they accept.

Syntactically, abstraction logic has:

• terms, which describe values;
• templates, which describe operations.

For example:

• a term x
• a term f[x]
• a template x. M[x]
• a template x y. N[x,y]

A template x. M[x] denotes a unary operation. A template x y. N[x,y] denotes a binary operation. Terms and templates are the only syntactic categories needed: variable application and abstraction application form terms, while templates bind variables.

A valuation \(\nu\) assigns to every variable \(x\) and every arity \(n\) an \(n\)-ary operation:

\[ \nu(x, n) : \univ^n \to \univ \]

In a full model, \(\nu(x,n)\) can be any \(n\)-ary operation on \(\univ\).

3. Full models versus general models

A full model validates every axiom under all valuations. In other words, if a schematic variable M[x] occurs in an axiom, then the variable \(M\) ranges over every unary operation on \(\univ\).

A general model is weaker. It consists of an algebra, a logical order, and a valuation space \(\valspace\).

The valuation space \(\valspace\) is a selected collection of valuations. It must be nonempty and closed under valuation updates and substitutions. These properties ensure that reasoning remains sound.

So the difference is:

4. The untyped lambda-calculus theory

In the experimental Paperweight syntax, the lambda-calculus theory is essentially:

declare("lam (x. M[x])")
declare("app F X")

axiom("beta", "equals (app (lam (x. M[x])) N) M[N]")

axiom("eta", "equals (lam (x. app F x)) F")

This is a compact abstraction-logic rendering of untyped lambda calculus. The abstraction lam (x. M[x]) is a proper operator: it takes a unary operation as input and returns a value. The operation app F X applies a lambda object \(F\) to an argument \(X\).

The β-axiom says:

app (lam (x. M[x])) N = M[N]

In a full model, however, M[x] ranges over all unary operations on \(\univ\). So β effectively says:

every unary operation on \(\univ\) can be reified as a value by lam, and then recovered by app.

That is an extremely strong condition. It is exactly the sort of thing abstraction logic normally avoids by distinguishing values from operations.

5. Adding implication is inconsistent

Minimal implicative logic adds a binary abstraction implies A B, with three axioms: modus ponens and two Hilbert-style implication axioms.

When this implication theory is combined with untyped lambda calculus, Curry’s paradox appears. Using a fixed-point combinator \(Y\), define:

Curry P = app Y (lam (c. implies c P))

The theory then proves arbitrary P.

The argument goes as follows. The fixed-point equation gives:

Curry P = implies (Curry P) P

Using this equality from left to right, this reads implies (Curry P) (implies (Curry P) P). By contraction, this yields implies (Curry P) P.

Using now the same equality from right to left, applying the contracted implication, this yields Curry P.

Applying modus ponens to Curry P and the contracted implication gives P. Since P was arbitrary, the combined theory is inconsistent.

6. Why this tells us something about full models

We use the following terminology relative to a chosen class \(\mathcal{C}\) of models.

A model \(\mathcal{M}\) of \(L\) expands to a model \(\mathcal{M}'\) of \(L'\) iff \(\mathcal{M}'\) interprets the new abstractions of \(L'\), while keeping the universe, the old abstractions, the logical order, and the valuation space of \(\mathcal{M}\) unchanged.

An extension \(L'\) of \(L\) is \(\mathcal{C}\)-model-conservative if every \(\mathcal{C}\)-model of \(L\) expands to a \(\mathcal{C}\)-model of \(L'\). It is \(\mathcal{C}\)-semantically conservative if, for every old-language formula \(\varphi\),

\[ L' \models_{\mathcal{C}} \varphi \quad\text{iff}\quad L \models_{\mathcal{C}} \varphi. \]

A theory \(L\) is \(\mathcal{C}\)-degenerate if every \(\mathcal{C}\)-model of \(L\) is degenerate. When \(\mathcal{C}\) is the class of all models, we simply say that \(L\) is degenerate.

The model-conservative property implies the semantic one, because old-language formulas cannot see the newly added symbols.

For full models, adding minimal implication is model-conservative in this sense: every full model of \(L\) expands to a full model of \(L + \mathrm{Implication}\) by interpreting the fresh abstraction implies as the Gödel implication, using the existing logical order of the model:

\[ u \Rightarrow v = \begin{cases} \mathrm{true} & \text{if } |u| \le |v|,\\ |v| & \text{otherwise.} \end{cases} \]

This validates the three minimal implication axioms.

The general reasoning is:

Inconsistency implies degeneracy.
Degeneracy implies full-model degeneracy.
If \(L'\) is a \(\mathcal{C}\)-semantically conservative extension of \(L\), then \(L'\) is \(\mathcal{C}\)-degenerate iff \(L\) is \(\mathcal{C}\)-degenerate.

This uses the fact that \(\mathcal{C}\)-degeneracy is equivalent to \(L \models_{\mathcal{C}} z\) for a variable \(z\): a degenerate model makes every formula true, while in a non-degenerate model the valuation space can update \(z\) to a false value.

Applying this with \(\mathcal{C}\) the class of full models and \(L' = L + \mathrm{Implication}\), the inconsistency of \(L'\) forces \(L\) to be full-model degenerate.

So for the untyped lambda-calculus theory:

The untyped lambda-calculus theory is not merely made dangerous by implication.
With respect to full models, it was already too strong: it is full-model degenerate.
Adding Implication expands this collapse to general models, and exposes it as inconsistency.

7. Why general models do not collapse in the same way

General models avoid this because they do not require β to hold under all valuations. They only require β to hold under valuations in a chosen valuation space \(\valspace\).

In a general model, M[x] need not range over every unary operation. It may range only over a collection of operations induced by the valuation space.

This is why abstraction logic has completeness for general models: the completeness theorem uses valuation spaces. For full models, the situation is different, in a way analogous to the distinction between Henkin and standard semantics in higher-order logic.

But this creates a subtle issue for extensions.

Suppose \(\valspace\) is a valuation space for a signature \(S\). If we extend the signature to \(S'\) by adding implies, then there are new substitutions, because templates may now contain implies.

So it is not automatic that

\(\valspace\) is closed under \(S\)-substitutions

implies

\(\valspace\) is closed under \(S'\)-substitutions.

This explains why adding implication is model-conservative, and therefore semantically conservative, for full models, but not automatically so for arbitrary general models.

If the implication extension were semantically conservative for general models, then the inconsistency of \(L + \mathrm{Implication}\), together with completeness for general models, would force \(L\) itself to be inconsistent, which it does not seem to be.

8. Relativised lambda calculus

A relativised lambda calculus might look like this.

declare("Lam X")
declare("Lam (x. M[x])")

declare("lam (x. M[x])")
declare("app F X")

The two declarations for Lam classify admissible lambda values and admissible lambda operations.

The key point is that β is no longer unconditional.

Instead of:

equals (app (lam (x. M[x])) N) M[N]

we use:

axiom("beta_Lam", "equals (app (lam (x. M[x])) N) M[N]", ["Lam (x. M[x])", "Lam N"])

That says:

β-reduction is valid only when the function body is an admissible lambda operation and the argument is an admissible lambda value.

The lambda-specific constructor-closure axioms are:

axiom("lam_closed", "Lam (lam (x. M[x]))", ["Lam (x. M[x])"])

axiom("app_closed", "Lam (app F X)", ["Lam F", "Lam X"])

The corresponding unary value-preservation axiom for the classifier Lam is:

axiom("Lam_body", "Lam M[x]", ["Lam (x. M[x])", "Lam x"])

This says that admissible unary operations send admissible values to admissible values.

For η, one might write:

axiom("app_template_closed", "Lam (x. app F x)", ["Lam F"])

axiom("eta_Lam", "equals (lam (x. app F x)) F", ["Lam F"])

9. How relativisation blocks Curry

In the untyped theory, Curry’s paradox uses the operation

c. implies c P

as an argument to lam.

In the relativised theory, β can only be used for this operation if we can prove:

Lam (c. implies c P)

The paradox is blocked unless the theory certifies this operation as lambda-admissible.

10. Lessons learnt

The lambda-calculus example teaches three lessons at once.

First, it explains why full models can be too strong for some applications. In a full model, positive-arity variables range over all operations. In the untyped lambda-calculus theory, that makes β far stronger than intended.

Second, it explains why valuation spaces are needed. They restrict the admissible valuations externally, allowing schematic axioms to behave like Henkin-style principles rather than standard full second-order principles.

Third, it explains relativisation. By adding an overloaded classifier Lam, one can internalise the role of the valuation space and recover meaningful full-model semantics for the embedded theory.

Source notes

This article is based on the discussion of abstraction logic, full models, valuation spaces, minimal implication, and the lambda-calculus/Curry example in One True Foundation: Unity in Multiplicity.