# [FOM] Voevodsky and inconsistent systems

Jeffrey Sarnat jeffrey.sarnat at gmail.com
Wed May 18 18:08:29 EDT 2011

```On Wed, 18 May 2011, Franklin wrote:

> Dear FOM-ers,
>
> Specifically I would like to know:
> [...]
> 1) If there are already actual examples of its use, i.e. if there are
> already examples in which a non-necessarily consistent system is used
> to derive correct theorems (with algorithms to detect them)? I mean

Yes. Coq implements a version of the Calculus of Inductive Constructions
(CIC) in which inductive (and co-inductive) functions are written with a
general recursion operator that can, in principle, be used to implement
well-typed, non-terminating proofs of false-statements. However, in order
for Coq to accept a particular well-typed CIC term as a proof, every
recursive function must also satisfy a separate syntactic criterion---the
so-called "guard condition"---that (hopefully) ensures every
inductive/co-inductive function is terminating/productive. The guard
condition is external to CIC's type system (or proof rules, depending on
which side of the Curry-Howard coin you prefer to look at) meaning that
it's fair to characterize CIC's type system as an "inconsistent system"
and the guard condition checker as an algorithm that detects correct
theorems.

Jeff

> useful, serious examples, in which the application is somehow needed.
> Non-useful examples should be easy to present: Take a consistent
> system, like propositional logic. Add the axiom schema: Any formula of
> length 20 implies A /\~A.
> (It could also be one axiom: A particular tautology with 20 symbols
> implies A /\~A).
> This other system will be inconsistent but any theorem with proofs not
> involving formulas of length greater than 20 should be correct. Then
> there is an algorithmic way of detecting correct theorems in this
> inconsistent system.
>
> 2) Some thoughts about the connotation of the development of such a program.
>
> Thank you.
> Best regards,
> ___
> Franklin Vera Pacheco (Frank cheValier on a Pc)
> PhD Student, University of Toronto
> http://www.franklinvp.com
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
```