Yes, there are lots of these - and the relevant notion is the arithmetic hierarchy.
There's a potential point of confusion worth addressing here, especially since it appeared in a now-deleted answer: we cannot conflate "true in $\mathbb{N}$" with "provable in $\mathsf{PA}$." In particular, for each formula $\varphi$ the set $$\{x: \mathsf{PA}\vdash\varphi(x)\}$$ is indeed r.e., but that does not mean that the set $$\{x: \mathbb{N}\models\varphi(x)\}$$ need be anywhere close to r.e.
Here's a brief summary. Every formula $\psi$ in the language of arithmetic is ($\mathsf{PA}$-provably) equivalent to one of the form $$Q_1x_1Q_2x_2....Q_nx_n\varphi(x_1,...,x_n)$$ where each $Q_i$ is a quantifier (either $\forall$ or $\exists$) and $\varphi$ uses only bounded quantifiers (quantifiers of the form $\forall y<n$ and $\exists y<n$). We can get an upper bound on the complexity of the set defined by $\psi$ by looking at:
the outermost quantifier $Q_1$, and
the number of quantifier alternations ("$\forall\exists$" or "$\exists\forall$" - this can be much less than the total number of quantifiers).
A formula of the above type whose outer quantifier is $\exists$ and which has $i$-many quantifier alternations is called $\Sigma_{i+1}$; a formula whose outer quantifier is $\forall$ and which has $i$-many quantifier alternations is called $\Pi_{i+1}$.
The first part of the connection between the arithmetic hierarchy and computational complexity is the following:
A set is r.e. iff it is definable by a $\Sigma_1$ formula.
See here. More generally, there is a connection between the arithmetical hierarchy on the one hand and Turing reducibility and the Turing jump and :
For each $n\in\mathbb{N}$ we have $X\le_T{\bf 0^{(n)}}$ iff $X$ is definable by a $\Sigma_{n+1}$ formula and $X$ is definable by a $\Pi_{n+1}$ formula.
This is due to Post. You may also find Shoenfield's limit lemma to be of interest. The simplest natural example of an arithmetic set which is not r.e., or indeed Turing-equivalent to any r.e. set (to rule out things like "the complement of the halting problem") is in my opinion the set of indices for Turing machines which halt on all inputs. This set, which is often denoted "$\mathsf{Tot}$" (for "total"), has Turing degree ${\bf 0''}$ and is $\Pi_2$ but not $\Sigma_2$.
(We say that a set is $\Sigma_n$ if it is definable by a $\Sigma_n$ formula, and similarly for $\Pi_n$; additionally, we say that a set is $\Delta_n$ iff it is both $\Sigma_n$ and $\Pi_n$. Note that there is no such thing as a "$\Delta_n$ formula" - whereas $\Sigma_n$-ness and $\Pi_n$-ness are syntactic properties, $\Delta_n$-ness is genuinely "semantic.")
Another important class of examples comes from the notion of bounded truth predicates. Per Tarski, the set $$\{\ulcorner\psi\urcorner: \mathbb{N}\models\psi\}$$ is not arithmetical (here "$\ulcorner\cdot\urcorner$" is your favorite Godel numbering function). However, for each $n$ the set of Godel numbers of true $\Sigma_n$ sentences is indeed $\Sigma_n$. The set of Godel numbers for false $\Sigma_n$ sentences (or Turing-equivalently the set of Godel numbers of true $\Pi_n$ sentences) is therefore $\Pi_n$ but not $\Sigma_n$. Similarly, the set of Godel numbers of false $\Pi_n$ sentences (or Turing-equivalently the set of Godel numbers of true $\Sigma_n$ sentences) is $\Sigma_n$ but not $\Pi_n$. Now just pick some really big $n$ (that is, $n>1$).
Best Answer
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.