>>11482565>>11480190The historical Curry Howard correspondence works like this:
Logical connectors are /\ (and), \/ (or), -> (implies) and forall, exists: quantifiers. You have a special constant propositional "§" which means "everything holds" but which is often called "false". The type of sentences is called "Prop". A sentence is itself a special case of a type and a proof of the sentence F is a program of type F (which "reliably produce the certainty of F" in some sense).
-There is for every A:Prop, a proof of § -> A (a proof is a program of a certain type, a formula is a type basically)
-A proof of A/\B is a pair (p,q) whre p is a proof of A and q is a proof of B
- a proof of A\/B is a pair (i,p) where i is a boolean and i=#t and p is a proof of A, or i=#f and p is a proof of B
-a proof of A -> B is a map which takes a proof of A and returns a proof of B
-a proof of "forall x:T, A(x)" is a map which takes
any element j of type T and returns a proof of A(j)
-a proof of "exists y:T, A(y)" is a pair (k,r) where k is an element of type T and r is a proof of A(r).
This is all you need to get started in COQ and intuitionnism. However there is something missing here: THERE ARE NO NEGATIONS!!
In classical logic, with truth tables we know that "False -> X" is always true and that "X -> False" is equivalent to "not(X)". So it is natural to define "not (A)" as an abreviation for "A -> §" with the formalism above, however you don't have the excluded middle.
In order to get it or certain equivalent theorems like "A \/ (A->B)" for every A,B:Prop, you need either to assume them (!) or introduce exception handling programs like call/cc, savestates, etc like in classical reaizability.
