1chapter FOL 2 3session FOL = Pure + 4 description " 5 First-Order Logic with Natural Deduction (constructive and classical 6 versions). For a classical sequent calculus, see Isabelle/LK. 7 8 Useful references on First-Order Logic: 9 10 Simon Thompson, Type Theory and Functional Programming (Addison-Wesley, 11 1991) (The first chapter is an excellent introduction to natural deduction 12 in general.) 13 14 Antony Galton, Logic for Information Technology (Wiley, 1990) 15 16 Michael Dummett, Elements of Intuitionism (Oxford, 1977) 17 " 18 theories 19 IFOL (global) 20 FOL (global) 21 document_files "root.tex" 22 23session "FOL-ex" in ex = FOL + 24 description " 25 Examples for First-Order Logic. 26 " 27 directories "Locale_Test" 28 theories 29 Natural_Numbers 30 Intro 31 Nat 32 Nat_Class 33 Foundation 34 Prolog 35 Intuitionistic 36 Propositional_Int 37 Quantifiers_Int 38 Classical 39 Propositional_Cla 40 Quantifiers_Cla 41 Miniscope 42 If 43 theories [document = false, skip_proofs = false] 44 "Locale_Test/Locale_Test" 45 document_files "root.tex" 46