Prove theorems without ax-8

metamath / set.mm

Metamath source file for logic and set theory

Other

254 stars 88 forks source link

Prove theorems without ax-8 #4172

Closed GinoGiotto closed 2 months ago

GinoGiotto commented 2 months ago

Edit a few proofs to reduce axiom usage, specifically:

Edit abv -> avoid ax-8
Edit rru -> avoid ax-10, ax-11, ax-12
Edit ab0 -> avoid ax-8
Edit ab0orv -> avoid ax-10, ax-11, ax-12 (ax-8 automatically avoided by previous edits)
Edit abn0 -> avoid ax-8

All added DV conditions are with dummy variables.

Axiom usage here: https://github.com/metamath/set.mm/commit/781a0bb89850b0271ab3b6d5288a598a6f318f57

benjub commented 2 months ago

A shortening:

    abv $p |- ( { x | ph } = _V <-> A. x ph ) $=
      ( vy cab wtru wceq wsb wal cvv cv wcel wb dfcleq vextru tbt df-clab albii
      bitr3i bitri weq df-v equid bitru abbii eqtri eqeq2i nfv sb8v 3bitr4i ) A
      BDZEBDZFZABCGZCHZUJIFABHULCJZUJKZUOUKKZLZCHUNCUJUKMURUMCURUPUMUQUPBCNOACB
      PRQSIUKUJIBBTZBDUKBUAUSEBUSBUBUCUDUEUFABCACUGUHUI $.

and this is one more reason to use https://us.metamath.org/mpeuni/bj-df-v.html as the definition (and this theorem does not require ax-8 nor df-clel either).

GinoGiotto commented 2 months ago

and this is one more reason to use us.metamath.org/mpeuni/bj-df-v.html

I definitely agree, I often use T. for tautologies and it generally makes proofs simpler. I would also argue to use us.metamath.org/mpeuni/bj-df-nul.html for the same reason.