First-Order Modal Logic

Preface
	What\'s in This Book
	How to Read This Book
	Differences from the First Edition
Acknowledgments
Contents
Part I Background: Propositional Classical Logic
	1 Background: Propositional Language
		1.1 Introduction
		1.2 The Propositional Language
		1.3 Using Induction
		Exercises
	2 Background: Propositional Axiomatics
		2.1 Truth Tables
		Exercises
		2.2 Axiom Systems
		2.3 The Goal and General Outline
		Exercises
		2.4 Consistency and Lindenbaum\'s Lemma
		Exercises
		2.5 Implication and the Deduction Theorem
		Exercises
		2.6 The Other Connectives
			2.6.1 Conjunction
			2.6.2 Disjunction
			2.6.3 Negation
			2.6.4 Implication
		Exercises
		2.7 Summary of Our Classical Axiom System
		Exercises
		2.8 Completeness At Last
		2.9 Redefining Consistency
	3 Background: Propositional Tableaus
		3.1 Tableaus
		Exercises
		3.2 Logical Consequence Using Tableaus
		Exercises
		3.3 Tableau Soundness
		Exercises
		3.4 Tableau Completeness
			3.4.1 Hintikka Sets
			3.4.2 Completeness, Constructively
			3.4.3 Tableau Completeness, Non-constructively
			3.4.4 Coda
		Exercises
		3.5 Strong Completeness and Compactness
		Exercises
		References
Part II Propositional Modal Logic
	4 Modal Logic, an Introduction
		4.1 What Is a Modal?
		Exercises
		4.2 Can There Be a Modal Logic?
		4.3 Aristotle\'s Modal Square
		4.4 Informal Interpretations
		Exercises
		4.5 Temporal Interpretations
		Exercises
		4.6 Historical Highlights
			4.6.1 Aristotle\'s Development of the Square
		Exercises
			4.6.2 Aristotle\'s Future Sea Battle
		Exercises
			4.6.3 The Master Argument of Diodorus Cronus
			4.6.4 The Once and Future Conditional
			4.6.5 The Reality of Necessity
		References
	5 Propositional Modal Logic
		5.1 What Are the Formulas?
		Exercises
		5.2 What Are the Models?
		Exercises
		5.3 Examples
		Exercises
		5.4 Modal Logics, Semantically Defined
		Exercises
		5.5 The Modal Cube
		Exercises
		5.6 Semantic Consequence
		Exercises
		References
	6 Propositional Modal Axiom Systems
		6.1 The Logic K Axiomatically
		Exercises
		6.2 More Axiom Systems
		Exercises
		6.3 Logical Consequence, Axiomatically
		Exercises
		6.4 Axiom Systems Work
			6.4.1 Soundness
			6.4.2 Completeness
		Exercises
		6.5 Informal Notes
			6.5.1 Gödel\'s Intuitionistic Logic Interpretation
			6.5.2 Epistemic Logic
			6.5.3 The Knowability Paradox
		6.6 Justification Logic
		Exercises
		References
	7 Propositional Modal Tableaus
		7.1 Tableaus
		Exercises
		7.2 More Tableau Systems
		Exercises
		7.3 Logical Consequence and Tableaus
		Exercises
		7.4 Modal Tableau Soundness
		Exercises
		7.5 Modal Hintikka Sets
		7.6 Propositional Modal Tableau Completeness
			7.6.1 Modal Tableau Completeness, Constructively
			7.6.2 Logical Consequence
			7.6.3 Modal Completeness, Non-constructively
		Exercises
		7.7 Other Kinds of Tableaus
			7.7.1 Priest Style Tableaus
			7.7.2 Negri Style Tableaus
			7.7.3 Hybrid Logic Tableaus
		References
Part III First-Order Modal Logic
	8 Quantified Modal Logic
		8.1 First-Order Modal Formulas
		Exercises
		8.2 An Informal Introduction
		Exercises
		8.3 Necessity De Re and De Dicto
		Exercises
		8.4 Is Quantified Modal Logic Possible?
		Exercises
		8.5 What the Quantifiers Quantify Over
		Exercises
		8.6 Constant Domain Models
		Exercises
		8.7 Varying Domain Models
		Exercises
		8.8 Free Logic, Briefly
		8.9 Different Media, Same Message
		Exercises
		8.10 Barcan and Converse Barcan Formulas
		Exercises
		References
	9 First-Order Modal Tableaus
		9.1 Constant Domain Modal Tableaus
		Exercises
		9.2 Varying Domain Tableaus
		Exercises
		9.3 Varying Domain Tableau Soundness
		9.4 Hintikka Sets (Again)
		Exercises
		9.5 Tableau Completeness with Quantification
		Exercises
		9.6 The Completeness Proof, an Example
		9.7 Completeness Using Maximal Consistency
		References
	10 First-Order Modal Axiomatics
		10.1 A Classical First-Order Axiom System
		Axiom Schemes
		Rules of Inference
		Exercises
		10.2 So What Are the Problems?
		10.3 Constant Domain Systems
		Exercises
		10.4 Varying Domain Systems
		Exercises
		References
Part IV Equality and Existence
	11 Equality
		11.1 Classical Background
		Exercises
		11.2 Frege\'s Puzzle
		Exercises
		11.3 The Indiscernibility of Identicals
		Exercises
		11.4 The Formal Details
		Exercises
		11.5 Tableau Equality Rules
		Exercises
		11.6 Tableau Soundness with Equality
		11.7 Hintikka Sets with Equality
		11.8 Tableau Completeness with Equality
		11.9 An Example
		Exercises
		References
	12 Existence
		12.1 To Be
		Exercises
		12.2 Tableau Proofs
		Exercises
		12.3 The Paradox of NonBeing
		12.4 Deflationists
		12.5 Parmenides\' Principle
		12.6 Inflationists
		Exercises
		12.7 Unactualized Possibles
		Exercises
		12.8 Barcan and Converse Barcan, Again
		Exercises
		12.9 Using Validities in Tableaus
		Exercises
		12.10 Tableaus Imitate Tableaus
		12.11 On Symmetry
		Exercises
		References
Part V Predicate Abstraction and Scope
	13 Predicate Abstraction, Informally
		13.1 Why Constants Should Not Be Constant
		13.2 Scope
		13.3 The De Re/De Dicto Distinction, More Examples
		13.4 The De Re/De Dicto Distinction: History
		13.5 Understanding the Distinction: Possible Worlds and Scope
		Exercises
		13.6 Predicate Abstraction: Informal Discussion
		13.7 The Scope Distinction and Predicate Abstraction: Informal Discussion
		13.8 Reading Predicate Abstracts
		Exercises
		13.9 Actuality
		13.10 What Is the Actuality Operator?
		References
	14 Predicate Abstraction, Formally
		14.1 Constant Symbol Syntax
		14.2 Constant Symbol Semantics, Always Designate Case
		Exercises
		14.3 Function Symbol Syntax
		14.4 Function Symbol Semantics, Always Designate Case
		Exercises
		14.5 Partiality and Designation
		14.6 Non-Designation Formally
		Exercises
		14.7 What We Still Can\'t Say
		14.8 Extending The Notation to Predicates
		References
	15 Tableaus for Predicate Abstraction
		15.1 Quantification and Non-rigidity
		15.2 Object Terms Syntactically
		15.3 Being on a Branch
		15.4 Constant Domain Tableau Rules
			15.4.1 Constant Domains Assuming Terms Always Designate, CA
			15.4.2 Constant Domains Assuming Terms Might Not Designate, CN
		Exercises
		15.5 Varying Domain Tableau Rules
			15.5.1 Varying Domains, Assuming Terms Always Designate, VA
			15.5.2 Varying Domains, Assuming Terms Might Not Designate, VN
		Exercises
		Reference
	16 Tableau Soundness and Completeness
		16.1 Object Terms Semantically
		Exercises
		16.2 A Technical Result
		16.3 Soundness for K (VN Version)
			16.3.1 Predicate Abstraction
				16.3.1.1 The Positive Abstract Rule
				16.3.1.2 The Negative Abstract Rule
				16.3.1.3 Equality, The Reflexivity Rule
				16.3.1.4 Equality, The General Substitutivity Rule
		Exercises
		16.4 Hintikka Sets for K (VN Version)
		Exercises
		16.5 Adding A Witness World
			16.5.1 Construction of Hw from H
		16.6 Hintikka\'s Lemma, First Pass
		Exercises
		16.7 Hintikka\'s Lemma, Second Pass
		16.8 Completeness for K (VN Version)
		Exercises
Part VI Applications
	17 Equality and Predicate Abstraction
		17.1 The Role of Scope
		17.2 More Examples
		Exercises
	18 Designation
		18.1 Designation and Existence
		Exercises
		18.2 Existence and Designation
		Exercises
		Reference
	19 Rigidity
		19.1 Rigid Designators
		Exercises
		19.2 Rigidity Formally
		Exercises
		19.3 Rigidity That Isn\'t Strong
		19.4 A Dynamic Logic Example
		References
	20 Definite Descriptions
		20.1 Two Theories of Descriptions
		20.2 Definite Description Syntax
		Exercises
		20.3 Semantics for Definite Descriptions
		20.4 Some Examples
		Exercises
		20.5 Russell\'s Approach
		Exercises
		20.6 Our Strong Recommendations
		20.7 Tableaus for Definite Descriptions
			20.7.1 On Origins
		Exercises
		20.8 Tableau Examples
		Exercises
		20.9 Soundness, With Definite Descriptions
		Exercises
		20.10 Hintikka Sets
		20.11 Hintikka\'s Lemma
		20.12 Completeness
		References
Afterword
Index