Am Sonntag, 8. März 2020 14:06:25 UTC+1 schrieb Mario Carneiro: > > It's not a conservative extension, as the intuitionistic logic development > makes clear. Peirce's law ((p -> q) -> p) -> p is not provable from > ax-1,2,mp >
There is some connection to theoretical computer science here, in particular grammars. I (faintly) remember, that the richness of constructable strings, and decidability (is a particular string contructable) are prominent questions in this part. It is way long back, that I dealt with questions like this. I still try to translate your words to what I remember from courses then: conservative seems to mean fully decidable... but it is provable from ax-1,2,3,mp, even though there are no negations > involved in the statement. By contrast, df-bi is a conservative extension > even though it has a peculiar form. This is easy to prove because you can > replace (p <-> q) with -. ((p -> q) -> -. (q -> p)) everywhere in a proof > using biconditionals to reduce it to a proof which refers to the theorem > bijust instead of df-bi, in the original axiom system. > > Thanks for your answer. Wolf -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/3279023c-fbfd-4dc9-b6ea-b0fada02d4ed%40googlegroups.com.
