[FOM] Voevodsky and inconsistent systems

[Jeffrey Sarnat]

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
>