This seems like it’s trying to be constructivist logic: your claim must construct at least one example of the thing it’s claiming; compare classical logic, which also allows constructing an “excluded middle” claim, ie a claim that some claim must either be true or not be true, and therefore if you can reason about either case, you can say something about all cases without ever having been able to construct an example that witnesses it being true or not true.
But constructivist logic still involves “not” statements and allows proof by contradiction. In constructivist logic, proof by contradiction must construct an example of the mathematical object which contradicts the negated theorem.
In constructivist logic, proof by contradiction must construct an example of the mathematical object which contradicts the negated theorem.
This isn’t true. In constructivist logic, if you are trying to disprove a statement of the form “for all x, P(x)”, you do not actually have to find an x such that P(x) is false—it is enough to assume that P(x) holds for various values of x and then derive a contradiction. By contrast, if you are trying to prove a statement of the form “there exists x such that P(x) holds”, then you do actually need to construct an example of x such that P(x) holds (in constructivist logic at least).
The way I think of it, is that constructivist logic allows “proof of negation” via contradiction which is often conflated with “proof by contradiction”. So if you want to prove ¬P, it’s enough to assume P and then derive a contradiction. And if you want to prove ¬¬P, it’s enough to assume ¬P and then derive a contradiction. But if you want to prove P, it’s not enough to assume ¬P and then derive a contradiction. This makes sense I think—if you assume ¬P and then derive a contradiction, you get ¬¬P, but in constructivist logic there’s no way to go directly from ¬¬P to P.
Proof of negation (allowed): Prove ¬P by assuming P and deriving a contradiction
Proof by contradiction (not allowed): Prove P by assuming ¬P and deriving a contradiction
This seems like it’s trying to be constructivist logic: your claim must construct at least one example of the thing it’s claiming; compare classical logic, which also allows constructing an “excluded middle” claim, ie a claim that some claim must either be true or not be true, and therefore if you can reason about either case, you can say something about all cases without ever having been able to construct an example that witnesses it being true or not true.
But constructivist logic still involves “not” statements and allows proof by contradiction. In constructivist logic, proof by contradiction must construct an example of the mathematical object which contradicts the negated theorem.
This isn’t true. In constructivist logic, if you are trying to disprove a statement of the form “for all x, P(x)”, you do not actually have to find an x such that P(x) is false—it is enough to assume that P(x) holds for various values of x and then derive a contradiction. By contrast, if you are trying to prove a statement of the form “there exists x such that P(x) holds”, then you do actually need to construct an example of x such that P(x) holds (in constructivist logic at least).
The way I think of it, is that constructivist logic allows “proof of negation” via contradiction which is often conflated with “proof by contradiction”. So if you want to prove ¬P, it’s enough to assume P and then derive a contradiction. And if you want to prove ¬¬P, it’s enough to assume ¬P and then derive a contradiction. But if you want to prove P, it’s not enough to assume ¬P and then derive a contradiction. This makes sense I think—if you assume ¬P and then derive a contradiction, you get ¬¬P, but in constructivist logic there’s no way to go directly from ¬¬P to P.
Proof of negation (allowed): Prove ¬P by assuming P and deriving a contradiction
Proof by contradiction (not allowed): Prove P by assuming ¬P and deriving a contradiction