## Why I do enjoy Scripting Languages

In the type theory of PM, the class φ has the same logical type as the function φ.
This makes it appropriate to use the following contextual definition, which allows one to eliminate the class term ψ from occurrences in the context f :

` f {(ψ)} . = : (∃φ) : φ!x . ≡x . ψx : f {φ!} ` Df

or in modern notation:

f {z | ψz} =df ∃φ[∀x(φx ≡ ψx) & f (λx φx)], where φ is a predicative function of x

Scripting language, a semantic world where classes were replaced by functions.

Via The Notation in Principia Mathematica.
Home