## Extensions of First Order LogicClassical logic has proved inadequate in various areas of computer science, artificial intelligence, mathematics, philosopy and linguistics. This is an introduction to extensions of first-order logic, based on the principle that many-sorted logic (MSL) provides a unifying framework in which to place, for example, second-order logic, type theory, modal and dynamic logics and MSL itself. The aim is two fold: only one theorem-prover is needed; proofs of the metaproperties of the different existing calculi can be avoided by borrowing them from MSL. To make the book accessible to readers from different disciplines, whilst maintaining precision, the author has supplied detailed step-by-step proofs, avoiding difficult arguments, and continually motivating the material with examples. Consequently this can be used as a reference, for self-teaching or for first-year graduate courses. |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

STANDARD SECOND ORDER LOGIC | 1 |

Standard structures | 22 |

Standard semantics | 30 |

Semantic theorems | 62 |

DEDUCTIVE CALCULI | 69 |

Sequent calculi | 75 |

Soundness theorem in standard semantics | 90 |

Incompleteness in standard structures | 94 |

Algebraic definition of relational general structures | 197 |

A functional theory of types | 205 |

Equational presentation of the functional theory of finite types | 214 |

MANYSORTED LOGIC | 220 |

Structures | 227 |

Substitution of a term for a variable | 236 |

Reduction to onesorted logic | 257 |

APPLYING MANYSORTED LOGIC 236 | 263 |

CATEGORICITY OF SECOND ORDER PEANO ARITHMETIC | 115 |

Categoricity of Peano axioms | 122 |

Peano models and primitive recursion | 129 |

Induction models | 135 |

Induction models and primitive recursion in induction models | 140 |

Second order frames | 154 |

Algebraic definition of general structures | 171 |

TYPE THEORY | 180 |

A relational theory of finite types | 187 |

Applying manysorted logic to higher order logic | 277 |

Applying manysorted logic to modal logic | 291 |

Prepositional modal logic as manysorted logic | 312 |

First order modal logic as manysorted logic | 327 |

Applying manysorted logic to dynamic logic | 335 |

352 | |

369 | |

### Common terms and phrases

binary relation cartesian product Chapter comprehension schema congruence relation consequence continuum hypothesis definable relations definition domain dynamic logic eOPER.SYM equality equivalence expression of type extensionality FOML formal language frames FREE(<p FUNC Henkin homomorphism hypothesis identity individual variables induction model interpretation introduced isomorphism Kripke Lowenheim-Skolem many-sorted language many-sorted logic many-sorted structure mathematical universe membership relation metalanguage modal logic n-ary function n-ary relation natural numbers non-standard normal modal logic obtained one-sorted OPER.CONS operation parametrically definable Peano arithmetic Peano model predicate Proposition prove quantifiers recursive relation constant relation variables relational general structure rules satisfies schema second order language second order logic second order relations second order structure sequent set of formulas set of sentences set theory set-theoretical sets and relations signature standard semantics standard structures TRANS TRANS(<p translation truth value type theory unary universe of individuals valid