Except in some degenerate cases, all proof systems contain rules of inference. They are what allow you to derive new theorems from old theorems. That is, even a proof system for classical propositional logic will include rules of inference. The most commonly available one is Modus Ponens.
Tautologies are definitely not things that are true by definition. The typical definition of "tautology" is: a formula of propositional logic is a tautology if and only if, when interpreted as a Boolean function, it is the constantly $1$ function. The set of tautologies is just a set of formulas. This subset of formulas is computable using the normal truth table approach.
A theorem is a formula that can be derived in our proof system. An axiom is a formula that is taken to be a theorem by fiat.
At no point in the above do I talk about "adopting" things as "true".
As Henning Makholm states, the point is to include all (substitution instances of) formulas provable in classical propositional logic as provable within classical first-order logic. However, first-order logic has additional formulas beyond propositional ones which would not be tautologies even if they were provable within classical first-order logic.
A proof system is like an unending jigsaw puzzle. Axioms are like the pieces of the puzzle. Rules of inference tell you when you're allowed to add a puzzle piece to an existing picture. Theorems are any of the pictures you can make. You can choose the axioms and rules of inference however you like (though usually we want to at least restrict things so that we can mechanically check if the rules are followed). There is absolutely no a priori reason this should have anything to do with reasoning.
While our definitions of proof systems and semantics for logics are usually motivated by informal reasoning, they are not defined by it.1 If it turns out informal reasoning works in a way incompatible with what classical first-order logic suggests, say, then that just means classical first-order logic is not a good model for informal reasoning and perhaps another logic would be a better model, not that the definition of classical first-order logic changes to come in line with our informal reasoning.
You are going to be a lot more confused and have a lot of unnecessary difficulty if you don't separate informal reasoning from formal logic. Conflating the two leads to simple questions like whether $A\to B$ is equivalent to $\neg A\lor B$ in classical propositional logic becoming potential philosophical crises. I'm not saying you can't think about the philosophical consequences of such an equivalence holding for informal reasoning, but you can have your philosophical crisis and do your homework too since the question doesn't depend on the resolution to that philosophical question but on the definition of classical propositional logic.
1 At least not directly, and no more than anything else is. We obviously need to use our informal reasoning somewhere to think about anything. The relationship for logic is no different than for, say, group theory or topology.