In type theory, what is the difference between the set of functions [tex]A \rightarrow B[/tex] and the implication set [tex]A \supset B[/tex]? Is there any difference? My text says that both of them are examples of sets (propositions) that are defined as special cases of the cartesian product [tex]\prod(A,B)[/tex] (this cartesian product is the set of functions [tex]f(x)[/tex] from the index set [tex]A[/tex] to [tex]B(x)[/tex] where the image of [tex]x[/tex] lies in a set [tex]B(x)[/tex] that is itself dependent on [tex]x[/tex]).(adsbygoogle = window.adsbygoogle || []).push({});

**Physics Forums | Science Articles, Homework Help, Discussion**

Join Physics Forums Today!

The friendliest, high quality science and math community on the planet! Everyone who loves science is here!

The friendliest, high quality science and math community on the planet! Everyone who loves science is here!

# Type Theory Question

Can you offer guidance or do you also need help?

Draft saved
Draft deleted

Loading...

Similar Threads for Type Theory Question |
---|

A About the “Axiom of Dependent Choice” |

B What is the usefulness of formal logic theory? |

I Countability of ℚ |

A Is there a decidable set theory? |

About the strategy of reducing the total suffering in a queue |

**Physics Forums | Science Articles, Homework Help, Discussion**