On Mon, Nov 4, 2019 at 6:02 PM Giovanni Mascellani <[email protected]> wrote:
> Hi Mario, > > Il 04/11/19 21:49, Mario Carneiro ha scritto: > > Maybe you could bring me up to speed on the details here, but as I see > > it, implication introduction is 'ex'. It is important for this that > > conjuncts be stored as a *left* associated list, possibly beginning with > > a T. if that makes things easier. Whenever you change the context, there > > is a cost associated with pulling any lemmas into the new context > > (including hypotheses) via adantr; you can either compute these lazily > > or precompute them and drop any that you don't end up needing. > > Hmm, there are different problems converging here and I am not sure we > are considering the same. Let me state more generally what I want to do. > I want to take an arbitrary ND proof (more specifically, ND proofs as > defined by GAPT[1], generated by GAPT itself munching resolutions found > by Prover9 or similar tools; however, I assume that the proof was > generated by a black box) and generate a Metamath proof of the same > statement. > > [1] https://www.logic.at/gapt/api/gapt/proofs/nd/NDProof.html > > Before even starting converting the proof, I need to decide how to > convert statements, i.e., to what to map a ND sequent in Metamath. My > current choice is to map, say, "ph, ps, ch |- th" to the Metamath statement > > |- ( ( ph /\ ( ps /\ ( ch /\ T. ) ) ) -> th ) > > I call this a "reified" ND inference, because the ND turnstile is mapped > to an element of the language, i.e., the implication. I don't know if > the word "reified" is logically/philosophically correct, I will be happy > to use a better one if anybody suggests it. > > Using your style, I would choose a global context, say et, and map the > same sequent to > > |- ( et -> ph ) > & |- ( et -> ps ) > & |- ( et -> ch ) > => |- ( et -> th ) > > Here the ND inference is not reified, because it is mapped to the "=>" > symbol which is not an element of the formal language. > Aha, I see the confusion now. The style you present above is deduction style as it is understood across theorems. That is, when we have a theorem A , B |- C we split up the context on separate hypotheses and stick a new context variable on the left, as you've done. But inside a theorem this is not possible, as you've observed, so a slight variant of the strategy is used. In an ND proof where all hypotheses have been transformed as such to ( ph -> A ) & |- ( ph -> B ) => ( ph -> C ), all steps in the proof will contain Gamma, plus additional local assumptions, for example A, B, D, E |- F, and this is concretely translated to |- ( ( ( ph /\ D ) /\ E ) -> F ). At a slightly higher level, we can still find the distributed context view of the statement, where we hold some context Delta fixed (in this case it is ( ( ph /\ D ) /\ E ) but in general it can be an extension of this), and then the step A, B, D, E |- F is identified (in context Delta) as the proof step |- ( Delta -> F ), where the four hypotheses are stored names of proof steps that prove |- ( Delta -> A ) , |- ( Delta -> B ) (by adantr from the original theorem hypotheses), and |- ( Delta -> D ) , |- ( Delta -> E ) (proven by simplr and simpr). So although we can't generalize over statements like |- ( et -> ph ) & |- ( et -> ps ) & |- ( et -> ch ) => |- ( et -> th ) in the middle of a proof, we can still identify the relevant substitution instance of this pattern as a part of the proof. The concrete encoding |- ( ( ( ph /\ D ) /\ E ) -> F ) is simply one way to make sure that A, B, D, E are all provable from the context; as you say right associating would work just as well, although metamath has a large number of theorems dealing with the left associated case (simpr, simplr, simpllr, simp-4r ... simp11r selects hypotheses, and adantr, ad2antrr, ad3antrrr, ad4antr, ... ad10antr weakens a context), exactly for making this kind of reasoning efficient. For extremely large contexts, this approach is quadratic where log-linear is possible, so you would probably want to do something else in that case, but this isn't really a problem in set.mm because the number of variables is already capped. > If I used your style, I would have had to use something like: > > ( |- ( et -> ph ) & |- ( et -> Gamma ) => |- ( et -> ps ) ) > => ( |- ( et -> Gamma ) => |- ( et -> ( ph -> ps ) ) ) > > but this is clearly not expressible in Metamath, because "&" and "=>" > are not reified. > It's actually A. et' ( |- ( et' -> ph ) & |- ( et' -> Gamma_1 ) & ... & |- ( et' -> Gamma_n ) => |- ( et' -> ps ) ) => ( |- ( et -> Gamma_1 ) & ... & |- ( et -> Gamma_n ) => |- ( et -> ( ph -> ps ) ) ) making the quantifier over contexts et' explicit. But the big observation is that we only care about one substitution instance of this (depending on the context where the step applies); in this case a reasonable choice of context is ( et /\ ph ), in which case you get ( |- ( ( et /\ ph ) -> ph ) & |- ( ( et /\ ph ) -> Gamma_1 ) & ... & |- ( ( et /\ ph ) -> Gamma_n ) => |- ( ( et /\ ph ) -> ps ) ) => ( |- ( et -> Gamma_1 ) & ... & |- ( et -> Gamma_n ) => |- ( et -> ( ph -> ps ) ) ) And now we eliminate the higher order arrow by observing that all the assumptions to the hypothesis are provable outright: simpr: |- ( ( et /\ ph ) -> ph ) adantr: |- ( et -> Gamma_1 ) => |- ( ( et /\ ph ) -> Gamma_1 ) ... adantr: |- ( et -> Gamma_n ) => |- ( ( et /\ ph ) -> Gamma_n ) and the conclusion is provable from the consequent of the hypothesis: ex: |- ( ( et /\ ph ) -> ps ) => |- ( et -> ( ph -> ps ) ) ) So the higher order inference decomposes into a set of theorem applications to *both* the conclusion (working backwards) and the hypotheses/subproofs (working forwards). On top of that, taken for granted that I will be using the "reified" > style, there is some freedom to decide whether to use a left or right > associated list, or a generic tree. Left vs right is not a big deal, I'd > say, in the worst case one has to prepare an additional layer of lemmata > to adjust things. Since I already use quite some technical lemmata[2] > for building these proofs, it doesn't change much. I discussed in my > previous email the alternative between a fixed list and a tree, but this > difference is in term of efficiency, while the reified vs non-reified ND > style is a more fundamental difference. > My point is that "ND style" incorporates *both* the reified and non-reified aspects. You can't prove theorems using only the non-reified approach, the context changing is an integral part of it. You probably are already aware of all this, but you might find my original talk on the ND style helpful: http://us.metamath.org/ocat/natded.pdf . > > While this is an option, I think it would be much simpler in a set.mm > > <http://set.mm> based system to use x R y for representing binary > > relations without additional variables getting in the way. > > Nice insight, but this works only for at most binary relations (and > relatedly functors). I would like to not lose generality with respect to > the possibility of translating whatever ND proof to Metamath, as is > currently the case. > Assuming you have a pairing operator, you can represent an n-ary operation via ( F ` <. x , <. y , <. z , ... >. >. >. ) and an n-ary relation via <. x , <. y , <. z , ... >. >. >. e. R. The cases n = 1, 2, 3 have special support in set.mm (n = 3 an "ordered triple"), and for medium size tuples you can use the <" A B C ... D "> sequence (df-s1, df-s2, ..., df-s8), using the "concat" function to get more than 8 arguments. (These operators are intended for representing large sequences and trees as metamath terms with log-overhead.) Mario -- 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/CAFXXJSvpmMEwp_HA_P_m%2BZU%3D82kPRFaKWSoY6V7sjn6a0Vw8Mw%40mail.gmail.com.
