3 ms·

I believe there are a couple of different claims being made in the above, I went ahead and just made a gist with some proofs (in lean) that try and hit some of

• danbruc 8y ago
  Thanks for the effort but unfortunately for me the page just says running and nothing ever happens, especially no output at all. Not even for the small example included by default. But besides that I did not really want to make any claims and certainly nothing that could be easily addressed by a proof, I think. My point was more that one has to take care that the type of logic one uses has to fit together with the domain one wants to reason about with that logic. If in the domain you want to reason about the law of excluded middle does not hold or only does so in a non-straight forward way, then using a logic with law of excluded middle will at least be not as easy as it could be or even painful or in the worst case lead to wrong conclusions.
  • ratmice 8y ago
    personally, I will generally just want to construct some artifact which has some property, e.g. the proof is a program to construct something. Where a classical proof doesn't give you this program, it merely states that such a property holds. Which is perfectly fine if that is what you want to know.