You must be talking about propositional logic since, as Noah points out in the comments, first-order logic is not decidable. And, as Mauro points out, truth-tables are a perfectly good method to decide whether a propositional logic statements is a tautology or not.
Now, you are asking for a proof as to why truth-tables are indeed such a decision procedure ... but that proof is simply this: A tautology is defined as a statement that for each valuation (truth-assignment) evaluates to true. Well, truth-tables exhaustively explore all possible valuations. To be precise: each valuation will be captured by one of the rows of the truth-table. And, since working out the values in a truth-table corresponds exactly to following the formal semantics according to which valuations are being defined, the eventual truth-value you find in the truth-table is exactly what it should be for that valuation. And finally, working out a truth-table takes a finite amount of time: since any statement in propositional logic is of finite length, there are finitely many propositional logic variables in any statement, and therefore you have a finite number of rows in the truth-table, and working out the truth-value of the statement for each row takes a finite number of steps, corresponding to the finite number of logical operations in the statement.
And so, if in a truth-table you find that the statement always evaluates to true (it takes finite time to check this) then you know that it evaluates to true for all possible valuations, and hence it is a tautology. On the other hand, if in at least one row it evaluates to false (again, you'll find this in finite time), then you know there is a valuation for which the statement is false, and hence the statement is not a tautology.
So yes, truth-tables are a perfectly good decision procedure.
Now, I know this is not your method ... so, what I say about that? Well, first take a look at Wikipedia's page for Propositional Logic:
Here, they start to describe what you want: a set of axioms (all tautologies) which, together with the single inference rule Modus Ponens, allows you to prove other tautologies. Now, you can prove that this set of axioms is complete (the same Wikipedia page has some discussion on completeness), in the sense that all tautologies can indeed be derived from the axioms and Modus Ponens. And that shows that the set of tautologies is recursively enumerable ... but not that the set of non-tautologies is enumerable ... and thus, as you realize, you don't have a decision procedure yet.
Indeed, using formal proofs you can only demonstrate that statements are tautologies, but not that statements are not tautologies (unless the statement happens to be a contradiction, in which case demonstrating (i.e. proving) its negation to be a tautology tells you that the original is not a tautology).
Given this limitation of proof methods it is indeed not at all clear how you would extend that into a decision procedure ... which is exactly why Mauro and I suggest a truth-table method, which can demonstrate both tautologies to be tautologies, and non-tautologies to be non-tautologies,
Now, there are some other methods, though, and one I really like is the semantic tableaux or truth-tree method. This method tries to figure out whether some statement (or set of statements) is satisfiable (i.e. can be made true), and you can show that for propositional logic, this method is in fact a decision procedure for exactly that: if the statement is not satisfiable, then the tableaux will eventually lead to all closed branches, and if it is satisfiable, then the tableaux is guaranteed to lead to at least one open branch (not an easy proof, but not crazy hard either). So, if you have a statement and want to know whether or not it is a tautology, you simply negate the statement, and use the tableaux method to figure out if that negation is satisfiable: if it is, then the original statement is not a tautology, and if it is not, then the original statement is a tautology. Hence, this is a decision procedure for propositional logic.
What's also cool about this method is that, unlike truth-tables, it is a method that you can use for fist-order logic ... though it is no longer a decision procedure for first-order logic, since you can get infinite-length trees. Indeed, as Turing showed, there simply cannot be any decision procedure for first-order logic.
Best Answer
"First, we can check if $w \in A \cup B$. Since this is decidable, we know that either $w \in A$ or $w \in B$."
I am failing to understand your proof right here.
Here is an approach to prove. Instead of reasoning on the level of each input to a Turing machine, let us reason on the level of semi-decidability and decidability.
The conditions areCondition 1 and condition 3 imply
Condition 4 and condition 5 imply
Condition 2 and condition 6 imply $B$ is decidable.
Exercise (provided by Johannes Kloos). Let $A$ and $B$ be semi-decidable languages such that both $A\cup B$ and $A\cap B$ are co-semi-decidable languages. Show that $B$ is decidable.