Skip to content

Latest commit

 

History

History
55 lines (37 loc) · 2.54 KB

README.md

File metadata and controls

55 lines (37 loc) · 2.54 KB

Formalizing Quantifiers

(working with Coq 8.14.1 and OLlibs 2.0.2)

A formalization of quantifiers based on:

  • formulas as first-order structures (no alpha-equivalence);
  • binding for quantifier rules implemented with de Bruijn indices.

It applies to:

  • first-order logics;
  • propositional second-order logics (a la system F for example).

Installation

Requires OLlibs (add-ons for the standard library): see installation instructions.

  1. install OLlibs

  2. install development

     $ ./configure
 $ make
 $ make install

Content:

  • term_tactics.v: some tactics used in following files

  • foterms.v: definitions and properties of first-order terms (with two kinds of variables)

  • foterms_ext.v: additional properties of first-order terms

  • foterms_std.v: standard first-order terms (with one kind of variables)

  • foformulas.v: definitions and properties of first-order formulas

  • foformulas_ext.v: additional properties of first-order formulas

  • nj1_frl.v: natural deduction for first-order Intuitionistic Logic with universal quantification only (normalization proof)

  • nj1.v: natural deduction for first-order Intuitionistic Logic (normalization proof and sub-formula property)

  • all1.v: sequent calculus for first-order Additive Linear Logic (cut elimination proof)

  • all2.v: sequent calculus for propositional second-order Additive Linear Logic (cut elimination proof)

  • F.v: formulas and natural deduction for propositional second-order Intuitionistic Logic (universal quantification only, i.e. System F)

  • nj2.v: formulas and natural deduction for propositional second-order Intuitionistic Logic

  • hilbert.v: Hilbert system for first-order Intuitionistic Logic with both universal and existential quantifications (standard alpha-equivalence-free presentation)

  • hilbert2nj.v: translation of Hilbert system into natural deduction

  • nj2hilbert.v: translation of natural deduction into Hilbert system

  • nj_vs_hilbert.v: equivalence of the two systems through the previous translations

Variations:

  • *_ar.v: terms with arity checks
  • *_vec.v: terms with vector arguments to control arities

Current examples are developed in Coq, but formalization does not depend on the surrounding meta-theory and should be adaptable to (any?) proof assistant.

(Thanks to Damien Pous for important suggestions and support.)