mm0 semantic equivalence

[Olof]

Hello! if I sound pretentious, it's because I let chat gpt rewrite my question in better English :). Anyways:

Hello! I've recently stumbled upon formal mathematics due to its potential application in interactive education. Despite delving into the source code of mm0 and scanning through available documentation, I find it challenging to fully grasp certain concepts.

I'm curious about how mm0 handles the normalization/canonicalization of expressions, if it addresses this at all. My interest stems from its potential use beyond proof generation, particularly in interactive scenarios where users may answer questions. Instead of requiring users to generate entire proofs to demonstrate their abilities, the idea is to allow users to generate expressions appearing in the proof. The backend then determines whether that is sufficient to conclude that the user has proven the provable, thereby eliminating the need to learn the advanced syntax of proof generation software. The concept involves representing questions as provable theorems within mm0 using eroteric logic.

For example, a simple "or" question could be answered by "proving" (providing selected expressions to) a theorem:
-- Or Inquiry
provable sort ef; -- question
term askOr: wff > wff > ef;
axiom inferOrAnswer1 (a b: wff): $ a $ > $ askOr a b $;
axiom inferOrAnswer2 (a b: wff): $ a $ > $ askOr b a $;
theorem isExample (h: $ a -> b -> c $): $ askOr (~((a -> b) -> (a -> c))) ((a -> b) -> (a -> c)) $ = '(inferOrAnswer2 (a2i h));
Some questions only require providing an expression to conclude that the end user has likely proven a provable, such as questions about solutions to equations. Tackling this is obviously challenging. How would one approach it, and does mm0/metamath already implement tools that could be useful to compare input expressions for "semantic equivalence"?

[Mario Carneiro]

MM0 does not itself do any normalization of expressions. Instead, it acts as a verification tool for already completed proofs, although it has some facilities for constructing proofs and it is extensible enough to let you add more automation to it, which you could use to automate normalization tasks. But most likely for some really advanced proof work you would want to use a custom front end language or user interface, and MM0 would come out the back as a way to generate portable and cross-checkable proofs. The facilities of MM0 are mostly designed for ensuring that large and complex systems produce trustworthy results, but it is far outshined by other tools when it comes to aspects of human-computer interaction.

As far as your example is concerned, I think that is a reasonable way to pose a "prove or disprove" question to a high automation system or AI, because the only way to construct a proof of isExample is by proving or disproving the claim.

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/8fdc51fa-a68b-44af-9c6c-6a7aa68cada5n%40googlegroups.com.

[Olof]

Alright, great. Moving on, would you consider the following general case of posing a question valid, or do you identify any issues with it? It's evident that the respondent needs to be familiar with the axioms and terms, but that holds true for natural language questions as well, I believe.
The extra sorts might be unnecessary, but good for clarity.
provable sort e;
provable sort ef;
term validDomainAnswer: wff > e;
term askForDomainAnswer: wff > ef;
axiom inferDomainAnswer (a b: wff): $ a $ > $ validDomainAnswer b  $ > $ askForDomainAnswer a $; -- a question is provable once a valid answer for it is provable,
axiom inferExpressionIsDomainAnswer (a b: wff): $ a $ > $ randomExpressionX $ > $ validDomainAnswer b $; -- randomExpressionX probably contains a and b... dunno...
theorem askDomainQuestion (h: $ a $): $ askForDomainAnswer a $ = '(inferDomainAnswer (inferExpressionIsDomainAnswer (manipulateToRandomExpressionX a randomHyps) a) a ); Essentially: Given a what is the askForDomainAnswer answer?

Regarding the normalization of expressions, especially mathematical expressions (QExpr) resembling human input, is it reasonable to apply transformation rules based on previously proven theorems? For instance, whenever a term that is proven to be commutative is encountered, it could be transformed into alphabetical order or a similar arrangement based on those proven theorems. In other words a separate language would state the rules of application of different theorems during the normalization process of different term expressions. This would allow the easy definition of semantic equivalence for various use cases and keep the normalization process connected to the formalization itself. I'm new to this so normalization might be more complex than that but anyways. Is this a valid thought? Is it already implemented somewhere?