Curry-Howard correspondence in CIC/propositional logic?

I am trying to understand how the type theory of the COQ theorem prover (calculus of constructions or CIC) works. Wikipedia states that it can be considered an extension of the Curry-Howard isomorphism.

For constructive propositional logic the Curry-Howard isomorphism states that types can be seen as propositions, and proofs as programs. For types/propositions $$A,B$$, propositions can be viewed as types in the following way (propositions on the left, types on the right, $$\Leftrightarrow$$ denoting correspondence)

$$A\rightarrow B \Leftrightarrow A\Rightarrow B$$ $$A\land B \Leftrightarrow A\times B$$ $$A\lor B\Leftrightarrow A+B$$

Then, for example, proving that

$$\forall A\forall B: A\rightarrow A\lor B,$$ where $$A,B$$ are interpreted as types can be seen as a proof that for any types $$A,B$$, the type $$A\Rightarrow A+B$$ exists. Proof of this fact can be converted into program and vice versa. In this case the program would simply return an $$x\in A$$, e.g. the left side of the pair, thereby showing the type exists.

Ok, so now to the question. CIC implements a predicate logic. How are the terms $$\forall x: A.B$$, $$\lambda x: A.B$$ interpreted in the correspondence? An example would be fine. Keep in mind I am very new to this $$\lambda$$ notation.

$$\forall x: A.B$$ is a type. It is interpreted as a terminating algorithm that takes in an $$A$$ and produces a $$B$$ as a result.

Under the Curry-Howard correspondence we interpret this as the logical statement that A implies B.

$$\lambda x: A. M$$ is a function. It takes an input $$x$$ of type $$A$$ and returns $$M$$ (which might reference $$x$$).

Under the Curry-Howard correspondence this is interpreted as a proof of $$A$$ implies $$B$$ (when $$M$$ has type $$B$$)..

• Is there a chance you could give an example of some proposition regarding naturals for example?
– Dole
Sep 17, 2020 at 16:46

This is not Curry-Howard, but a separate line of development that gets confused with it, that arises mostly from DeBruijn. Coq is an evolutionary descendant of AutoMath (A Description On ArXiv), which I put up a resurrected, revived version of here AutoMath on GitHub. In the file laying out the syntax (currently under "SyntaxNew.txt"), you'll see a description of the syntax and of the type-proposition correspondence. It, along with Martin-Löf are higher-order type theories that adopt an approach substantially different from that laid out by the Curry-Howard correspondence.

Its main feature is that types can be indexed, and the index type - itself - is included in the type system ... hence: "higher order". The product type $$(∏x∈A)B(x)$$ corresponds, roughly, to the bounded quantifier $$(∀x∈A)B(x)$$, but doubles over as an analogue of the conditional $$A ⊃ B$$, if $$B$$ is independent of $$x$$. So, it's conflating $$(∀x∈A)B = A ⊃ B$$, in that case, treating the index type $$A$$, itself, as a proposition.

AutoMath includes this feature. It also includes operators, and I don't know if Coq has this. Thus, an operator $$O(x)$$ may be defined as type $$B$$ for variables $$x$$ of type $$A$$. This corresponds to the assertion $$A ⊢ B$$, which should not be confused with the conditional $$A ⊃ B$$. (The relation between the two, in most formulations of logic, is that $$⊢ A ⊃ B$$ if and only if $$A ⊢ B$$, so that $$⊃$$ internalizes $$⊢$$.)

There's an "internal" λ-abstraction, that goes with the product type, so that if $$b(x): B(x)$$ for all $$x: A$$, then $$(Λx∈A)b(x): (∏x∈A)B(x)$$. That the epitome of a type-inference rule in Martin-Löf. In AutoMath (in the form I revised its resurrection to), the corresponding syntax is $$[A x: b(x)]$$. This should be contrasted with the "external" λ that goes with the assertions $$⊢$$ and that is encapsulated by the syntax for operator definitions. I believe Coq makes a similar distinction.

For AutoMath, the "application" type rule would then by that if $$F: (∏x∈A)B(x)$$ and $$a: A$$ then $$F: B(a)$$. In contrast, for the operator $$O$$, described above, one would just have $$O(a): B$$, when $$a: A$$. So, there is a corresponding distinction between an "internal" function application - that goes with both the modus ponens rule for $$⊃$$ and instantiation rule for $$∀$$ - versus operator application, which goes with the assertion $$⊢$$.

For higher-order type theories you also have the "sum" types $$(∑x∈A)B(x)$$ which double over as the analogue of the bounded existential quantifier $$(∃x∈A)B(x)$$ and, when $$B$$ is independent of $$x$$, conjunction $$A∧B$$ ... thereby conflating $$(∃x∈A)B = A ∧ B$$ in that case. AutoMath has no support for sum types. The type-checking rule is that $$(a,b(a)): (∃x∈A)B(x)$$ provides a witness $$b(a): B(a)$$ to a solution $$x = a$$ to $$B(x)$$, for $$a: A$$, where $$b(x): B(x)$$, for $$x: A$$.

An approach closer to the spirit of Curry-Howard, for quantifiers, would drop the distinction between internal and external λ's and treat the quantifiers essentially as just infinitary analogues of the conjunction (for $$∀$$) and disjunction (for $$∃$$), similar to what Dana Scott does in The Algebraic Interpretation of Quantifiers: Intuitionistic and Classical [PDF], particularly as seen in the formulas of Theorem 7.2 in the linked reference $$⟦∃x·Φ(x)⟧_T = ⋁_{τ∈\text{Term}} ⟦Φ(τ)⟧_T,\quad ⟦∀x·Φ(x)⟧_T = ⋀_{τ∈\text{Term}} ⟦Φ(τ)⟧_T$$ (where $$T$$ is the name of whatever first-order theory is being formalized) which corresponds to the rules $$(∃x)B_x ⊢ D ⇔ B_t ⊢ D,\text{ for all terms }t,\quad C ⊢ (∀x)A_x ⇔ C ⊢ A_t,\text{ for all terms }t$$ (where $$C$$ and $$D$$ are both independent of $$x$$) that generalize the rules for finite $$n$$-tuples (for $$n = 0$$ and $$n = 2$$): $$⊥ ⊢ D ⇔\text{ always },\quad C ⊢ ⊤ ⇔\text{ always },\\ A ∨ B ⊢ D ⇔ A ⊢ D\text{ and }B ⊢ D,\quad C ⊢ A ∧ B ⇔ C ⊢ A\text{ and }C ⊢ B,$$ to infinite-tuples. (Footnote: he goes beyond this theorem in following sections.)

An operator algebra suitable for this, with $$∘$$ given by: $$f: A ⊃ B,\quad g: B ⊃ C,\quad ⇒ \quad g ∘ f: A ⊃ C$$ might look like the following: $$f_x:C ⊃ A_x\text{ for all }x ⇒ ⟨x∷f_x⟩: C ⊃ ∀x·A_x,\\ π_t: ∀x·A_x ⊃ A_t\text{, for all terms }t,\\ π_t ∘ ⟨x∷f_x⟩ = f_t,\\ h: C ⊃ ∀x·A_x ⇒ h =⟨x∷π_x ∘ h⟩$$ for $$∀$$ (where $$C$$ is independent of $$x$$), with corresponding rules for infinite-tuples: $$a_x: A_x\text{ for all }x ⇒ (x∷a_x): ∀x·A_x,\\ c:C → ⟨x∷f_x⟩c = (x∷f_x c),\\ π_t (x∷a_x) = a_t,\\ p: ∀x·A_x ⇒ p =(x∷π_x p)$$ and a dual operator set for $$∃$$: $$g_x: B_x ⊃ D\text{ for all }x ⇒ [g_x∷x]: ∀x·B_x ⊃ D,\\ σ_t: B_t ⊃ ∃x·B_x\text{, for all terms }t,\\ [g_x∷x] ∘ σ_t = g_t,\\ h: ∀x·B_x ⊃ D ⇒ h =[h ∘ σ_x∷x]$$ (where $$D$$ is independent of $$x$$). These would be examples of proofs within this algebra $$[⟨x∷σ_x ∘ π_y⟩∷y]: ∃y·∀x·A_{xy} ⊃ ∀x·∃y·A_{xy},\\ λh·λp·(x∷(π_x h)(π_x p)): ∀x·(A_x ⊃ B_x) ⊃ ∀x·A_x ⊃ ∀x·B_x.$$