[FOM] Voevodsky and inconsistent systems

[Franklin]

Dear FOM-ers,

 I would like to hear comments about the project presented in
Voevodsky's talk http://video.ias.edu/voevodsky-80th
(as opposed to the way he chose to motivate it)
The talk intended to present the possibility of using inconsistent
systems to obtain correct theorems.
There is an ongoing discussion about the consistency of PA, which he
used to motivate the need for such a program.
Instead I would like to see how is the program itself seen in the
professional community of FOM.
I do not work in foundational mathematics but nevertheless I am
inclined to learn and be aware of its development.

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
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