4 ms·

Trying to be maximally precise, the prime G isn’t really constructed, but it must exist because ABC+1 must have a prime factorization by the fundamental theorem

Trying to be maximally precise, the prime G isn’t really constructed, but it must exist because ABC+1 must have a prime factorization by the fundamental theorem of arithmetic. And the contraction is that G can’t be any of {A, B, C}. Edit: The above added a nit-picky side-point to your original response, which was a lot shorter. Afterwards, you edited your reply to be a lot more exhaustive and a lot less... friendly? I don't think that's the best way to use HN's edit window. But see my grandchild comment below for my response to all the points you edited in afterwards.

ogogmad 5y ago
G's existence is proved in a way which is valid in constructive foundations. It is therefore constructed. And this construction can be carried out algorithmically: Just find the prime factors of ABC+1. Obviously, this is not computationally efficient, but constructive logic doesn't care. Constructive logic only cares that a construction can be carried out, and that its worst case time complexity has some explicit bound. The existence of this bound for finding larger primes implies a weak bound on the density of the primes. Also, I made some edits to my original comment.
- codeflo 5y ago
  Yes, you edited your reply to be a lot less polite after you saw my reply to your reply, and I don’t think I did anything to provoke that. I might’ve responded differently if I had realized you were in attack mode. Some points I’d like to clarify: 1. Multiple contradictory edits in the answer is weird by Stack Exchange standards regardless of the merits of the discussion, that’s the main thing I observed. 2. Whether Euclid uses contradiction or not is not really open to interpretation: the word “absurd” appears right in the proof. If people want to split hairs about whether that contradiction is in the lemma or the main proof, I guess fine. 3. There are of course multiple subschools of constructivism that accept and don’t accept different things. Not all of them ignore computational complexity. For example, some ultrafinitists reject the unique prime factorization theorem on the basis that you can’t really execute the factorization algorithm even for relatively modest numbers. To be clear, that’s not exactly my view, but I would for example agree that something like “just find the prime factors” sweeps a bit of relevant subtlety under the rug: you can only do that conceptually, not actually.
  - ogogmad 5y ago
    > Yes, you edited your reply to be a lot less polite after you saw my reply to your reply, and I don’t think I did anything to provoke that. I might’ve responded differently if I had realized you were in attack mode. Sorry. Point taken. I'm way too quick to annoy at the moment, and I retroactively edit too much. I probably should keep my comments relatively unchanged after making them. > If people want to split hairs This entire discussion is about splitting hairs. And the MO answer acknowledges that there's a contradiction somewhere, and only argues over where it is. See the last edit on the answer.
    - codeflo 5y ago
      > Sorry. Point taken. I'm way too quick to annoy at the moment That makes two of us. No offense taken.

ogogmad 5y ago

G's existence is proved in a way which is valid in constructive foundations. It is therefore constructed. And this construction can be carried out algorithmically: Just find the prime factors of ABC+1. Obviously, this is not computationally efficient, but constructive logic doesn't care. Constructive logic only cares that a construction can be carried out, and that its worst case time complexity has some explicit bound. The existence of this bound for finding larger primes implies a weak bound on the density of the primes. Also, I made some edits to my original comment.

codeflo 5y ago
Yes, you edited your reply to be a lot less polite after you saw my reply to your reply, and I don’t think I did anything to provoke that. I might’ve responded differently if I had realized you were in attack mode. Some points I’d like to clarify: 1. Multiple contradictory edits in the answer is weird by Stack Exchange standards regardless of the merits of the discussion, that’s the main thing I observed. 2. Whether Euclid uses contradiction or not is not really open to interpretation: the word “absurd” appears right in the proof. If people want to split hairs about whether that contradiction is in the lemma or the main proof, I guess fine. 3. There are of course multiple subschools of constructivism that accept and don’t accept different things. Not all of them ignore computational complexity. For example, some ultrafinitists reject the unique prime factorization theorem on the basis that you can’t really execute the factorization algorithm even for relatively modest numbers. To be clear, that’s not exactly my view, but I would for example agree that something like “just find the prime factors” sweeps a bit of relevant subtlety under the rug: you can only do that conceptually, not actually.
- ogogmad 5y ago
  > Yes, you edited your reply to be a lot less polite after you saw my reply to your reply, and I don’t think I did anything to provoke that. I might’ve responded differently if I had realized you were in attack mode. Sorry. Point taken. I'm way too quick to annoy at the moment, and I retroactively edit too much. I probably should keep my comments relatively unchanged after making them. > If people want to split hairs This entire discussion is about splitting hairs. And the MO answer acknowledges that there's a contradiction somewhere, and only argues over where it is. See the last edit on the answer.
  - codeflo 5y ago
    > Sorry. Point taken. I'm way too quick to annoy at the moment That makes two of us. No offense taken.