An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof

Kluwer Academic Publishers (2002)
Abstract
This introduction to mathematical logic starts with propositional calculus and first-order logic. Topics covered include syntax, semantics, soundness, completeness, independence, normal forms, vertical paths through negation normal formulas, compactness, Smullyan's Unifying Principle, natural deduction, cut-elimination, semantic tableaux, Skolemization, Herbrand's Theorem, unification, duality, interpolation, and definability. The last three chapters of the book provide an introduction to type theory (higher-order logic). It is shown how various mathematical concepts can be formalized in this very expressive formal language. This expressive notation facilitates proofs of the classical incompleteness and undecidability theorems which are very elegant and easy to understand. The discussion of semantics makes clear the important distinction between standard and nonstandard models which is so important in understanding puzzling phenomena such as the incompleteness theorems and Skolem's Paradox about countable models of set theory. Some of the numerous exercises require giving formal proofs. A computer program called ETPS which is available from the web facilitates doing and checking such exercises. Audience: This volume will be of interest to mathematicians, computer scientists, and philosophers in universities, as well as to computer scientists in industry who wish to use higher-order logic for hardware and software specification and verification.
Keywords Logic, Symbolic and mathematical  Type theory
Categories (categorize this paper)
Buy the book $59.95 used (65% off)   $103.98 new (39% off)   $125.88 direct from Amazon (26% off)    Amazon page
Call number QA9.A638 2002
ISBN(s) 1402007639   9781402007637
Options
 Save to my reading list
Follow the author(s)
My bibliography
Export citation
Find it on Scholar
Edit this record
Mark as duplicate
Revision history Request removal from index
 
Download options
PhilPapers Archive


Upload a copy of this paper     Check publisher's policy on self-archival     Papers currently archived: 10,747
External links
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library
References found in this work BETA

No references found.

Citations of this work BETA
Sean A. Fulop (2010). Grammar Induction by Unification of Type-Logical Lexicons. Journal of Logic, Language and Information 19 (3):353-381.
Similar books and articles
Analytics

Monthly downloads

Added to index

2009-01-28

Total downloads

114 ( #8,458 of 1,098,869 )

Recent downloads (6 months)

5 ( #57,750 of 1,098,869 )

How can I increase my downloads?

My notes
Sign in to use this feature


Discussion
Start a new thread
Order:
There  are no threads in this forum
Nothing in this forum yet.