We can also interpret this in proof theory. K-types don’t care how many steps there are in the proof, they only care about the number of axioms used in the proof. T-types do care how many steps there are in the proof, whether those steps are axioms or inferences.
I don’t get how you apply this in proof theory. If K-types want to minimize the Kolmogorov-complexity of things, wouldn’t they be the ones caring about the description length of the proof? How do axioms incur any significant description length penalty? (Axioms are usually much shorter to describe than proofs, because you of course only have to state the proposition and not any proof.)
I see, with that mapping your original paragraph makes sense.
Just want to note though that such a mapping is quite weird and I don’t really see a mathematical justification behind it. I only know of the Curry-Howard isomorphism as a way to translate between proof theory and computer science, and it maps programs to proofs, not to axioms.
I don’t get how you apply this in proof theory. If K-types want to minimize the Kolmogorov-complexity of things, wouldn’t they be the ones caring about the description length of the proof? How do axioms incur any significant description length penalty? (Axioms are usually much shorter to describe than proofs, because you of course only have to state the proposition and not any proof.)
when translating between proof theory and computer science:
(computer program, computational steps, output) is mapped to (axioms, deductive steps, theorems) respectively.
kolmogorov-complexity maps to “total length of the axioms” and time-complexity maps to “number of deductive steps”.
I see, with that mapping your original paragraph makes sense.
Just want to note though that such a mapping is quite weird and I don’t really see a mathematical justification behind it. I only know of the Curry-Howard isomorphism as a way to translate between proof theory and computer science, and it maps programs to proofs, not to axioms.