> if it is weakened, how can you prove the same stuff?
replySometimes, you can't. In particular, so-called "non-constructive" proofs don't work in intuitionistic logic. Some mathematicians like to work in intuitionistic logic: for philosophical reasons, pragmatic technical considerations, or just because they think it's interesting.
This is not entirely true: non-constructive proofs can be fully understood within intuitionistic logic as proofs of negative statements, viz. statements about what isn't constructively true or doesn't constructively exist. From this point of view, intuitionistic logic can be seen as stronger and more powerful than classical logic, because it can endow positive statements (particularly statements about logical disjunctions or existentials) with computational content whenever they have a direct proof.
replyClassical logic doesn't bother with this; positive and negative statements are completely dual to one another, and this duality is elegant in its own way (as people who are committed to classical logic will readily point out), but one needs linear logic in order to combine it with an awareness of constructive statements.
Having a weaker base system means you can distinguish more fine grained between statements.
replyFor example, in an intuitionistic setting there is a difference between a set being non-empty and a set having an element.
Intuitionistic logic can prove less than classical logic, but what you gain is that proofs are constructive. Also you can use it to reason about things for which law of excluded middle doesn't hold (typically types).
reply