Free Logic Now!

It’s time to make logic free! Toward this end, I am writing a totally free logic text, suitable for teaching formal logic to undergraduates as well as graduate students. Topics covered will include natural deduction and semantics for propositional and first-order logic with functions and identity; Turing machines and noncomputable functions (including the halting problem), undecidability of first-order logic, and Gödel’s Incompleteness Theorems.
At present, the text contains a working presentation of propositional and first-order logic, with identity. It has a working presentation of Turing machines with a proof of the uncomputability of the halting problem. Turing’s proof of undecidability of first-order logic is being written. I’ve also finished a presentation of the First Incompleteness Theorem, including primitive recursion, Peano arithmetic, omega incompleteness, and so on.
As a preview, here is the current, ‘not ready for primetime’, incomplete draft. Suggestions, comments, and corrections are hereby solicited and welcomed. I have deliberately placed several errors in the text so that it is not subject to the ‘preface paradox’.