Extensions of First-Order Logic

Ch 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 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 expressive power of standard SOL
4.9. Negative results
5. Semantic theorems
5.1. Coincidence lemma
5.2. Substitution lemma
5.3. Isomorphism theorem
Ch 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 C_2
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 C_2- 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)
Ch 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 second order induction axiom and 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 theory of natural numbers
3.5. Weak incompleteness of SOL with standard semantics
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
Ch 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 schema of comprehension
6. Weak second order logic
6.1. General idea
6.2. Metaproperties of weak second order logic
Ch 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 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 domains
3.3. Theorem
3.4. Some parametrically definable relations also included in 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 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
Ch 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
Ch 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 logic
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 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
Index