Curry Howard correspondence and Church-Turing thesis

Question

Curry-Howard correspondence states the equivalence between logic/deduction and types/programs.

The Church-Turing thesis states the equivalence of some models of computation. Specifically, all computable functions can be written both on a Turing Machine and in Lambda Calculus.

Not all logics are equivalent however. 2nd order logic can quantify over sets whilst 1st order can't.

Can someone explain the dissonance? Can some computable functions be expressed at a "higher-level" but not at a "simpler-level"?

[CLARIFICATION]

If I define a model for computation off say 2nd order logic whilst the Turing Machine is a model for 1st order logic, then does that mean my hypothetical language can compute "uncomputable" functions? It appears so to me because 2nd order logic is more powerful than 1st order logic. This is clearly nonsense because Haskell is based off a flavor of 2 order logic (system F with extensions) but isn't more powerful than say C: any program achievable in Haskell is achievable in C. The mapping (or equivalence) between logic and computation does not appear to preserve the notion of strength: 2nd order logic is stronger than 1st order logic but programming languages off 2nd and 1st order logic have the same strength. Does that make sense?

The only conclusion I can come to is that the relationship between logic and types is not a straightforward mapping. The Turing Machine is not based off any specific logic and that any logic/deductive system can be mapped to the Turing Machine. Can you confirm?

[CLOSING WORDS]

I think that my mistake is in not realizing that there is a large divide between the colloquial "program" and programs in the context of types.

Haskell which is based on a stronger, more expressive type system does indeed provide stronger, more expressive programs. These programs are stronger in the sense that more can be guaranteed about them (in the same sense as "type safe"). This does not mean that Haskell can "compute" more; it is still merely Turing complete.

Answer 1

I'm not sure where you see the dissonance.

The Church-Turing thesis is a hypothesis stating that Turing Machines (equiv. Lambda Calculus or Recursive Functions) can do anything that we'd think of as computable.

The Curry-Howard correspondence is a much stronger statement that certain types of intuitionistic logic are structurally identical to things kind of like the Lambda Calculus. It doesn't really say which logic it corresponds to, it just shows that you can map the logical constructions in a canonical way to a (typed) computational model and vice versa. If you take different logics, you get different models and vice versa. The models may or may not be Turing-complete, although if we believe the Church-Turing thesis (it does seem to be doing alright so far), if you get a model that's more powerful than a Turing Machine, then you've got something incomputable in there.

Nonetheless, the logic you deal with does limit what you can compute in the corresponding model. For example, the Calculus of Inductive Constructions, which is a type theory and the basis for Coq, only allows types that it can verify have decreasing definitions (i.e. a recursive destruction of the type will terminate), but there are perfectly computable types which it can't verify, so you're locked out of using them.

Answer 2

TLDR: A sound logic corresponds to a non-Turing-complete lambda calculus, so the Church-Turing thesis doesn't apply.

It's important to remember that most Dependently Typed programming languages aren't Turing Complete. When you allow for non-halting programs, your logic becomes unsound. So the Curry-Howard Isomorphism doesn't really apply to

Consider Haskell, which is Turing Complete. Basically, it allows for general recursion by having an axiomatically defined fixed-point operator of type $(\alpha \rightarrow \alpha) \rightarrow \alpha$. Basically, it allows you to write a function taking a "self" argument, and create a new function which receives itself as the "self" argument.

This can be done with something like the Y-combinator, but there's no way to properly type such a function. So, there's an axiom that asserts that this fixpoint function is well typed.

The problem is, this now allows you to write programs that don't halt. When you use Curry-Howard, this allows you to prove False theorems.

Look at the type of that function as a proposition. $(P \implies P) \implies P$ as an axiom lets you prove anything, since every proposition implies itself. There's a result called the Recursion Theorem that basically says you can always find such a function in a Turing-Complete language.

Allowing for non-halting programs is what makes Turing Machines powerful, and is at the heart of the Church-Turing thesis. But as soon as you allow that, any meaningful relation to logic is lost.

Coq and Agda get around this by enforcing termination using structural recursion, but neither language is Turing Complete in the conventional sense, so the Church-Turing thesis doesn't apply to them.