>>11066223Many instructions that are set comprehensions in set theory are (but not only) primitive in type theoretic (product, disjoint sum, function space) and those come with explicit construction rules. The language then has not only proposition but also judgements. E.g. you can make the judgement
(3,7) : N x N
where 3 is short for SSS0 and N ist defined (effectively axiomatically, if your theory is so weak you can't model it) as (rather generic) type with only two "axioms"
0 : N
S : N -> N
A statement of the form "a : A" (a judgement) is not a proposition you can use as subexpression in other sentence.
The type of a term is unique in this framework (unlike set theory, where both {3, N} And {{3,5},3} are set containing 3)
Type theory isn't a mathatical theory written down in logic. Instead, the theory is a logic. And more, it's a proof relevant logic.
And it embeds other logics . E.g. considering the type of Propositions Prop and consider two generic propositions (Think P:Prop and Q:Prop and R:Prop and universally quantify over them, i.e. consider P and Q variables in the following), then
((P->Q) x P) -> P
is inhabited (the term is "(f,p) mapsto ,f(p)")
And so is, for example)
(P->R x Q-> R) -> ((P + Q) -> R)
(via "(f,g) mapsto ((p or q) mapsto If (p typecheck against P) then return f(p) else return g(q)))")
The first example is modus ponems, the second says that "and" is stonger than "or".
All mathematical propositions have a type in that sense that's equivalent to them (at least with term axioms). All intuitiinistic propositions are constructible (have algorithms in terms of functions, pairs and sums for implications, and and ors) unconditionally (see Coq).
Google for Curry-Howard
