IRC channel logs

<fltrz>anyone familiar with metamath?

<fltrz>I understand the verifier itself, but not the exact formalization in set.mm

<fltrz>I'm working on a proof (using mmj2), and got quite far, but I keep getting stumped on an embarrasingly fundamental step: proving a positive integer is a natural number

<fltrz>basically how do I prove |- ( ( A e. ZZ /\ 1 <_ A ) -> A e. NN ) ?

<fltrz>I'm wondering if I'm really supposed to drill down below the ZZ>= constructs?

<fltrz>oh I see, I'm supposed to use eluz2

<aggi>fltrz: an axiomatic statement cannot be "proven"; you may place any amount of apples on your desk, count them, and consider it _evident_

<aggi>anyway, wrong channel

<river>i don't quite agree, you can prove an axiom by invoking the axiom

<stikonas[m]>Then it's not am axiom but theorem in your logical system

<nektro>river's got it

<stikonas>oh, if you mean the same axiom, not some other axiom...

IRC channel logs

2023-04-19.log