Why formal logic definitions are a mess

I have a growing list of complaints. One basic problem with logic is that it tries to be timeless and tries to have the meaning of an expression limited to the words in the expression. Narrative reaches into the past and the future with it's implicit meanings. Here is a list of problems with the definitions of formal logic.

One basic problem is that math co-opts natural language but has no safeguards to ensure that the co-opted version is what people actually use in the midst of a proof. Eg phrase "if A then B" subsumes so many different concepts that the transitivity of the relation is in question, having only been established for the things being subsumed but never for a mixture of such things. Again, there are no guardrails to ensure this. [I actually think Russell was aware of this but, other than admonishing the audience, he proceeds.]

Truth: 

• This is called an 'undefined' constant. It is never established that way. In fact it has a several distinct meanings that are being suppressed for the definition but (inevitably) used in actual practice. There is no way to establish the truth of a proposition using the rules of logic, so what is the point of relying on 'truth' to define logic?
• Put another way, to say "true" is an undefined constant leaves it unclear how we know something is true? For example: "If you count from one to ten then you must pass five". This is true but how can we believe it is the same as the  undefined constant version of "true"? In fact, why would it be? 
  

Circularity: 

• I count three places in the definition of "and" where they use the 'and' concept. Once explicitly, to define 'and' using "and"; and then subtly in the 'newline' needed for additional rules of "detachment". Alternatively you see a definition in terms of truth tables which is un-objectionable but also empty. Also boolean tables have rows and columns which serve as 'and' mechanisms. Those un-acknowledged  mechanism are what actually performs the definition, not the undefined zeros and ones.
• Consider this bit of gibberish:

Logical implication is a logical relation between two propositions in which the second is a logical consequence of the first1234. It means that if the first proposition is true, then the second proposition must also be true2534. Logical implication is also known as implication, logical consequence, implies, or If... then234.

So who defines "logical consequence"? And what is with the "if...then" in the second definitions? 

Overlapped Definitions:

• The idea that there are more logical operators than logical operations shows that the latter have not been factored correctly.
• Isn't it a little embarrassing, every time you say "or" to follow it with "but not both". The word "or" in natural language means choose one and has never meant "both". So, OR and XOR. Which is it? Also, why would natural language speakers find themselves using a locution like "and/or"?
  

Deliberate Obfuscation:

• The meaning of "if A then B" is entirely artificial, co-opting natural language and then adding insult to injury by bullying the reader. It means: replace A with B cuz I said so! To be fair, it is a shorthand for skipping steps and its transitivity is established by ignoring intermediate steps.

Lack of clarity on 'universal' vs 'particular'

• It is elementary in computer programming to distinguish between a class definition and a class instance. The idea is less crisp in textbooks on logic. Mathematicians submit themselves to obfuscating different kinds of sets, so "man", "men", "mankind", "Socrates", ... these are difficult for ma-man Russell.

Non-atomic "atoms":

• The "universal quantifiers" 'for all' and 'there exist' are not fundamental but derived from simpler operations: stepping through elements of a set, testing for each element for pattern match/mis-match, employing different exit strategies for ending the testing. Iteration and pattern matching are clearly more fundamental. So why are these derived concepts taken as starting points? [Answer: so that the ideas of "all" and "some" can apply when we skip the step of defining the iteration/matching/exit.]

Finally, there are serious issues with treating all propositions and entities as equivalent and existing on the same "playing field". Bertrand Russell was the first to express doubts about the types of entities collected in a set but logicians, concerned with the infinite, overlook problems with very finite entities. No one would say, in natural language, that the a dot's color is "red and green". It would be considered incoherent for someone to say a cup was "red or shiny". This un-secured nonsense shows the necessity of treating different types of attribute in different ways.

Update:  There is a different thing wrong with the example of "All men are mortal". You do not need the "All" and the issues it brings with it. Instead you can simply observe that the definition of 'man' adds requirements to the definition of 'mortal'. You do not need any single example for the a priori truth of the statement. I am not sure what Russell's excuse would be for getting this wrong. Another place where he is hoisted on the petard of his own intention/extension ambiguity.