Project Page Index Table of Contents
  • Decidability of bounded quantifiers.
  • Witness Operator
    • On natural numbers.
    • For product types.
  • Division with Rest
    • Uniqueness
    • Homomorphism property of the modulus.
  • Prime Numbers
    • Irreducible Numbers
    • It is decidable whether a number is irreducible.
    • Every number > 1 has an irreducible factor.
    • Prime and irreducible are equivalent
    • There are infinitely many irreducible numbers.
    • An injective function producing infinitely many irreducible numbers.
  • Proposed new definition of First Order Logic in Coq
    • Substituion lemmas
    • Bounded formulas
  • Natural Deduction
    • Definition
    • Lemmas for context manipulation.
    • Soundness
  • Full Syntax
  • Tarski Semantics
    • Semantic notions
    • Results for bounded formulas.
  • Peano Arithmetic
    • Non-logical symbols used in the language of PA
    • PA Axioms
      • Basic Axioms
      • Induction Scheme
      • Equality Axioms
    • Robinson Arithmetic
    • The Theory PA
    • PA Models
    • Euclidean Lemma
    • Uniqueness for the Euclidean Lemma
    • Standard Model of PA
  • Homomorphism Properties of Numerals
  • Closed terms are numerals.
  • Provability of equality for closed terms is decidable.
  • Tennenbaum's Theorem
    • Preliminaries
      • Synthetic Computability Definitions
      • Standard Model Definition
      • Delta_0 and Sigma_1 Formulas
      • Definition of CT and RT
    • Assuming RT there are recursively inseparable Sigma_1 Formulas.
    • Overspill Lemma
    • Facts about divisibility and order of standard and non-standard numbers.
      • Non-standard numbers are larger than any numeral.
      • Divisibility is decidable if the PA model is a data type
    • Coding Lemma for natural numbers
    • Coding Lemma for non-standard Models.
    • Potentiall existence of a number for which divisibility is not decidable.
    • Tennebaum's Theorem
      • Base Version
      • Witness Operator
      • Weaker Assumptions
      • Makholm
      • McCarty
Generated by coqdoc and improved with CoqdocJS