Logic
Logic makes proof itself the object of study. It fixes a formal language, a precise notion of truth, and rules of inference — then asks what those rules can reach and where they must stop.
Propositional logic comes first. A handful of connectives — and, or, not, implies — combine atoms into formulas, and a truth table settles every question about them by brute enumeration.
Two views run in parallel. Syntax is the game of symbols and inference rules; semantics is what those symbols mean once you interpret them. Keeping the two apart is the whole discipline.
First-order logic adds quantifiers. With for all and there exists ranging over a domain, the language can finally state real mathematics — orderings, arithmetic, the theory of a structure.
The soundness and completeness theorems then tie the two views together: a sentence is provable exactly when it is true in every model. Deduction and truth turn out to be the same reach.
That equivalence makes proof mechanical. Resolution refutes an unsatisfiable set by resolving clauses until it derives the empty clause — a contradiction — which is the engine underneath automated theorem provers.
But mechanising proof runs into a wall. Validity in first-order logic is undecidable, and once a theory can talk about its own arithmetic, it can talk about its own provability.
Gödel's incompleteness theorems close the subject: any consistent theory strong enough for arithmetic has true sentences it cannot prove, and it can never prove its own consistency — the boundary logic set for itself.