## Logic of ArithmeticFor propositional logic it can be decided whether a formula has a deduction from a finite set of other formulas. This volume begins with a method to decide this for the quantified formulas of those fragments of arithmetic which express the properties of order-plus-successor and of order-plus-addition (Pressburger arithmetic). It makes use of an algorithm eliminating quantifiers which, in turn, is also applied to obtain consistency proofs for these fragments. |

### What people are saying - Write a review

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

### Contents

Consistency Decidability Completeness for the Arithmetic | 10 |

Consistency Decidability Completeness for the Arithmetic | 34 |

Introduction to Chapters 39 | 56 |

Undefinability and Incompleteness General Theory | 71 |

Elementary and Primitive Recursive Functions | 99 |

Recursive Relations andRecursive Functions | 132 |

The Arithmetization of Syntax | 155 |

Consequences of Arithmetization | 165 |

Dependences | 187 |

Axioms for Arithmetic | 190 |

Peano Arithmetic PA and its Expansion PR | 219 |

Unprovability of Consistency | 255 |

Epilogue | 292 |

298 | |

299 | |

### Common terms and phrases

AB-closed algebra algorithm analogous argument arithmetic arity Assume atomic formulas atomic sentences axiom system BEV(x Boolean bounded formulas canonically represented ccqt Chapter characteristic function closed class closed under superposition consistency proofs consistent constant terms contains Corollary deduction definition EB-formula elementary elementary function Entscheidungsproblem equality logic finite fixpoint fk(a follows formally defined free variables function f function symbols graph h A(x,y h Vy hence h holds implies h internal L-formula language Lemma mathematical modulo modus ponens natural numbers Observe obtain open formulas p-bounded PR-terms predicate symbols primitive recursive function propositionally provably equivalent prove provs(G quantifier quantifier elimination recursion equations recursive relations recursively enumerable rep(x rep(y rep(z replaced representability Rx(v satisfying semantically defined sequence statement subset tion true truth Vy y<s(x Vy y<x w-consistent whence