Is A∨¬A a tautology when there is a proof (by contradiction)?

Question

A∨¬A is stated as a "tautology" but is it really a tautology? It can be proven by counterposition. And therefore it is not a tautology when it can be proven(?)

Update

Here's the proof (by contradiction) I mean:

¬(A∨¬A) (assumption)
   A      (assumption)
   A∨¬A  (rule of introduction)
  人      (contradiction)
 ¬A
 A∨¬A   (rule of introduction)
 人      (contradiction)
¬¬(A∨¬A)
A∨¬A

Answer 1

$A\vee \neg A$ is a tautology in classical (i.e., Aristotelian) logic because you can prove that using the deduction rules of the classical proposition calculus no matter what the truth value of $A$ is, the truth value of $A\vee \neg A$ is always true. That is the meaning of tautology.

In non-classical logical systems, such as intuitionism or constructivism, $A \vee \neg A$ is not a tautology. There the interpretation of $P \vee Q$ is not "either P or Q is true" but rather the more constructive "Either I have a proof of P or I have a proof of Q". A famous example to illustrate this is the following: Theorem: There exist two irrational numbers $a,b$ such that $a^b$ is rational. A classical proof can go like this: if $\sqrt2 ^\sqrt2$ is rational we are done. Else, consider $(\sqrt2^{\sqrt2})^{\sqrt2}=\sqrt2^2=2$, a rational. Classically this finishes the proof but constructively it is not a valid proof since it does not actually show which one of the two candidates works.

Answer 2

Try constructing a truth table and you will see that it is in fact a tautology.

Answer 3

Part of the problem here may be that "tautology" has a far more specific meaning in mathematical logic than in ordinary usage. The more specific meaning is "a statement S that always true, solely on the basis of how S is constructed from smaller statements by means of propositional connectives and the meanings (truth tables) of the connectives". So $A\lor\neg A$ is a tautology because it is true solely because of the meanings of $\lor$ and $\neg$. But $1=1$ is not a tautology because its truth depends on the meaning of $=$, which is not a propositional connective. Similarly, if $P$ is a unary predicate, then $P(a)\to(\exists x)\,P(x)$, though logically valid, is not a tautology because its validity depends on the meanings of both $\to$ and $\exists$, the latter of which is not a propositional connective.

In ordinary, non-technical usage, "tautology" means (according to my dictionary) saying the same thing in different words; I've heard it used more generally to mean anything that is obviously true. So all of the examples in my first paragraph would be tautologies in this sense.