Extensions of First-Order Logic

PREFACE
CHAPTER I: STANDARD SECOND ORDER LOGIC
 1.- Introduction
  1.1. General idea
  1.2. Expressive power
  1.3. Model-theoretic counterparts of expressiveness
  1.4. Incompleteness
 2.- Second order grammar
  2.1. Definition (signature and alphabet)
  2.2. Expressions: terms, predicates and formulas
  2.3. Remarks on notation
  2.4. Induction
  2.5. Free and bound variables
  2.6. Substitution
 3.- Standard structures
  3.1. Definition of standard structures
  3.2. Relations between standard structures established without the formal language
 4.- Standard semantics
  4.1. Assignment
  4.2. Interpretation
  4.3. Consequence and validity
  4.4. Logical equivalence
  4.5. Simplifying our language
  4.6. Alternative presentation of standard semantics
  4.7. Definable sets and relations in a given structure
  4.8. More about the expressive power of standard SOL
  4.9. Negative results
 5.- Semantic theorems
  5.1. Coincidence lemma
  5.2. Substitution lemma
  5.3. Isomorphism theorem
CHAPTER II: DEDUCTIVE CALCULI
 1.- Introduction
  1.1. General idea
  1.2. Motivations
  1.3. Desired metaproperties of a calculus: soundness and completeness
  1.4. Our second-order calculi
 2.- Sequent calculi
  2.1. Deductions
  2.2. Sequent rules common to all calculi
  2.3. Sequent rules for calculus C2
  2.4. Sequent rules for a calculus including lambda
  2.5. Deductions
  2.6. Derivable rules
  2.7. Equality and comprehension
  2.8. Deduction exercises
 3.- Soundness theorem in standard semantics
  3.1. The soundness of rules common to all three calculi in standard semantics
  3.2. The soundness of lambda rules
  3.3. The soundness of comprehension
 4.- Incompleteness in standard structures
  4.1. Incompleteness of C2 in standard structures
  4.2. Incompleteness of second order logic in standard structures (strong sense)
  4.3. Incompleteness of second order logic in standard structures (weak sense)
CHAPTER III: CATEGORICITY OF SECOND ORDER PEANO ARITHMETIC
 1.- Introduction
 2.- Second order Peano axioms
  2.1. Definitions: Peano models and induction models
  2.2. Comparison between the second order induction axiom and the first order induction schema
  2.3. Non-standard models
 3.- Categoricity of Peano axioms
  3.0. Partial functions
  3.1. Recursion theorem
  3.2. Relationship between induction models and Peano models
  3.3. Isomorphism of Peano models
  3.4. Peano arithmetic and the theory of natural numbers 127
  3.5. Weak incompleteness of SOL with standard semantics 128
 4.- Peano models and primitive recursion
  4.1. Addition, multiplication and exponentiation in Peano models
  4.2. Theorem: recursive operations in Peano models
 5.- Induction models
  5.1. Induction models and congruences
  5.2. Congruence relations on natural numbers
  5.3. Relative interdependence of Peano axioms
 6.- Induction models and primitive recursion in induction models
  6.1. Addition and multiplication in induction models
  6.2. Exponential operation on induction models
  6.4. Universal operations
CHAPTER IV: FRAMES AND GENERAL STRUCTURES
 1.- Introduction
  1.1. Frames and general structures
  1.2. Standard/nonstandard view
  1.3. The concept of subset
  1.4. Summary
 2.- Second order frames
  2.1. Definition of frames
  2.2. Semantics on frames
  2.3. Soundness and completeness in frames
  2.4. Undefinability of identity in frames
  2.5. Frames and lambdas
  2.6. Definable sets and relations in a given frame
 3.- General structures
  3.1. Definition of general structures
  3.2. Semantics based on general structures
  3.3. General structures and lambdas
  3.4. Soundness and completeness in general structures
 4.- Algebraic definition of general structures
  4.1. Fundamental relations of a structure
  4.2. Algebraic definition of general structures
 5.- Logics obtained by weakening the schema of comprehension
 6.- Weak second order logic
  6.1. General idea
  6.2. Metaproperties of weak second order logic
CHAPTER V: TYPE THEORY
 1.- Introduction
  1.1. General idea
  1.2. Paradoxes and their solution in type theory
  1.3. Three presentations of type theory
 2.- A relational theory of finite types
  2.1. Definition (signature and alphabet)
  2.2. Expressions
  2.3. Equality
  2.4. Free variables and substitution
  2.5. Deductive calculus
  2.6. The relational standard structure and the relational standard hierarchy of types
  2.7. RTT with lambda
  2.8. Incompleteness of standard type theory
  2.9. Relational general structures and relational frames
 3.- Algebraic definition of relational general structures
  3.1. Fundamental relations
  3.2. Definition of relational general structure by algebraic closure of the domains
  3.3. Theorem
  3.4. Some parametrically definable relations also included in the universe of relational general structures defined by algebraic closure
  3.5. Theorem
 4.- A functional theory of types
  4.1. Definition (signature and alphabet)
  4.2. Expressions
  4.3. Functional frames, functional general structures and functional standard structures
  4.4. From RTT to FIT
 5.- Equational presentation of the functional theory of finite types
  5.1. Main features of ETT
  5.2. Connectors and quantifiers in ETT
  5.3. The selector operator in ETT
  5.4. A calculus for ETT
CHAPTER VI: MANY-SORTED LOGIC
 1.- Introduction
  1.1. Examples
  1.2. Reduction to and comparison with first order logic
  1.3. Uses of many-sorted logic
  1.4. Many-sorted logic as a unifier logic
 2.- Structures
  2.1. Definition (signature)
  2.2. Definition (structure)
 3.- Formal many-sorted language
  3.1 Alphabet
  3.2. Expressions: formulas and terms
  3.3. Remarks on notation
  3.4. Abbreviations
  3.5. Induction
  3.6. Free and bound variables
 4.- Semantics
  4.1. Definitions
  4.2. Satisfiability, validity, consequence and logical equivalence
 5.- Substitution of a term for a variable
 6.- Semantic theorems
  6.1. Coincidence lemma
  6.2. Substitution lemma
  6.3. Equals substitution lemma
  6.4. Isomorphism theorem
 7.- The completeness of many-sorted logic
  7.1. Deductive calculus
  7.2. Syntactic notions
  7.3. Soundness
  7.4. Completeness theorem (countable language)
  7.5. Compactness theorem
  7.6. Lowenheim-Skolem theorem
 8.- Reduction to one-sorted logic
  8.1. The syntactical translation (relativization of quantifiers)
  8.2. Conversion of structures
CHAPTER VII: APPLYING MANY-SORTED LOGIC
 1.- General plan
  1.1. Aims
  1.2. Representation theorem
  1.3. Main theorem
  1.4. Testing a given calculus for XL
Applying many-sorted logic to higher order logic
 2.- Higher order logic as many-sorted logic
  2.0. Preliminaries
  2.1. The formal many-sorted language MSL 
  2.2. The syntactical translation
  2.3. Structures
  2.4. The equivalence SOL-MSL
Applying many-sorted logic to modal logic
 3.- Modal logic
  3.1. Some history
  3.2. A formal language for PML
  3.3. Modal propositional logics
  3.4. Normal modal logics
  3.5. Consistency of all normal modal logics contained in S5
  3.6. Kripke models
  3.7. A formal language for FOML
  3.8. Semantics
  3.9. A deductive calculus for FOML(S5)
 4.- Propositional modal logic as many-sorted logic
  4.1. The formal many-sorted language MSL
  4.2. Translating function
  4.3. General structures and frames built on PM-structures
  4.4. The MODO theory
  4.5. Reverse conversion
  4.6. Testing the calculus
 5.- First order modal logic as many-sorted logic
  5.1. The formal many-sorted language MSL
  5.2. Translating function
  5.3. Theorems on semantic equivalence FOML-MSL
  5.4. Metaproperties of FOML-S5: compactness, and Lowenheim-Skolem
  5.5. Soundness and completeness of S5
Applying many-sorted logic to dynamic logic
 6.- Dynamic logic
  6.1. General idea
  6.2. A formal language for PDL
  6.3. Semantics
  6.4. The logic PDL
 7.- Propositional dynamic logic as many-sorted logic
  7.1. The formal many-sorted language MSL
  7.2. Translating function
  7.3. Structures and frames built on PD-structures
  7.4. The SOLO theory
Bibliography
List of notation
Index