In many contexts we distinguish between proofs using AC and proofs which do not use AC. (To phrase this somewhat differently: If there is a proof without AC, this proof is usually preferred.)

I would like to know whether there are names commonly used for these two types of proofs.

In my mother tongue I have heard the names which could be translated to English as effective-proof (for the proof avoiding AC) and non-effective proof or ineffective proof (for the proofs employing AC).

When I searched for these term on internet 1, 2, 3 and in Google Books 1, 2, 3, I found some hits. But not enough to be persuaded that these two terms are widely used.

So I would like to ask

  • Can some of the names for the proofs with/without AC which I mentioned above considered standard?
  • Are other names for such proofs commonly used?
  • 1
    $\begingroup$ Without AC: 'constructive'. With AC: 'non-constructive' if it's actually referred to. $\endgroup$ – user117644 Feb 20 '15 at 8:53
  • 1
    $\begingroup$ I had the feeling that the phrase constructive proof is often used in different meaning. Wikipedia article I linked mentions famous example of with $\sqrt2^{\sqrt2}$ and $(\sqrt2^{\sqrt2})^{\sqrt 2}$. $\endgroup$ – Martin Sleziak Feb 20 '15 at 8:59
  • 2
    $\begingroup$ I've not run into a pair of terms that could reliably be interpreted that way. Constructive doesn't work, because it frequently excludes much more than just $\mathsf{AC}$, and neither does effective. (I'm curious about your first sentence, though: the only context in which I find any need to make the distinction is that of specifically investigating consequences of $\mathsf{AC}$ and its variants. In any other context I consider its use utterly unremarkable.) $\endgroup$ – Brian M. Scott Feb 20 '15 at 9:37
  • 2
    $\begingroup$ Same as Brian. I don't know a "correct" term. I usually just write "choice free" or "in ZF" or "the axiom of choice is not needed". $\endgroup$ – Asaf Karagila Feb 20 '15 at 9:45
  • 1
    $\begingroup$ @mistermarko "Constructive proof" is different concept with the "proof without AC". König's lemma is provable in ZF without AC, but it is considered to nonconstructive. $\endgroup$ – Hanul Jeon Feb 21 '15 at 2:50

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.