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

Maybe propositional axioms might better be updated to check well-formation? #5

Open elexunix opened 3 years ago

elexunix commented 3 years ago

It would be better for the axioms from namespace propositional (hypothesis_addition, conditional_modus_ponens, ...) to check whether their arguments are well-formed, wouldn't it?

For example, do we permit substituting variable<conjunction<a, b>> and b into the axiom x -> y -> x? Or it is better to generate an illformed type or compile-error at this moment?

elexunix commented 3 years ago

Yes, of course, they are tautologies

elexunix commented 3 years ago

But it prevents proving&testing propositional lemmas... As random structs are no longer considered to be suitable for substitution. Seems like one would always have to construct silly wffs and use them to check lemmas of this kind. Maybe there is a better solution?