Searching set.mm by formula (up to α-equivalence)

[Jasper Nice]

Dear Metamath community,

My hope is that this question is not too off-topic.

I am an amateur logician who is frequently running into new theorems which seem to have the consistent property that obstruct me from some time from making progress.

I am also completely new to Metamath, and have only heard of it at this point. I put a sincere effort in, in an attempt to figure out how to search for a specific theorem of predicate calculus. However, I have been unable to navigate something like set.mm in a way that lets me find the theorems I'm looking for quickly.

Ideally, I would like to be able to search for a formula, and have returned to me any which are alpha equivalent to it. Alternatively, if this is a bad approach, please advise me of how I can find the theorems I am looking for.

E.g., such a theorem might be of the form 

    (((∀x)(B → C)) → (((∃x)B) → ((∃x)C)))

where everything is composed from primitive connectives To, Not and For.

Thank you very much for your attention to this matter,

Jasper

[Igor Ieskov]

Hi Jasper,

One of possible ways to find a particular theorem is to use pattern search in the Metamath-lamp proof assistant.

To find a theorem in set.mm:
1. Open mm-lamp proof assistant in your browser. Use either the latest version (usually the most stable) or the dev version (sometimes it has new features not available in other versions).
2. In “Source type” select “Web”, in “Alias” select set.mm:latest. Confirm downloading the set.mm file from the Metamath site and wait while the file is downloaded. Click the “Apply changes” button.
3. Open an Explorer tab.
4. In the "pattern" text field enter a search pattern and press enter.

For example, for the formula

(((∀x)(B → C)) → (((∃x)B) → ((∃x)C)))

the search pattern could be
A. x ph -> ps -> E. x ph -> E. x ps

This pattern will find the theorem exim |- ( A. x ( ph -> ps ) -> ( E. x ph -> E. x ps ) )

-

Igor

[Jasper Nice]

Dear Igor,

Thank you for for attention to this, and for teaching me how to achieve my goal.

I did try to search for that particular theorem as an example, and the search goes to 60% very quickly, and then stalls for a very long time. In fact, I have not been able to get it to terminate yet.

Is this something that is likely the result of user-error on my behalf?

Thank you again for your help; being able to navigate the database will be extremely helpful in what I'm trying to do.

Jasper

[Igor Ieskov]

Unfortunately the search algorithm is not optimized enough and such stalling happens for some patterns. But usually it happens when a pattern contains parenthesis. The pattern from my previous message works well for me, though I notice some small pause less than a second on exactly 60% too.

When this happens, you have a few options:

1. Rewrite the pattern (in many cases it is enough to remove some parenthesis only). This may, however, require some knowledge of set.mm syntax. For the example pattern, I rewrote it as

$[+ A. x $] $* ph -> ps -> $* $[+ E. x ph $] $* -> $* $[+ E. x ps $]

and it still produces useful results. Check whether it is not stalling for you.

2. Eliminate the assertion which causes the search to stall from the proof assistant context by using “Stop before” instead of “Read all” when loading set.mm database. If the pattern stalls at 60%, this means there is some assertion at around index 30408 (this is 60% of the overall number of assertions in set.mm) which makes the search engine stall. Let’s take some smaller index, say 30000. Using the explorer tab, we can find that the assertion with this index is upgrwlkedg. So you can “stop before” upgrwlkedg and check if the search works well. This of course will hide everything after upgrwlkedg. But if you need some basic theorems, that might be sufficient for you, since many basic theorems are located near the beginning of set.mm.

Igor