# Was Martin-Löf inspired by Peirce when he introduced the dependent sum and dependent product types?

In the following article:

https://plato.stanford.edu/entries/peirce-logic/

it is mentioned that Peirce's introduced the use of the symbols $\Sigma$ and $\Pi$ to express logical sums and products, but also to denote the existential and universal quantifiers. Is the use of these symbols related to their use in, for example, intuitionistic type theory as dependent sum and dependent type?

• No. Probably not. I'd argue that there is too much of a direct analogy between sums/products and there-exists/for-every, to think there is some historical context to their use (other than Euler, etc.) – Not Mike Dec 19 '17 at 8:45