Hello! I was checking this question math.stackexchange.com/questions/333625/… and in the proof of the second argument (2) I think the accepted answer uses (1) to prove x+b=b. Am I missing smt ?
I mean its x + b = (a.(b.c)) + b = (a.(b.c)) + (a.b+a'.b) and then I think the answer uses (a.(b.c))+(a.b+a'.b) = (a.(b.c)+a.b) + a.b to go to (a.(b.c+b))+a.b, no ?
@user21820 if we have defined irrationality as the negation of rationality or connectedness as a negation of disconnectedness is the only way to prove such things (that the number is irrational or that the set is connected) via a proof by negation: A, contradiction => not A?
@giannisl9 Yes it uses (1), but I don't see a problem with that, so I don't really see why you say "you should not use (1)".
But certainly, as you said, you can invoke duality or just mechanically translate the proof for (1) to a proof for (2) via duality.
@famesyasd It depends on what really you mean by "by contradiction" and "only way". If your foundational system is intuitionistic, "irrational" is just "¬rational", and proving something is irrational simply involves ¬intro. No ¬¬elim is needed in that last step. If your foundational system is 3-valued, and you don't even have LEM for ∃ ranging over N, then it's possible that you cannot conclude that every real is either rational or irrational, and even ¬intro won't be allowed.
Specifically, if you prove "if r is rational: contradiction." in 3-valued logic, but "r is rational" is not known to be boolean (either true or false), then you cannot even conclude "r is not rational". But once you accept/believe that rationality is boolean for every real, then you basically have classical logic for rationality.
@user21820 I mean (1) is the associativity law for the + and (2) for the . so, they are the same thing but for another operator. That is why I think that if you want to use (1) to prove (2), just state the duality, if not don't use it at all, prove them separately.
