This page is an introduction to the textbook and applications that make up Language, Proof, and Logic. It is primarily intended for instructors who are considering adopting LPL. If you are a new user and have questions that are not answered here, we recommend that you read our FAQ.
Language, Proof, and Logic is a textbook and software package, intended for use in undergraduate level logic courses. The text covers topics such as the boolean connectives, formal proof techniques, quantifiers, basic set theory, and induction. The last few chapters include material on soundness, completeness, and Godel's incompleteness theorems.
The book is a completely rewritten and much improved version of The Language of First-order Logic. Introductory material is presented in a more systematic and accessible fashion. The book is appropriate for a wide range of courses, from first logic courses for undergraduates (philosophy, mathematics, and computer science) to a first graduate logic course.
The package includes four pieces of software:
- Tarski's World, a program that teaches the basic first-order language and its semantics;
- Fitch, a natural deduction proof environment for giving and checking first-order proofs;
- Boole, a program that facilitates the construction and checking of truth tables and related notions (tautology, tautological consequence, etc.);
- Submit, a program that allows students to submit exercises done with the above programs to the Grade Grinder, the online grading service.
Grade reports are returned to the student and, if requested, to the student's instructor, eliminating the need for tedious checking of homework. All programs are available for the Windows, Macintosh and Linux platforms. Instructors do not need to use the programs themselves in order to be able to take advantage of their pedagogical value.
Boole is an aid for creating truth-tables. It includes an option to automatically generate the columns of the truth-table, although this option is disabled in the earliest exercises. Boole can be used to check the truth-table, either as it is being built or when it is complete, and to assess sentences of first order logic.Fitch is a tool for building formal proofs in the format presented in LPL. The instant feedback that Fitch provides, in verifying each proof and marking steps that do not check out properly, makes it possible for students to correct and learn from their mistakes without the intervention of an instructor.
Tarski's World is an environment in which students can evaluate sentences of first order logic. The students can create worlds, each of which consists of a chess-like board with blocks of various shapes and sizes positioned on it. Sentences are evaluated in the worlds, which can demonstrate counter-examples to the arguments presented in exercises.
- Tarski's World Screenshots (Macintosh)
Submit is a very different application. It is used to send exercise files created in the other three applications to the Grade Grinder. There are currently two Grade Grinder servers, one at Stanford and one at the University of Chicago. Submit chooses one of the servers to connect to. The student must enter a Book Number, which can be found on the sleeve the CD came in, in order to use Submit. He or she must also enter their name and email address. The instructor's name and email address are optional. After the Grade Grinder verifies the student's Book Number, name, and email address, it receives the files. The files are graded and a grade report is sent out, by email, from the Grade Grinder to the student. If the student has chosen to submit to an instructor as well, the instructor's name and email address are verified and an email is sent to him or her.
- Submit Screenshots (Windows)
More about the Grade Grinder...
