Skip to main content
added 552 characters in body
Source Link
varkor
  • 7k
  • 18
  • 39

The exponential $B^A$ corresponds to the implication (or function space) $A \Rightarrow B$. The reason you have not seen exponentiation explicitly appear in the treatment of propositional logic is that in that setting you can define implication in terms of negation and disjunction, i.e. as $\neg A \lor B$. However, in other settings (such as constructive logic), this is not possible, and implication must be given separately.

There is a distinction to be drawn, though, between the logic of the lattice of subobjects (giving the propositional logic definable within the topos) and the internal language of the topos itself (which is a higher-order logic). We may have exponentials of the subobjects and not general exponentials in the category itself, or vice versa. The exponential is important in toposes for giving constructions of function spaces (like in the category of sets), which is exactly what makes the internal language "higher-order" logic.

If you want to learn more about exponentiation and implication (or, more generally, function types in a type theory), the place to start is the correspondence between the simply-typed $\lambda$-calculus and cartesian-closed categories. The internal language of toposes subsumes the simply-typed $\lambda$-calculus, so this is a simpler starting point.

This other answer about the distinction between $\vdash$ and $\Rightarrow$ in categorical logic might also be helpful.

The exponential $B^A$ corresponds to the implication $A \Rightarrow B$. The reason you have not seen exponentiation explicitly appear in the treatment of propositional logic is that in that setting you can define implication in terms of negation and disjunction, i.e. as $\neg A \lor B$. However, in other settings (such as constructive logic), this is not possible, and implication must be given separately.

If you want to learn more about exponentiation and implication (or, more generally, function types in a type theory), the place to start is the correspondence between the simply-typed $\lambda$-calculus and cartesian-closed categories. The internal language of toposes subsumes the simply-typed $\lambda$-calculus, so this is a simpler starting point.

This other answer about the distinction between $\vdash$ and $\Rightarrow$ in categorical logic might also be helpful.

The exponential $B^A$ corresponds to the implication (or function space) $A \Rightarrow B$. The reason you have not seen exponentiation explicitly appear in the treatment of propositional logic is that in that setting you can define implication in terms of negation and disjunction, i.e. as $\neg A \lor B$. However, in other settings (such as constructive logic), this is not possible, and implication must be given separately.

There is a distinction to be drawn, though, between the logic of the lattice of subobjects (giving the propositional logic definable within the topos) and the internal language of the topos itself (which is a higher-order logic). We may have exponentials of the subobjects and not general exponentials in the category itself, or vice versa. The exponential is important in toposes for giving constructions of function spaces (like in the category of sets), which is exactly what makes the internal language "higher-order" logic.

If you want to learn more about exponentiation and implication (or, more generally, function types in a type theory), the place to start is the correspondence between the simply-typed $\lambda$-calculus and cartesian-closed categories. The internal language of toposes subsumes the simply-typed $\lambda$-calculus, so this is a simpler starting point.

This other answer about the distinction between $\vdash$ and $\Rightarrow$ in categorical logic might also be helpful.

Source Link
varkor
  • 7k
  • 18
  • 39

The exponential $B^A$ corresponds to the implication $A \Rightarrow B$. The reason you have not seen exponentiation explicitly appear in the treatment of propositional logic is that in that setting you can define implication in terms of negation and disjunction, i.e. as $\neg A \lor B$. However, in other settings (such as constructive logic), this is not possible, and implication must be given separately.

If you want to learn more about exponentiation and implication (or, more generally, function types in a type theory), the place to start is the correspondence between the simply-typed $\lambda$-calculus and cartesian-closed categories. The internal language of toposes subsumes the simply-typed $\lambda$-calculus, so this is a simpler starting point.

This other answer about the distinction between $\vdash$ and $\Rightarrow$ in categorical logic might also be helpful.