Natural Deduction and the Calculus of Constructions

If we define p ∧ q as forall c. (p -> q -> c) -> c, you can implement left-elimination by instanciating c to p:

elim_left p_and_q = p_and_q(const) (with the brackets as function application)

where const a b = a is equivalent to your t1.

Excuse the notation, I'm not a Lean programmer and I couldn't manage to copy-paste lambda's into the code-blocks easily!

I think the comment by u/ebingdom is misleading and mostly incorrect.

There are three things that should be separated here. Natural deduction, logic, and type theory. Natural deduction is simply a style of writing down formal proofs, where we construct derivations as trees of inference rules. There are other styles too, like Hilbert systems or sequent calculus. Natural deduction has nothing in particular to do with classical logic or set theory. It absolutely can be used to formalize those things, but it's frequently used to formalize constructive logic as well.

As you mention, type theory and logic correspond. Natural deduction is a very, well, natural way to write down the rules of a logic, and it turns out to be a very natural way to write down the rules of a type theory as well! In logic we define introduction and elimination rules for propositions and in type theory we define introduction and elimination rules for types.

The principle difference between these rules is that in type theory, we decide to write down what a term of each type looks like. Instead of

A true    B true
-----------------
   A /\ B true

We write

M : A   N : B
--------------
(M,N) : A * B

These terms actually correspond directly to the trees of inference rules you'd see when writing derivations of logical propositions. In fact, if you have a well typed term, you can actually recover its entire typing derivation simply by inspecting the term (that's what type checking is!). Well typed terms are, from one perspective, simply compressed typing derivations (you can actually take this idea even further in languages like Lean and Agda, check out intrinsically typed terms).

The suggestion that proofs are first class in type theory but purely meta-theoretical in natural deduction doesn't really make any sense, since as I mentioned, you can write down the rules type theory using natural deduction. I think what u/ebingdom is getting at is the fact that when working within type theory, we generally do not bother writing down inference rules, and instead stick to writing down well typed terms, which are much smaller and more pleasant to work with. In logic, we frequently lack these nice proof terms, and have to work with big derivation trees instead. But they're still just as "first class" as proofs/terms in type theory! Check out the Hypothetical Derivation section of the Wikipedia page on natural deduction. Inference rules can bind variables and take "arguments" no problem. The confusing thing is that we sometimes write proofs about inference rules. Things like proving that there is no way to derive a proof of falsehood. This is meta-theory, and it can be done on both logics and type theories.

To address your question about defining A ∧ B as ∀ C : P. (A → B → C) → C, this is a way of encoding logical conjunction/product types using only function types (frequently called a Church encoding, they were invented by Alonzo Church). This shows that a system that has function types is actually just as powerful as one with both functions and builtin product types. As you say, Lean does not encode product types as functions, instead it simply includes them as primitive.

One major downside to Church encodings is that they frequently fail to extend effectively to dependent type theories like Lean's. That is, you can encode non-dependent pair A * B, but you cannot fully encode a dependent pair Σ(x : A) B(x), since you will not be able to encode its second projection. `

The main differences between type theory and natural deduction are:

1. Natural deduction typically includes the law of the excluded middle as an inference rule, whereas in type theory this must be added as an axiom if one wants to use it. That is to say, type theory is usually constructive and natural deduction is usually classical, but that is not required to be the case.
2. In type theory, proofs are "first class objects"—they can be and often are arguments and return values of functions. In natural deduction, proofs are metatheoretical only.
3. In natural deduction, you typically assume some axiomatization of set theory, such as ZFC. So you have two layers: a deductive system of inference rules and a set of axioms. In type theory, there is one unified system in which logic itself can be defined (even the notion of propositional equality).