So I have been learning Hilbert style FOL from "Introduction to Mathematical Logic" but some people say that it is impractical. On the other hand , I want to study axiomatic set theory , real-analysis etc using a FOL deductive system. So I have been trying to learn Fitch-style Natural Deduction for Propositional and Predicate Calculus.

The textbook I am trying to find should have the following things:

(1)FOL syntax.
(2)A logical deductive system (Natural Deduction fitch style).
(3)Conventional and self contained.
(4)Should be Concise.
(5)Only requires pen and paper.

I have found one book "Language, Proof and Logic" but I found it a bit too wordy for It has a lot of exercises which requires the programmes provided with the paid version of the book.I have the free version,So I might miss out on a lot of things I could have learned.I haven't been able to find any other book about this subject.Does anyone know of a textbook where I can learn this kind of Deductive system to use for all mathematics?

  • $\begingroup$ If you want to master the basic methods of mathematical proof, may I humbly suggest my DC Proof 2.0 freeware with accompanying interactive tutorial that is downloadable from my homepage: dcproof.com It is based on a form of natural deduction that is implicitly used in most math textbooks. It is not standard FOL or Fitch-style. $\endgroup$ Commented Jul 26, 2021 at 14:51
  • $\begingroup$ You can search for F.B.Fitch, Symbolic Logic: An Introduction in libraries. $\endgroup$ Commented Sep 23, 2021 at 14:30
  • $\begingroup$ but there are many textbooks with ND: van Dalen as well as Chiswell & Hodges $\endgroup$ Commented Sep 23, 2021 at 14:32
  • 1
    $\begingroup$ @MauroALLEGRANZA: The asker was looking for a textbook with a practical deductive system. So, unfortunately, almost all logic texts including those two you mentioned are useless for this purpose, because they are books that study logic rather than teach how to use logic to do mathematics. For example, van Dalen's system starts with only ∧,→,⊥,∀ as primitive and defines the others in terms of those. That's good for studying FOL (less cases), but bad for using FOL. $\endgroup$
    – user21820
    Commented Sep 24, 2021 at 14:19
  • 1
    $\begingroup$ Also, C&H is wrong in their claim "Sometimes in mathematics one would like to allow structures with empty domains, but these occasions are too few to justify abandoning natural deduction.", because there are ND systems and Fitch systems that work for empty structures. In fact I even recommend my Fitch-style system over other systems. And here is a sequent-style counterpart. $\endgroup$
    – user21820
    Commented Sep 24, 2021 at 14:20

1 Answer 1


forall x checks all the points in your list. It doesn't discuss examples from concrete mathematical theories, but it introduces the formalism generally enough to be applicable to set theory and the like, and is well-written i.m.o., and completely free.

  • $\begingroup$ Please don't recommend forallx next time as it causes serious conceptual misunderstandings. I also didn't know until multiple people came to me with questions about that book. If you find another free introductory logic text with a Fitch-style deductive system, please let me know as I could not find any except LPL. I also have my own, but it is not for really beginner-level consumption, though I use it in my teaching. $\endgroup$
    – user21820
    Commented Jul 30, 2021 at 13:43
  • $\begingroup$ Thanks for letting me know, I'll have a look at the chat messages you linked. $\endgroup$ Commented Jul 30, 2021 at 14:20
  • 2
    $\begingroup$ The book is open source, and the sections of the book causing the misunderstanding can be edited on the github page if you think those paragraphs can be improved. $\endgroup$
    – saolof
    Commented Jul 25, 2023 at 7:57

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .