Please, could you help me make sense of/classify types of deductive reasoning?
When studying mathematical logical, I have noticed there is this Hilbert's axiomatic system (Hilbert calculus) with its inference rules and axioms. We call it deduction when deriving theorems, and sequence of those applied rules is called a formal proof.
But there is also other type of "not so rigorous" deduction, which is somehow based on semantical understanding of the meaning of the words. I will give you an example of what I mean by that: "Suppose that any horse can sit in any chair. Also suppose that cars can fly and can carry things of any weight and any size on its seats. ==> Therefore I deduce that any horse can fly." - there could definitely be a better example but I think it illustrates you what I mean by this "type" of "everyday" deduction.
Than there is this next kind of deduction, which is somehow right between those two deductions in terms of their "rigorousness" - deduction used in most of the mathemacal proofs (informal proofs). This type of deduction also uses semantic understanding, but somehow more strictly than in the previous example (maybe?). Maybe there is another type, I am not sure.
Also there is a difference between those types of deductive reasoning in explicitly stating the rules which I use in reasoning (formal proofs) vs. some implicit rules I use (I would call them a "common sense" reasoning rules, but I would appreciate some more detailed descrition of "those rules" we people implicitly use for informal proofs).
Is there any naming convention for those types of deductions? Could you help me make some clear distinction between those "deductions".