## Lectures on Mathematical Logic, Volume 2In this volume, logic starts from the observation that in everyday arguments, as brought forward by say a lawyer, statements are transformed linguistically, connecting them in formal ways irrespective of their contents. Understanding such arguments as deductive situations, or "sequents" in the technical terminology, the transformations between them can be expressed as logical rules. The book concludes with the algorithms producing the results of Gentzen's midsequent theorem and Herbrand's theorem for prenex formulas. |

### What people are saying - Write a review

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

### Contents

Sequent Calculi for Positive Logic | 5 |

Cuts | 27 |

Continuous Cut Elimination | 46 |

Sequent Calculi for Minimal and Intuitionistic Logic | 67 |

Sequent Calculi for Classical Logic | 88 |

Classes of Algebras Associated to a Calculus | 126 |

Calculi of Formulas | 168 |

Modus Ponens Calculi for Positive Logic | 174 |

The Variants cxqt0 of cxqt | 240 |

The Variants cxqt and cxqt2 of cxqt | 243 |

The Calculi cxqs | 245 |

The Deduction Theorem and Other Metarules for the Calculi ccqt | 248 |

Tautologies of Positive Quantifier Logic | 250 |

Tautologies of Minimal Quantifier Logic | 252 |

Tautologies of Classical Quantifier Logic | 253 |

Selected Topics in Sequential Quantifier Logic | 256 |

Modus Ponens Calculi for Minimal and for Intuitionistic Logic | 181 |

Modus Ponens Calculi for Classical Logic | 185 |

Historical Notes to Chapters 17 | 196 |

Sequent Calculi for Quantifier Logic | 202 |

Sequent Calculi with Qrules | 204 |

The Replacement Theorem and Cut Elimination for Calculi with rep | 212 |

The Substitution Theorem and Cut Elimination for Calculi with sub | 219 |

The Sets SUB | 221 |

The Substitution Theorem Resumed | 226 |

Cut Elimination Resumed | 231 |

Inversion Rules | 233 |

9 Semantical Consequence Operations and Modus Ponens Calculi | 236 |

Relations between Classical and Intuitionistic Derivability | 259 |

Equality Logic | 263 |

Language Extensions with Predicate Symbols | 270 |

Language Extensions with Function Symbols 1 | 274 |

Language Extensions with Function Symbols 2 | 285 |

The Midsequent Theorem | 288 |

Herbrands Theorem for Prenex Formulas | 298 |

Tableaux | 305 |

317 | |

321 | |

### Common terms and phrases

admissible algebra algorithm antecedent arity assume atomic formula bd(a bijection Boolean Boolean algebra Boolean lattice branch carries Chapter classical classical logic conclusion congruence relation connectives consequence operation consider contain cut degree cut elimination cut formula cut rule d-frame deductive situations define definition e-frames eigen eigenvariable element endsequent equations f-terms falsifies finite follows fr(u function hence Heyting algebra holds homomorphism implies inductive hypothesis instances instantiation interdeducible intuitionistic intuitionistic logic inversion rule left premiss Lemma length length(D logical rules M-sequents maximal nodes MK-derivation modus ponens calculi mula node f Observe occur permutation predecessor prepositional principal formula proof of Lemma propositionally Q-rules quantifier recursion reflexivity axiom remain in effect rep(x,y replaced RFC-lattices root piece semantical sequent sequent calculi side formula sub(x,t subderivation subformula succedent tableau tion transformed upper neighbour variables weakening whence