# What is the name of proofs with (without) Axiom of Choice

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?
• Without AC: 'constructive'. With AC: 'non-constructive' if it's actually referred to. – user117644 Feb 20 '15 at 8:53
• 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}$. – Martin Sleziak Feb 20 '15 at 8:59
• 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.) – Brian M. Scott Feb 20 '15 at 9:37
• 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". – Asaf Karagila Feb 20 '15 at 9:45
• @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. – Hanul Jeon Feb 21 '15 at 2:50