Melvin Fitting est un logicien passionné par la logique philosophique et les systèmes de preuve par tableau. Son travail est motivé par la compréhension que la logique elle-même est multiple, s'adaptant au contexte et au sujet traité. Il défend l'idée que la logique est un outil pour explorer la cohérence, non pour affirmer la vérité absolue. Fitting s'efforce d'incarner des positions philosophiques au sein de systèmes formels, démontrant leur cohérence interne. Il considère la logique comme un instrument dynamique et agréable de la pensée.
Fitting and Mendelsohn offer an in-depth exploration of first-order modal logic, utilizing possible world models, tableau proofs, and philosophical discussions. Key topics include quantification, equality, existence, non-rigid constants, predicate abstraction, and definite descriptions, addressing significant philosophical issues.
Exploring the implications of Russell's paradox, the book delves into the complexities of set theory and logical formulas. It highlights how the collection of sets that do not contain themselves cannot form a set, leading to the conclusion that certain formulas are undefinable. This discussion paves the way for Tarski's result on the undefinability of truth and connects to significant contributions from Gödel, Church, Rosser, and Post, illustrating the profound impact of these ideas on mathematical logic and the foundations of mathematics.
The book delves into Gödel's modal ontological argument within the framework of intensional logic. It begins with a semantic presentation of classical type theory and introduces tableau rules, culminating in a completeness proof. The discussion expands to include modal logic, exploring concepts like extensionality and identity. Various ontological proofs for God's existence are examined, leading to a formalization of Gödel's argument. The author critiques objections, particularly Sobel's challenge regarding Gödel's assumptions, emphasizing the distinction between intensional and extensional interpretations of properties.
This book explores various formal proof procedures developed by logicians, including tableau systems, Gentzen sequent calculi, natural deduction systems, and axiom systems. It covers proof methods for normal and non-normal modal logics, as well as Intuitionistic and Classical logic, providing a comprehensive study of each system's applications and differences.