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:

• x
• f[x]
• x. M[x]
• 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 \]

Crucially, \(\nu(x,n)\) need not be one of the named operators of the algebra. In a full model, it 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 exposes the collapse

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, from Curry P one obtains implies (Curry P) P. By contraction, this yields the contracted implication from Curry P to P.

Using the same equality from right to left, the contracted implication has the right-hand shape implies (Curry P) P, so it 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

For full models, adding minimal implication is semantically conservative.

Given any full model of a theory \(L\), one can interpret the fresh abstraction implies as the Gödel implication, using the existing logical order of the full 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. Hence every full model of \(L\) expands to a full model of \(L + \mathrm{Implication}\).

Therefore:

If \(L + \mathrm{Implication}\) is inconsistent, then every full model of \(L + \mathrm{Implication}\) is degenerate.
But every full model of \(L\) expands to one of \(L + \mathrm{Implication}\).
Hence every full model of \(L\) was already 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 has only degenerate full models.
Implication only exposes the collapse syntactically.

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 an admissible Henkin-style collection of operations.

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 conservative for full models but not automatically conservative for arbitrary general models.

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.