Skip to content

Commit

Permalink
rm ax-10 from a couple of sbied* variants (#3802)
Browse files Browse the repository at this point in the history 
* rm ax-10 from a couple of sbied* variants

* discouraged

* typo

* reduce axiom usage for sbiedvw

* review issues

* review issue
  • Loading branch information
@wlammen
wlammen authored Jan 29, 2024
1 parent b9d47a8 commit b6dd646
Show file tree
Hide file tree
Showing 2 changed files with 73 additions and 28 deletions.
2 changes: 2 additions & 0 deletions discouraged
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17306,6 +17306,7 @@ New usage of "sbi2ALT" is discouraged (1 uses).
New usage of "sbi2vOLD" is discouraged (0 uses).
New usage of "sbieALT" is discouraged (1 uses).
New usage of "sbiedALT" is discouraged (1 uses).
New usage of "sbiedwOLD" is discouraged (0 uses).
New usage of "sbievOLD" is discouraged (0 uses).
New usage of "sbimALT" is discouraged (3 uses).
New usage of "sbimdOLD" is discouraged (0 uses).
Expand Down Expand Up @@ -19248,6 +19249,7 @@ Proof modification of "sbi2ALT" is discouraged (55 steps).
Proof modification of "sbi2vOLD" is discouraged (44 steps).
Proof modification of "sbieALT" is discouraged (73 steps).
Proof modification of "sbiedALT" is discouraged (60 steps).
Proof modification of "sbiedwOLD" is discouraged (51 steps).
Proof modification of "sbievOLD" is discouraged (41 steps).
Proof modification of "sbimALT" is discouraged (27 steps).
Proof modification of "sbimdOLD" is discouraged (62 steps).
Expand Down
99 changes: 71 additions & 28 deletions set.mm
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17490,15 +17490,56 @@ disjoint variable condition ( ~ sb2 ). Theorem ~ sb6f replaces the
( ) B $.
$}

${
$d x y $.
sbrimvlem.1 $e |- ( A. x ( ph -> ( x = y -> ps ) )
<-> ( ph -> A. x ( x = y -> ps ) ) ) $.
$( Common proof template for ~ sbrimvw and ~ sbrimv . The hypothesis is an
instance of ~ 19.21 . (Contributed by Wolf Lammen, 29-Jan-2024.) $)
sbrimvlem $p |- ( [ y / x ] ( ph -> ps ) <-> ( ph -> [ y / x ] ps ) ) $=
( wi wsb weq wal sb6 bi2.04 albii 3bitr2i imbi2i bitr4i ) ABFZCDGZACDHZBF
ZCIZFZABCDGZFQRPFZCIASFZCIUAPCDJUDUCCARBKLEMUBTABCDJNO $.
$}

${
$d x y $. $d x ph $.
$( Substitution in an implication with a variable not free in the
antecedent affects only the consequent. Version of ~ sbrim and sbrimv
based on fewer axioms, but with more disjoint variable conditions.
Based on an idea of Gino Giotto. (Contributed by Wolf Lammen,
29-Jan-2024.) $)
sbrimvw $p |- ( [ y / x ] ( ph -> ps ) <-> ( ph -> [ y / x ] ps ) ) $=
( weq wi 19.21v sbrimvlem ) ABCDACDEBFCGH $.
$}

${
$d x y $. $d x ps $.
sbievw.is $e |- ( x = y -> ( ph <-> ps ) ) $.
$( Version of ~ sbiev with an extra DV condition, not requiring ~ ax-12 .
(Contributed by BJ, 18-Jul-2023.) $)
$( Version of ~ sbie and ~ sbiev with more disjoint variable conditions,
requiring fewer axioms. (Contributed by BJ, 18-Jul-2023.) $)
sbievw $p |- ( [ y / x ] ph <-> ps ) $=
( wsb weq wi wal sb6 equsalvw bitri ) ACDFCDGAHCIBACDJABCDEKL $.
$}

${
$d x ph $. $d x ch $. $d x y $.
sbiedvw.1 $e |- ( ( ph /\ x = y ) -> ( ps <-> ch ) ) $.
$( Version of ~ sbied and ~ sbiedv with more disjoint variable conditions,
requiring fewer axioms. (Contributed by Gino Giotto, 29-Jan-2024.) $)
sbiedvw $p |- ( ph -> ( [ y / x ] ps <-> ch ) ) $=
( wsb wi sbrimvw weq wb expcom pm5.74d sbievw bitr3i pm5.74ri ) ABDEGZCAQ
HABHZDEGACHZABDEIRSDEDEJZABCATBCKFLMNOP $.
$}

${
$d x y ps $. $d t y $. $d t x $. $d u y $.
2sbievw.1 $e |- ( ( x = t /\ y = u ) -> ( ph <-> ps ) ) $.
$( Version of ~ 2sbiev with more disjoint variable conditions, requiring
fewer axioms. (Contributed by Gino Giotto, 10-Jan-2024.) $)
2sbievw $p |- ( [ t / x ] [ u / y ] ph <-> ps ) $=
( wsb weq sbiedvw sbievw ) ADEHBCFCFIABDEGJK $.
$}

${
$d y z $.
$( Version of ~ sbcom3 with a disjoint variable condition using fewer
Expand Down Expand Up @@ -19658,10 +19699,19 @@ Converse of the inference rule of (universal) generalization ~ ax-gen .
${
sbrim.1 $e |- F/ x ph $.
$( Substitution in an implication with a variable not free in the
antecedent affects only the consequent. (Contributed by NM,
antecedent affects only the consequent. See ~ sbrimv for a version with
disjoint variables not requiring ~ ax-10 . (Contributed by NM,
2-Jun-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) $)
sbrim $p |- ( [ y / x ] ( ph -> ps ) <-> ( ph -> [ y / x ] ps ) ) $=
( wi wsb sbim sbf imbi1i bitri ) ABFCDGACDGZBCDGZFAMFABCDHLAMACDEIJK $.

$d x y $.
$( Substitution in an implication with a variable not free in the
antecedent affects only the consequent. Version of ~ sbrim not
depending on ~ ax-10 , but with disjoint variables. (Contributed by
Wolf Lammen, 28-Jan-2024.) $)
sbrimv $p |- ( [ y / x ] ( ph -> ps ) <-> ( ph -> [ y / x ] ps ) ) $=
( weq wi 19.21 sbrimvlem ) ABCDACDFBGCEHI $.
$}

${
Expand Down Expand Up @@ -19821,31 +19871,21 @@ Converse of the inference rule of (universal) generalization ~ ax-gen .
sbiedw.1 $e |- F/ x ph $.
sbiedw.2 $e |- ( ph -> F/ x ch ) $.
sbiedw.3 $e |- ( ph -> ( x = y -> ( ps <-> ch ) ) ) $.
$( Version of ~ sbied with a disjoint variable condition, which does not
require ~ ax-13 . (Contributed by Gino Giotto, 10-Jan-2024.) $)
$( Version of ~ sbied with a disjoint variable condition, requiring fewer
axioms. (Contributed by Gino Giotto, 10-Jan-2024.) Avoid ~ ax-10 .
(Revised by Wolf Lammen, 28-Jan-2024.) $)
sbiedw $p |- ( ph -> ( [ y / x ] ps <-> ch ) ) $=
( wsb wi sbrimv nfim1 weq wb com12 pm5.74d sbiev bitr3i pm5.74ri ) ABDEIZ
CATJABJZDEIACJZABDEFKUAUBDEACDFGLDEMZABCAUCBCNHOPQRS $.

$( Obsolete version of ~ sbiedw as of 28-Jan-2024. (Contributed by Gino
Giotto, 10-Jan-2024.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
sbiedwOLD $p |- ( ph -> ( [ y / x ] ps <-> ch ) ) $=
( wsb wi sbrim nfim1 weq wb com12 pm5.74d sbiev bitr3i pm5.74ri ) ABDEIZC
ATJABJZDEIACJZABDEFKUAUBDEACDFGLDEMZABCAUCBCNHOPQRS $.
$}

${
$d x ph $. $d x ch $. $d x y $.
sbiedvw.1 $e |- ( ( ph /\ x = y ) -> ( ps <-> ch ) ) $.
$( Version of ~ sbiedv with a disjoint variable condition, which does not
require ~ ax-13 . (Contributed by Gino Giotto, 10-Jan-2024.) $)
sbiedvw $p |- ( ph -> ( [ y / x ] ps <-> ch ) ) $=
( nfv nfvd weq wb ex sbiedw ) ABCDEADGACDHADEIBCJFKL $.
$}

${
$d x y ps $. $d t y $. $d t x $. $d u y $.
2sbievw.1 $e |- ( ( x = t /\ y = u ) -> ( ph <-> ps ) ) $.
$( Version of ~ 2sbiev with a disjoint variable condition, which does not
require ~ ax-13 . (Contributed by Gino Giotto, 10-Jan-2024.) $)
2sbievw $p |- ( [ t / x ] [ u / y ] ph <-> ps ) $=
( wsb weq sbiedvw sbievw ) ADEHBCFCFIABDEGJK $.
$}

${
$d x z $. $d y z $.
$( Obsolete version of ~ sbequi as of 7-Jul-2023. Version of ~ sbequi with
Expand Down Expand Up @@ -21994,9 +22034,10 @@ proposition with a distinct variable (closed form of ~ nfsb4 ).
sbied.2 $e |- ( ph -> F/ x ch ) $.
sbied.3 $e |- ( ph -> ( x = y -> ( ps <-> ch ) ) ) $.
$( Conversion of implicit substitution to explicit substitution (deduction
version of ~ sbie ). (Contributed by NM, 30-Jun-1994.) (Revised by
Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen,
24-Jun-2018.) $)
version of ~ sbie ) See ~ sbiedv , ~ sbiedw , ~ sbiedvw for variants
using disjoint variables, but require fewer axioms. (Contributed by NM,
30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof
shortened by Wolf Lammen, 24-Jun-2018.) $)
sbied $p |- ( ph -> ( [ y / x ] ps <-> ch ) ) $=
( wsb wi sbrim nfim1 weq wb com12 pm5.74d sbie bitr3i pm5.74ri ) ABDEIZCA
TJABJZDEIACJZABDEFKUAUBDEACDFGLDEMZABCAUCBCNHOPQRS $.
Expand All @@ -22006,7 +22047,8 @@ proposition with a distinct variable (closed form of ~ nfsb4 ).
$d x ph $. $d x ch $.
sbiedv.1 $e |- ( ( ph /\ x = y ) -> ( ps <-> ch ) ) $.
$( Conversion of implicit substitution to explicit substitution (deduction
version of ~ sbie ). (Contributed by NM, 7-Jan-2017.) $)
version of ~ sbie ). See ~ sbied , ~ sbiedvw , ~ sbiedw for similar
variants (Contributed by NM, 7-Jan-2017.) $)
sbiedv $p |- ( ph -> ( [ y / x ] ps <-> ch ) ) $=
( nfv nfvd weq wb ex sbied ) ABCDEADGACDHADEIBCJFKL $.
$}
Expand All @@ -22015,7 +22057,8 @@ proposition with a distinct variable (closed form of ~ nfsb4 ).
$d x y ps $. $d t y $.
2sbiev.1 $e |- ( ( x = t /\ y = u ) -> ( ph <-> ps ) ) $.
$( Conversion of double implicit substitution to explicit substitution.
(Contributed by AV, 29-Jul-2023.) $)
See ~ 2sbievw for a variant with extra disjoint variables, but based on
fewer axioms. (Contributed by AV, 29-Jul-2023.) $)
2sbiev $p |- ( [ t / x ] [ u / y ] ph <-> ps ) $=
( wsb nfv weq sbiedv sbie ) ADEHBCFBCICFJABDEGKL $.
$}
Expand Down

0 comments on commit b6dd646

Please sign in to comment.