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.
Newer Post Older Post Home