I’m (re?)learning formal logic from Margaris (1990). Here are some excerpts from the introduction
Quote
The definition of statement above is formal because it involves only the form of certain expressions, not their meaning. The axiomatic theories we shall study are formal axiomatic theories. The axiomatic theories of everyday mathematics are informal theories. In an informal theory, the statements are made in a natural language (e.g., English). Symbols are used, but they are abbreviations for meaningful words and phrases. In a formal theory, the statements are written in a specially constructed symbolic language and are manipulated in accordance with specified rules which make no appeal to any possible meaning of the statements.
Quote
A formal proof leaves nothing to the imagination. There is an effective procedure for deciding whether or not a formal proof is correct. Every step can be checked to see if it is justified as an axiom or by some rule of inference, with the checker relying only on the forms of the steps-not their meaning. No intelligence beyond the ability to follow routine instructions is necessary to check a formal proof. A digital computer can be programmed to check formal proofs.
Formal logic is not concerned with meaning. It is a set of abstract rules of reasoning within a predetermined domain.
→ nothing prevents us from having true contradictions if we pick the right axioms. → formal logic can inform us about the consequences of that choice.