Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

rm ax-10 from a couple of sbied* variants #3802

Merged
merged 6 commits into from
Jan 29, 2024
Merged

rm ax-10 from a couple of sbied* variants #3802

Show file tree
Hide file tree
Changes from 4 commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
b681a92
rm ax-10 from a couple of sbied* variants
wlammen Jan 28, 2024
360dc36
discouraged
wlammen Jan 28, 2024
0702ee9
typo
wlammen Jan 28, 2024
ff606ee
reduce axiom usage for sbiedvw
wlammen Jan 29, 2024
5c6842a
review issues
wlammen Jan 29, 2024
f61fa92
review issue
wlammen Jan 29, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions discouraged
View file
Open in desktop
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
98 changes: 70 additions & 28 deletions set.mm
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17490,15 +17490,55 @@ 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 , sbrimv
wlammen marked this conversation as resolved.
Show resolved Hide resolved
based on fewer axioms, but with more disjoint variables. Based on an
wlammen marked this conversation as resolved.
Show resolved Hide resolved
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 , ~ sbiev with more disjoint variables, requiring
wlammen marked this conversation as resolved.
Show resolved Hide resolved
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 , ~ sbiedv with more disjoint variable condition,
wlammen marked this conversation as resolved.
Show resolved Hide resolved
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 a disjoint variable condition, requiring fewer
axioms. (Contributed by Gino Giotto, 10-Jan-2024.) $)
wlammen marked this conversation as resolved.
Show resolved Hide resolved
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 +19698,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 +19870,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 +22033,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 +22046,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 +22056,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
Loading