Melvin Fitting è un logico con un profondo interesse per la logica filosofica e i sistemi di dimostrazione a tableau. Il suo lavoro è motivato dalla consapevolezza che la logica stessa è molteplice, adattandosi al contesto e all'argomento. Sostiene l'idea che la logica sia uno strumento per esplorare la coerenza, non per affermare la verità assoluta. Fitting si impegna a incarnare posizioni filosofiche all'interno di sistemi formali, dimostrandone la coerenza interna. Considera la logica uno strumento dinamico e piacevole del pensiero.
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.