In ND , I have propositions as their own things, but in simply typed lambda calculus, I have propositions associated with proof. The question I want to ask is, how do these two different way of treating proposition (as being attached without proof vs with) cause differences between the calculus' in the big picture?
$\begingroup$
$\endgroup$
5
-
1$\begingroup$ Thsi question is unclear. For instance, if I say "Curry-Howard isomorphism", would you accept the answer? $\endgroup$– Andrej BauerCommented Jul 9, 2022 at 15:39
-
$\begingroup$ I haven't learned of that but could you explian why you say it is unclear @AndrejBauer $\endgroup$– BrianCommented Jul 9, 2022 at 16:50
-
$\begingroup$ I think the OP is about the difference of say Church's original formulation of simple type theory and simply typed lambda calculus. One has proofs that are different from terms, the other does not. $\endgroup$– Trebor ♦Commented Jul 9, 2022 at 19:05
-
$\begingroup$ Ok, but what would constitute an answer to the question how these are different in "the big picture"? $\endgroup$– Andrej BauerCommented Jul 9, 2022 at 19:10
-
1$\begingroup$ @EthakkaappamwithChai: it seems clear that you should read about the Curry-Howard correspondence and come back if you have any specific questions about it. I think it's what you're looking for. $\endgroup$– Andrej BauerCommented Jul 9, 2022 at 19:15
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
The big picture is painted by the Curry-Howard isomorphism.
If you make your question more specific and targeted, a less general answer might be possible.