Define pairs in higher-order logic using lambda abstraction. For example, let:
makePair = λu.λv.λw. w u v
firstElem = λp. p (λx.λy. x)
Then firstElem(makePair(u, v)) equals u.
The method presented offers a clean and elegant way to deal with pairs in higher-order logic. In my own projects I found that representing pairs as lambda abstractions strips away unnecessary syntactic overhead and makes the underlying operations more apparent. By viewing a pair as a function that takes a selector, it not only simplifies the definition of operations like retrieving the first element, but it also allows for easy extension. This pattern can be leveraged when modeling more complex data structures and functional transformations.