Logic is the study of dependence-relations holding among statements. Two statements stand in such a relation if the truth of one of them is relevant in some way to the truth of the other. The primary relevance-relations are entailment (P entails Q if it is not possible for Q to be false if P is true), confirmation (P confirms Q if P raises the probability of P), disconfirmation (P disconfirms Q if P lowers the probability of Q), and incompatibility (P is compatible with Q if P entails not-Q).
Formal, or ‘mathematical’ logic, is the discipline that attempts to automate the making of inferences. To ‘automate’ the making of some class of inferences is to identify a recursive function (a function defined for its own outputs) that generates those inferences on the basis of a small number of axioms (statements that are simply assumed to be true).
For a number of reasons, it turns out that rather serious limits to what can be done in the way of automating the making of inferences. The best known limits relate to Godel’s incompleteness result (which is an analogue of a result generated in 1880 by George Cantor), but the most significant such limitations are quite math-light and easily articulated.