search

elexunix / qock

This project is currently an implementation of a proof-checker. But it is planned to be extended; for example, to support algorithm extraction from intuitionistic proofs, which is considered to be an interesting feature.
0 stars 0 forks source link

[Major goal] Intuitionistic proofs to algorithms effectively #2

Open elexunix opened 3 years ago

elexunix commented 3 years ago

It is possible to translate some intuitionistic proofs into algorithms I don't know neither a formalization, nor a proof sketch, but some projects like Coq have it implemented

My first idea of how this conception might sound (probably it is wrong, but.. well, it is just the first trial) as follows: If a Pi_2 statement (forall n exists m ...) is proven in PA without using the law of excluded middle, then probably the proof can be translated into an algorithm that for that n given m. Maybe this can be done somehow inductively, contructing a Pi2-formula -> algorithm translation using algorithms for subformulas, but I don't know; obviously, it needs to be investigated first by talking to people who know something about the result. Seems like I know somebody

elexunix commented 3 years ago

Seems like I have finally found a proof-theoretic article which explains it all, together with the axioms and rules of inference specific for intuitionism! Check out this one: https://arxiv.org/pdf/2003.01935.pdf