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.
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).
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