Is your position that the term "proof by contradiction" should not be limited to proofs of ¬¬P followed by double negation elimination, and should instead also encompass proofs of ¬P that start with "suppose P, for contradiction"? I agree that this is in keeping with traditional usage.
But I think Andrej Bauer's distinction is hardly unique to him (and I probably first encountered it from a different source). It's simply a way to square two widely-held beliefs, even amongst professional mathematicians (in my experience):
1. Intuitionistic logic does not admit proof by contradiction.
2. The proof that √2 is irrational requires proof by contradiction, and therefore is not intuitionistically valid.
I assume you would prefer to correct the first "misconception", by clarifying that only proofs of positive statements that assume the negative are non-constructive. This is in line with what Bridges says in your link.
The other alternative would be to more narrowly redefine "proof by contradiction" so that it does not apply to the proof of the irrationality of √2. I happen to prefer this because its simplicity appeals to me, but this is a matter of taste and admittedly hard to defend. I've also made peace with the idea that terminology is fluid and can have somewhat varying meanings for different communities and across time.
I think if someone understands the topic well enough to have the discussion we're having, they're unlikely to have the misconception we're talking about. So in that sense, we're engaging in a bit of pedantry.
To be fair, one doesn't need a deep knowledge of the "discipline proper" to realize this. If you're considering the field to be intuitionistic logic or constructive mathematics, I would readily admit that I have a superficial knowledge. If you consider the "discipline" to be mathematics broadly, even this level of knowledge is actually quite uncommon.
Would you care to enlighten us about any of the subtleties of intuitionistic logic that make this a shibboleth, rather than a reasonable view of what a proof by contradiction is?
I agree with what you say about mathematicians, being in an adjacent field myself. However, most mathematicians are not logicians, and we are seldom careful about making distinctions that only matter in non-classical logics. I do think that this particular distinction (between proving negation vs. proving the negation of a negation) is worth making, though.
Even if we are, as a matter of practice, used to invoking the law of the excluded middle without a second thought, I think it's good to keep in mind in which proofs it is actually required and where it is not. So, for example, and to the GP's point, proving ¬Q ⇒ ¬P by proving P ⇒ Q doesn't require LEM, but the converse does.
The trouble is that when translating mathematics to logic, it's often not clear what is a negation and what isn't. Is "x is irrational" the sentence ¬P for P being "x is rational" or is it simply an atomic sentence on its own? One may scoff at these questions (and many of my colleagues do) but I have personally found them helpful to think about, and also relevant now that logic-based computer proof systems are becoming more important to mathematicians.
Also, proving ¬P by assuming P and deriving a contradiction is not "proof by contradiction"! That is just how you prove negations — ¬P is often taken to be syntax sugar for P ⇒ False.
It's only proof by contradiction if you prove P by assuming ¬P and deriving a contradiction. Technically, what you've actually done is proven ¬(¬P). Now if you're a classical logician, you would say that ¬(¬P) is equivalent to P; if you're a constructivist, you wouldn't.
So proof by contradiction isn't in the constructivist's toolbox, with the proviso that many people think they're doing a proof by contradiction when they're not actually.
You probably know this already, but the problem isn't remote desktop into a logged-in session (krdp supports this) but rather logging in remotely into a headless server without a local session running. This is slightly more complicated because the login manager has to get involved and present its UI remotely. This is what that bug is tracking.
The things that "start going really wrong" are listed immediately after that quote, and have nothing to do with the drop-off trajectory. Epic had problems with the ground stations they were using to communicate with their spacecraft. One of the two stations was offline because of a power failure. Then they "discover[ed] an unlikely incompatibility between their transmissions and the ground station hardware."
On a ride share mission, the primary payload determines the target orbit. If Intuitive Machines decides they want to go to a different orbit, then Epic has to deal with it. But they will be told this well before launch, with enough time to plan how many trajectory change maneuvers they need.
But even though they know beforehand how many burns they'll need, their exact parameters have to be calculated after launch once SpaceX uses the rocket's on-board guidance instruments to determine the actual insertion orbit. Usually this is within a few meters per second of the planned orbital velocity, but you need to know that last bit of error to figure out exactly how long the correction burns need to be. This doesn't change the overall maneuver plan, just the fine details.
The problem was that after launch, when SpaceX gave them the information they needed to calculate the burn parameters, they didn't have a working uplink to command their spacecraft to do the burn. So it just stayed on its original trajectory for longer than intended, getting more off-course the whole time.
Passkeys are a public/private keypair, where the service you're authenticating against has the public key and your browser has the private key. To authenticate, the browser demonstrates that it has the private key by signing and returning a challenge sent by the server.
So, unlike API keys, the actual passkey is never sent anywhere out of your device. Passkeys are more like SSH keys than API keys.
One difference between SSH and the WebAuthn protocol is that the challenge identifies which key it is expecting. So the user doesn't have to explicitly select which key to use.
It turns out the acidic environment in most beverages inverts the sucrose in cane sugar to form a 50:50 mix of fructose and glucose. In the end, the fructose/glucose ratio in cane-sugar-sweetened drinks becomes similar to high-fructose corn syrup, which is about 55:42. And the reaction is quick: about half the sucrose gets inverted in about three weeks. [1]
But I think Andrej Bauer's distinction is hardly unique to him (and I probably first encountered it from a different source). It's simply a way to square two widely-held beliefs, even amongst professional mathematicians (in my experience):
1. Intuitionistic logic does not admit proof by contradiction. 2. The proof that √2 is irrational requires proof by contradiction, and therefore is not intuitionistically valid.
I assume you would prefer to correct the first "misconception", by clarifying that only proofs of positive statements that assume the negative are non-constructive. This is in line with what Bridges says in your link.
The other alternative would be to more narrowly redefine "proof by contradiction" so that it does not apply to the proof of the irrationality of √2. I happen to prefer this because its simplicity appeals to me, but this is a matter of taste and admittedly hard to defend. I've also made peace with the idea that terminology is fluid and can have somewhat varying meanings for different communities and across time.
I think if someone understands the topic well enough to have the discussion we're having, they're unlikely to have the misconception we're talking about. So in that sense, we're engaging in a bit of pedantry.
To be fair, one doesn't need a deep knowledge of the "discipline proper" to realize this. If you're considering the field to be intuitionistic logic or constructive mathematics, I would readily admit that I have a superficial knowledge. If you consider the "discipline" to be mathematics broadly, even this level of knowledge is actually quite uncommon.