# Wadler's whys

*Propositions as Types is a notion with mystery. Why should it be the case that intuitionistic natural deduction, as developed by Gentzen in the 1930s, and simply-typed lambda calculus, as developed by Church around the same time for an unrelated purpose, should be discovered thirty years later to be essentially identical?
And why should it be the case that the same correspondence arises
again and again?*

## Minimal Necessary and Sufficient set of notions

The minimal necessary and sufficient (optimal) set of *notions* to describe (by a mind of an external observer) *any process whatsoever* in the Universe which itself is just on one single process, are:

- Simultaneity - happening to be present
*at the same locality*(no notion of time) - given as a set of arguments. - Alternative - possibility of different outcomes (of different sets of events) - this or that, partitioning.
- Application - a transformation, a single step of a process (
*Implication*is the just another name for it) -*every step is True*. - Concept - a binding, a reference to a
*verbalized concept of the mind*(a variable, bound of free) - universal notion of "things" being "there".

Implication (or application) reflects the immanent and fundamental causality of everything, governed by the *immutable laws* of the Universe.

Conjunction reflects the fact that causation is usually multiple (a different set of inputs).

Disjunction reflects the fact that different outcomes are possible (from different set of inputs) under the same set of laws.

Transformations are stable (immutable) - same input, same output. Always.

And this is enough to describe everything What Is, given you are not drowning in abstract bullshit which does not exist outside your head.

## Lambda Calculus

This is precisely why the Lambda Calculus are sufficient and expressive enough to describe any system of logic (which in turn a formal system do describe *aspects of reality*).

## Typing

To avoid *paradoxes* partitioning of concepts is necessary. Not every application is possible in this Universe, there are various constraints at all levels.

A type system filters out those applications which are "impossible" - contradictory - violate known constraints.

See also Algebraic Types

**Note:**See TracWiki for help on using the wiki.