Formal logic distinguishes a sentence being true in a structure from its having a derivation in a proof system. That distinction is the organizing question for this selection. Forall x supplies practice with syntax, truth tables and natural deduction; Sets, Logic, Computation turns attention to semantics, completeness, compactness and computation. If derivation rules still feel arbitrary, begin with the former before asking what a completeness theorem proves.
What to work on
Evaluate a first-order formula in a specified structure and assignment.
Distinguish semantic consequence from formal derivability.
Use compactness to construct a model satisfying infinitely many constraints.
Trace a Turing-machine computation and explain the halting-problem diagonal argument.
A starting text
Sets, Logic, Computation: An Open Introduction to Metalogic — Richard Zach, based on the Open Logic Project. Start with sections 7.2-7.5 on structures, satisfaction and variable assignments and 11.1-11.6 on natural deduction. Continue with 12.8-12.11 on completeness, compactness and Lowenheim-Skolem, then 14.3-14.4 and 15.4 on machines and halting.
Choosing what to read
Keep a small structure beside every quantified formula and evaluate it under explicit variable assignments. Write a derivation and a semantic explanation of the same consequence, marking where their methods differ. For compactness, spell out the enlarged language and check finite satisfiability rather than invoking the theorem by name. When reading the halting argument, identify the alleged decider's input and output before constructing the contradictory machine.
Connect satisfaction and derivability, then study compactness and halting.
How it reads
Metalogic and computation after elementary formal logic.
What it expects
Quantifiers, elementary sets and some experience with a formal proof system.
What to keep in mind
This reading does not by itself establish arithmetic incompleteness.
Practice
Exercises provided; public solutions not verified. Problems for chapters 7, 11, 12 and 14, beginning on printed pages 133, 224, 253 and 303 respectively.
Complete public PDF.
Edition, reading range and source
Start with sections 7.2-7.5 on structures, satisfaction and variable assignments and 11.1-11.6 on natural deduction. Continue with 12.8-12.11 on completeness, compactness and Lowenheim-Skolem, then 14.3-14.4 and 15.4 on machines and halting.
Metalogic and computation problem sets. Problems for chapters 7, 11, 12 and 14, beginning on printed pages 133, 224, 253 and 303 respectively.. Exercises provided; public solutions not verified.
Try these before moving on
Try a proof or calculation before opening the hint. These solutions address the checks below, not the exercises in the linked textbooks.
Use compactness to show that any first-order theory with arbitrarily large finite models has an infinite model; write the additional sentences explicitly.
A hint
Expand the language by countably many constants and require them to be pairwise distinct. Check an arbitrary finite subset of the expanded theory.
Work through the solution
Let T be a first-order theory with equality, having finite models of unbounded cardinality. Add constants c0,c1,… and put T′=T∪{ci=cj:i<j}. Any finite subset Δ of T′ mentions only finitely many of these constants, say r of them. Choose a model of all of T with at least r elements and interpret those constants as distinct elements (the remaining constants may be interpreted arbitrarily). This expanded model satisfies Δ.
By the compactness theorem, T′ has a model. Its interpretations of all ci are pairwise distinct, so its universe is infinite. Forgetting the new constants gives an infinite model of T. The use of a model of all of T in the finite-subset argument also handles an infinite theory T.
If this was the sticking point:
Proofs & Mathematical Writing — Review the quantifiers in finite satisfiability and the distinction between a finite subset and the whole theory.
Already comfortable with this? Skip the satisfaction and deduction review only if you can evaluate quantified formulas and give rule-by-rule derivations. Skip the whole selection only if you can also prove the compactness application and reconstruct the halting argument without conflating truth and provability.
P. D. Magnus, Tim Button, Aaron Thomas-Bolduc and Richard Zach, with contributors · Textbook · Introductory
Introduces formal languages, truth tables and natural deduction. Exercises and solutions support a first logic course; metatheory is developed further in the next text.
Develops completeness, compactness and undecidability after elementary formal logic. A structured bridge from proof systems to mathematical metatheory.
Purchase or library subscription required; previews are not the complete book.
A compact logical course for readers wanting a focused introduction before longer treatments. Compare formal arguments with ordinary mathematical reasoning.
Heinz-Dieter Ebbinghaus, Jörg Flum and Wolfgang Thomas · Textbook · Graduate · English · Purchase / institutional access
Purchase or library subscription required; previews are not the complete book.
A systematic first-order-logic course on semantics, completeness, computability and limits of formal methods. Work with examples of structures as well as formal deductions.
Yuri I. Manin · Textbook · Graduate · English · Purchase / institutional access
Purchase or library subscription required; previews are not the complete book.
Links foundations with computability and mathematical structures, including a categorical perspective. A mathematically mature alternative to a first introductory course.
Preparation: First-order logic; algebra and mathematical maturity.
John Longley and Dag Normann · Textbook · Research · English · Purchase / institutional access
Purchase or library subscription required; previews are not the complete book.
Studies computation with functionals and higher-type operations. It is a specialist continuation of computability, not an introductory programming book.