Sorry I didn't have time to read the proof you shared. I couldn't read it easily and wasn't sure if it completely answered what I really wanted since I want to show that definitions satisfy the precise meaning of eliminability and non-creativity. Maybe the proofs help but I couldn't convert them to something I could actually read like latex or unicode. Sorry, reading that format just hurts my eyes.
https://math.stackexchange.com/questions/1298909/is-criterion-of-eliminability-and-criterion-of-non-creativity-independent There seems to be some steps missing because nothing inside the formal language can alone prove a metalogical fact. It's a meta-theorem like the deduction theorem that seems intuitively trivial still needs some kind of inductive proof. On Wednesday, July 12, 2023 at 12:13:34 AM UTC-4 [email protected] wrote: > "The problem is an alias rule can still fail if the syntax of the > definition doesn't meet certain criteria. [...]" > > Maybe I should've been clearer about the syntax definition. In my theory, > one can skip a lot of parentheses since I considered left first bracketing, > which I explained prior to that definition. Metamath however enforces > formulas of a style with fixed parentheses and would thereby deny any input > where formulas omit or introduce those. > > > Formulas are actually tree structures, for example the theorem of df-bi > has the following syntax tree: > > > > You could put parentheses around formulas in infinitely many correct ways, > while not changing the identity of the formula. That has nothing to do with > intuition, but is well-defined based on bracketing order, as well as > order of order of precedence for operators (but in this case, all binary > operators share the same priority, and it doesn't matter for nullary and > unary operators). > > Parentheses in logic work just the same as in all kinds of mathematical > formulas, they merely prescribe order of operation. Some kind of solvers > (such as Metamath) rule this out for efficiency or ease of implementation, > but that is a technical detail that is rather disruptive and inelegant in > a theoretical context. > > > All the alias replacement rules are well defined, regardless of which > parentheses > were used. If the parentheses change in the way that the identity of the > formula (here: the order of operations) changes, the corresponding rules > simply do not apply anymore. > > > My solution was merely meant to answer your questions on how df-bi can be > justified via a rigorous proof from Metamath's propositional axioms. I have > no better understanding in how Metamath's "definition checker" works than > definitions being treated merely as axioms, as has been confirmed by > multiple people in this thread. > > Additionally, I understand that these definitions are well-justified, > which is also pointed out, for example, in the description of df-bi ( see > https://us.metamath.org/mpeuni/df-bi.html ). > > I have provided you with a proof for that. > > > ------------------------------ > *Von:* [email protected] <[email protected]> im Auftrag von > Marshall Stoner <[email protected]> > *Gesendet:* Mittwoch, 12. Juli 2023 04:35:51 > > *An:* Metamath > *Betreff:* Re: [Metamath] Uncomfortable with definitions as axioms ... > help? > I trust that intuitively that these definitions are valid. The problem is > an alias rule can still fail if the syntax of the definition doesn't meet > certain criteria. If the parenthesis surrounding ↔ were missing in the > definition of the biconditional, for instance. If I could understand how > the definition checker for the set.mm database works I would have a > better understanding. I have my own hypothesis, but I'm not sure if it's > fully sufficient. > > My hypothesis would as follows... > > Let LS⁺ᴰ is the set of all WFFs in the system with new definition D > and LS is the set of all WFFs in the system before adding the new > definition. Then let F ≔ { Ψ ⇒ Φ } be the substitution rule replacing the > definiendum Ψ with the definiens Φ. > > Now the first criteria should be that for any member of LS⁺ᴰ, a member of > LS should result after applying F a finite number of times. > > The second criteria is that if we call the process of applying F a finite > number of times to obtain a member of LS, F*, then F* should be a > function. I.e. the result should be unique. If in any case the result > depends on the order application (ambiguous nesting of the definiendum or > clashing with other symbols), then the definition is going to be creative. > > But are these two criteria alone enough? > On Monday, July 10, 2023 at 12:48:41 PM UTC-4 [email protected] > wrote: > >> I was also disturbed by the issue of definitions being extra axioms >> according to Metamath, and solved it via interpreting only 'not' and >> 'imply' as part of the propositional core language, and all the other >> junctors as different ways to express something in terms of 'not' and >> 'imply' (which is also done in >> https://us.metamath.org/mmsolitaire/pmproofs.txt when proving statements >> which contain different junctors, see "Result of Proof" lines which differ >> from their theorems). >> >> The concept to build only on what is essentially required leads to much >> slimmer definitions that make use of a logical system (e.g. when defining >> semantics). >> >> >> Here is one of my exemplary syntax definitions: >> >> >> Alias step verifications can be done by converting both formulas into the >> core language and checking for equality. >> >> Based on >> >> >> (A1) ⊢\psi\imply(\phi\imply\psi) >> (A2) >> ⊢\psi\imply(\phi\imply\chi)\imply((\psi\imply\phi)\imply(\psi\imply\chi)) >> (A3) ⊢\not\phi\imply\not\psi\imply(\psi\imply\phi) >> (MP) {\psi,\psi\imply\phi}⊢\phi >> >> I gave the below proof of df-bi. Most of it proves that a formula is >> equivalent to itself, from where a single alias step leads to df-bi. >> Since df-bi, under the previous alias definitions, equals ( >> \phi\equiv\psi)\equiv(\phi\equiv\psi). >> >> a2i: >> 1. >> \phi\imply(\psi\imply\chi) >> premise >> 2. >> \phi\imply(\psi\imply\chi)\imply(\phi\imply\psi\imply(\phi\imply\chi)) >> (A2) ; 〈\phi, \psi〉, 〈\psi, \phi〉 >> 3. >> \phi\imply\psi\imply(\phi\imply\chi) >> (MP):1,2 >> >> mms-H6: >> 1. >> \not1\imply\not2\imply(2\imply1) >> >> (A3) ; 〈\phi, 1〉, 〈\psi, 2〉 >> 2. >> \not1\imply\not2\imply(2\imply1)\imply(0\imply(\not1\imply\not2\imply(2\imply1))) >> >> (A1) ; 〈\phi, 0〉, 〈\psi, \not1\imply\not2\imply(2\imply1)〉 >> 3. >> 0\imply(\not1\imply\not2\imply(2\imply1)) >> >> (MP):1,2 >> 4. >> 0\imply(\not1\imply\not2\imply(2\imply1))\imply(0\imply(\not1\imply\not2)\imply(0\imply(2\imply1))) >> >> (A2) ; 〈\chi, 2\imply1〉, 〈\phi, \not1\imply\not2〉, 〈\psi, 0〉 >> 5. >> 0\imply(\not1\imply\not2)\imply(0\imply(2\imply1)) >> >> (MP):3,4 >> >> mms-T13: >> 1. >> \not\not0\imply(1\imply\not\not0) >> >> (A1) ; 〈\phi, 1〉, 〈\psi, \not\not0〉 >> 2. >> \not\not0\imply(\not\not(1\imply\not\not0)\imply\not\not0) >> >> (A1) ; 〈\phi, \not\not(1\imply\not\not0)〉, 〈\psi, \not\not0〉 >> 3. >> \not\not0\imply(\not\not(1\imply\not\not0)\imply\not\not0)\imply(\not\not0\imply(\not0\imply\not(1\imply\not\not0))) >> >> (mms-H6) ; 5 ; 〈0, \not\not0〉, 〈1, \not(1\imply\not\not0)〉, 〈2, \not0〉 >> 4. >> \not\not0\imply(\not0\imply\not(1\imply\not\not0)) >> >> (MP):2,3 >> 5. >> \not\not0\imply(\not0\imply\not(1\imply\not\not0))\imply(\not\not0\imply(1\imply\not\not0\imply0)) >> >> (mms-H6) ; 5 ; 〈0, \not\not0〉, 〈1, 0〉, 〈2, 1\imply\not\not0〉 >> 6. >> \not\not0\imply(1\imply\not\not0\imply0) >> >> (MP):4,5 >> 7. >> \not\not0\imply(1\imply\not\not0\imply0)\imply(\not\not0\imply(1\imply\not\not0)\imply(\not\not0\imply0)) >> >> (A2) ; 〈\chi, 0〉, 〈\phi, 1\imply\not\not0〉, 〈\psi, \not\not0〉 >> 8. >> \not\not0\imply(1\imply\not\not0)\imply(\not\not0\imply0) >> >> (MP):6,7 >> 9. >> \not\not0\imply0 >> >> (MP):1,8 >> >> mpd: >> 1. \phi\imply\psi premise >> 2. \phi\imply(\psi\imply\chi) premise >> 3. \phi\imply\psi\imply(\phi\imply\chi) (a2i):2 ; 3 >> 4. \phi\imply\chi (MP):1,3 >> >> id: >> 1. \phi\imply(\phi\imply\phi) (A1) ; 〈\psi, \phi〉 >> 2. \phi\imply(\phi\imply\phi\imply\phi) (A1) ; 〈\phi, \phi\imply\phi〉, >> 〈\psi, \phi〉 >> 3. \phi\imply\phi (mpd):1,2 ; 4 ; 〈\chi, \phi〉, >> 〈\psi, \phi\imply\phi〉 >> >> mms-T35: >> 1. >> \not\not(0\imply1)\imply(0\imply1) >> >> (mms-T13) ; 9 ; 〈0, 0\imply1〉 >> 2. >> \not\not(0\imply1)\imply(0\imply1)\imply(\not\not(0\imply1)\imply0\imply(\not\not(0\imply1)\imply1)) >> >> (A2) ; 〈\chi, 1〉, 〈\phi, 0〉, 〈\psi, \not\not(0\imply1)〉 >> 3. >> \not\not(0\imply1)\imply0\imply(\not\not(0\imply1)\imply1) >> >> (MP):1,2 >> >> mms-*4.2: >> 1. >> P\implyP >> >> (id) ; 3 ; 〈\phi, P〉 >> 2. >> P\implyP\imply(\not\not(P\implyP\imply\not(P\implyP))\imply(P\implyP)) >> >> (A1) ; 〈\phi, \not\not(P\implyP\imply\not(P\implyP))〉, 〈\psi, P\implyP〉 >> 3. >> \not\not(P\implyP\imply\not(P\implyP))\imply(P\implyP) >> >> (MP):1,2 >> 4. >> \not\not(P\implyP\imply\not(P\implyP))\imply(P\implyP)\imply(\not\not(P\implyP\imply\not(P\implyP))\imply\not(P\implyP)) >> >> (mms-T35) ; 3 ; 〈0, P\implyP〉, 〈1, \not(P\implyP)〉 >> 5. >> \not\not(P\implyP\imply\not(P\implyP))\imply\not(P\implyP) >> >> (MP):3,4 >> 6. >> \not\not(P\implyP\imply\not(P\implyP))\imply\not(P\implyP)\imply(P\implyP\imply\not(P\implyP\imply\not(P\implyP))) >> >> (A3) ; 〈\phi, \not(P\implyP\imply\not(P\implyP))〉, 〈\psi, P\implyP〉 >> 7. >> P\implyP\imply\not(P\implyP\imply\not(P\implyP)) >> >> (MP):5,6 >> 8. >> \not(P\implyP\imply\not(P\implyP)) >> >> (MP):1,7 >> 9. >> P\equivP >> >> alias:8 >> >> df-bi: >> 1. >> \phi\equiv\psi\equiv(\phi\equiv\psi) >> >> >> (mms-*4.2) ; 9 ; 〈P, \phi\equiv\psi〉 >> 2. >> \not(((\phi\equiv\psi)\imply\not((\phi\imply\psi)\imply\not(\psi\imply\phi)))\imply\not(\not((\phi\imply\psi)\imply\not(\psi\imply\phi))\imply(\phi\equiv\psi))) >> >> alias:1 >> >> Here is a way to define these formal proofs: >> >> Reasons and alias steps are technically not even part of a formal proof, >> but they should in practice be provided for clarity. >> Depending on the alias step, one might even prefer several sub-steps >> because it can be a little too much for our sluggish minds to process. >> However, the theory is nice and clean this way, which I think was the >> focus here. >> >> ------------------------------ >> *Von:* [email protected] <[email protected]> im Auftrag >> von Marshall Stoner <[email protected]> >> *Gesendet:* Samstag, 8. Juli 2023 23:40:22 >> *An:* Metamath >> *Betreff:* Re: [Metamath] Uncomfortable with definitions as axioms ... >> help? >> >> New link. >> >> paper <https://1drv.ms/b/s!AuvNPSOQfN3xjK1_IfOJ7LIT5Pl3NQ?e=5Ou22H> >> >> On Saturday, July 8, 2023 at 5:22:17 PM UTC-4 Marshall Stoner wrote: >> >>> I'm currently working on a "textbook-like" introduction to the system >>> used in set.mm. I'm currently thinking about how I should provide a >>> proof justifying the definition of '↔'. >>> >>> I write the abbreviation eq(𝜑, 𝜓) ≔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)). >>> Then the definition is just the expansion of eq((𝜑 ↔ 𝜓), eq(𝜑, 𝜓)). >>> The elimination rule becomes (𝜑 ↔ 𝜓) ≔ eq(𝜑, 𝜓). Applying the >>> elimination rule to the definition you get eq(eq(𝜑, 𝜓), eq(𝜑, 𝜓)) which >>> can be proved as a theorem without any reference to the symbol '↔'. Any >>> theorem containing '↔' must have a proof tree that can be traced backwards >>> to a statement of the definition itself. You replace (𝜑 ↔ 𝜓) with eq(𝜑, >>> 𝜓) in the definition, you have a proved a theorem. You then replace it >>> everywhere else you see it, tracing the same steps forward as you traced >>> backwards. Every line along along the way should still be justified since >>> eq(𝜑, 𝜓) is a WFF that is self-contained. >>> >>> Anyways, I'm still working on the exact wording to make this >>> "meta-argument" absolutely 100% clear to myself and anyone else. Writing >>> out a formal induction meta-proof in the way the standard deduction theorem >>> is typically proved feels a bit cumbersome to me, but I don't want to just >>> handwave anything away either. I feel like I should maybe provide an >>> example showing how the elimination rule would work on a WFF containing >>> nested '↔'. The elimination rule has to be applied recursively until the >>> symbol is gone. >>> >>> paper <https://1drv.ms/b/s!AuvNPSOQfN3xjK1-DmOLCnCMd9hDrQ?e=5expKV> >>> On Wednesday, December 21, 2022 at 7:57:14 PM UTC-5 [email protected] >>> wrote: >>> >>>> On Wed, Dec 21, 2022 at 7:12 PM Samuel Goto <[email protected]> wrote: >>>> >>>>> Hey all, >>>>> >>>>> As I'm looking into metamath there is something lingering that is >>>>> making me uncomfortable: definitions are axioms. >>>>> >>>>> This is obviously intended and by design by the community (the book >>>>> has a whole chapter about it), but I'm still uncomfortable with the >>>>> justifications and consequences. >>>>> >>>> >>>> You are right to be concerned. I was also concerned several years ago, >>>> and the solution I came up with was to observe that definitions in >>>> set.mm follow a very regular structure, such that all definitions with >>>> that structure can be given a metatheoretic argument for conservative >>>> extension. So I added a "definition checker" module to mmj2, which checks >>>> the rules described in the "Additional rules for definitions" section of >>>> https://us.metamath.org/mpeuni/conventions.html . This program is run >>>> as part of the set.mm CI, so we can be sure that (with a small list of >>>> exceptions) every df-* axiom is actually conservative over the ZFC axioms. >>>> >>>> >>>>> A few irrational feelings I think I'm having: >>>>> >>>>> - I can't parse or understand df-bi trivially. What does it mean? >>>>> >>>> >>>> df-bi is one of the exceptions, because the first rule is that a >>>> definition has to have <-> or = as the root symbol and this doesn't work >>>> when we are defining <-> itself. That doesn't mean that the definition is >>>> not conservative, only that it can't be automatically checked. The way to >>>> read df-bi is that it is defining (𝜑 ↔ 𝜓) to be ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → >>>> 𝜑)) (that is dfbi1), except that the root ↔ in the definition is itself >>>> expanded according to this expression. The justification that this is a >>>> conservative extension is that if you replace all instances of (𝜑 ↔ 𝜓) >>>> with ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) in df-bi, you get bijust, which is >>>> provable without df-bi. So you can perform that replacement in any >>>> derivation to eliminate the defined symbol. >>>> >>>> >>>>> - How do I know that the axioms of the definitions aren't >>>>> introducing contradictions? >>>>> >>>> >>>> As I mentioned, we can reduce the problem to a small list of exceptions >>>> like df-bi, plus the definition schema given by the definition checker's >>>> rules. The schema can be proved by a direct substitution argument like the >>>> one I just gave for df-bi, except that to handle bound variables we also >>>> need to have the ability to perform alpha-renaming, such as in _V = { x | >>>> x >>>> = x }, which you can use to prove the theorem { x | x = x } = { y | y = y >>>> }, so we need to know that this was already provable before (this is >>>> vjust). The ability to perform alpha renaming in any formula is a >>>> metatheorem of set.mm's axiom system. >>>> >>>> >>>>> - It seems that definitions aren't supposed to "extend the >>>>> language", but I don't get that sentiment as I read them >>>>> >>>> >>>> I'm not sure I would say that. Definitions definitely are intended to >>>> extend the language, but a conservative extension means that no statements >>>> expressible in the original language become provable as a result of the >>>> introduction of the definition. (In particular, if |- F. was not provable >>>> before, it is still not provable, so the extension is sound.) >>>> >>>> >>>>> - We say "all you need is propositional and first order logic and >>>>> set theory axioms" but then proceed to introduce a bunch by definitions >>>>> >>>> >>>> Yes, I tend to agree with this sentiment. It's not *really* true that >>>> you don't need definitions. You don't need them *in principle*, but if you >>>> don't like exponentially long proofs (which can make a qualitative >>>> difference if you have ultrafinitist tendencies and don't trust proofs >>>> that >>>> cannot be checked on any computer present or future) then you are more or >>>> less forced to accept them. >>>> >>>> >>>>> I'm sure this can't be a new sentiment, since an entire chapter in >>>>> the book was dedicated to it, but I was wondering if: >>>>> >>>>> (a) Does anyone have some explanation posted online that I could >>>>> read to inform myself and perhaps settle my anxiety? >>>>> (b) Is there a version of metamath and/or set.mm that don't rely >>>>> on definitions as axioms? >>>>> >>>> >>>> For the reasons I stated above, a set.mm without definitions would not >>>> be remotely usable. And metamath doesn't really support definitions in any >>>> other way. >>>> >>>> Even with the definition checker, the situation was still somewhat >>>> problematic to me, since the definition checker is now essentially a part >>>> of the "trusted code base" of metamath (unless you want to personally >>>> review all of those thousand definitions-as-axioms in set.mm) and yet >>>> it is not a required part of metamath verifier operation, and it has only >>>> one implementation, which moreover is tailored to set.mm notions. So I >>>> tried to make a version of metamath that includes definitions as part of >>>> the kernel, and the result is Metamath Zero ( >>>> https://github.com/digama0/mm0). It unfortunately complicates several >>>> things to take definitions as primitive because you need to have a notion >>>> of bound variable to handle examples like df-v, as well as a conversion >>>> judgment to handle definition unfolding without having to also bake in an >>>> equality operator (since not all metamath databases have one, or only have >>>> one for some sorts and not others). You can read about MM0 in >>>> https://arxiv.org/abs/1910.10703 . >>>> >>>> Another Metamath variant which adds definitions as a primitive part of >>>> the language is GHilbert by Raph Levien, although this diverges a bit more >>>> from metamath and is closer to lambda calculus / LF in terms of its >>>> primitive operators. >>>> >>> -- >> 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/a3d5056d-9e16-4678-af16-1a91431bbffcn%40googlegroups.com >> >> <https://groups.google.com/d/msgid/metamath/a3d5056d-9e16-4678-af16-1a91431bbffcn%40googlegroups.com?utm_medium=email&utm_source=footer> >> . >> > -- > 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/583ce4fe-d4de-46a5-9a61-1922d45ecfden%40googlegroups.com > > <https://groups.google.com/d/msgid/metamath/583ce4fe-d4de-46a5-9a61-1922d45ecfden%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/b3c24569-83ef-4b88-89a5-77e4f1a12bb0n%40googlegroups.com.
