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

fix definition bugs #3247

Merged
merged 6 commits into from
Aug 31, 2023
Merged

fix definition bugs #3247

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
943619d
fix definition bugs
digama0 Jun 12, 2023
2ec001c
actually a bug in the definition checker
digama0 Jun 13, 2023
88c933f
wcel2-wl isn't primitive
digama0 Jun 13, 2023
62d501b
Merge branch 'develop' into defn_fix
tirix Aug 29, 2023
82b0faa
Remove typesetting definition for wl-in
tirix Aug 29, 2023
0520f4b
Merge branch 'develop' into defn_fix
tirix Aug 29, 2023
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
10 changes: 0 additions & 10 deletions discouraged
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14622,7 +14622,6 @@ New usage of "conventions" is discouraged (0 uses).
New usage of "conventions-comments" is discouraged (0 uses).
New usage of "conventions-labels" is discouraged (0 uses).
New usage of "counop" is discouraged (0 uses).
New usage of "cqpOLD" is discouraged (0 uses).
New usage of "cramerimplem1OLD" is discouraged (0 uses).
New usage of "crhmsubcALTV" is discouraged (1 uses).
New usage of "cringcALTV" is discouraged (9 uses).
Expand Down Expand Up @@ -18081,17 +18080,8 @@ New usage of "wrdsplexOLD" is discouraged (0 uses).
New usage of "wrdvOLD" is discouraged (0 uses).
New usage of "wvd2" is discouraged (5 uses).
New usage of "wvd3" is discouraged (3 uses).
New usage of "wvhc10" is discouraged (0 uses).
New usage of "wvhc11" is discouraged (0 uses).
New usage of "wvhc12" is discouraged (0 uses).
New usage of "wvhc2" is discouraged (5 uses).
New usage of "wvhc3" is discouraged (3 uses).
New usage of "wvhc4" is discouraged (0 uses).
New usage of "wvhc5" is discouraged (0 uses).
New usage of "wvhc6" is discouraged (0 uses).
New usage of "wvhc7" is discouraged (0 uses).
New usage of "wvhc8" is discouraged (0 uses).
New usage of "wvhc9" is discouraged (0 uses).
New usage of "wwlksm1edgOLD" is discouraged (1 uses).
New usage of "wwlksnextbiOLD" is discouraged (0 uses).
New usage of "wwlksnextbij0OLD" is discouraged (1 uses).
Expand Down
91 changes: 34 additions & 57 deletions set.mm
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12270,6 +12270,9 @@ When the universe is infinite (as with set theory), such a
wal $a wff A. x ph $.
$}

$( Register 'A.' as a primitive expression (lacking a definition). $)
$( $j primitive 'wal'; $)


$(
-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
Expand Down Expand Up @@ -12353,6 +12356,10 @@ When the universe is infinite (as with set theory), such a
wceq $a wff A = B $.
$}

$( Register class-to-set promotion and class equality as primitive
expressions. $)
$( $j primitive 'cv' 'wceq'; $)


$(
-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
Expand Down Expand Up @@ -14668,9 +14675,6 @@ introduce universal quantification ("for all", e.g. ~ ax-4 ) in order to
$( Let ` t ` be an individual variable. $)
vt $f setvar t $.

$( Register 'A.' as a primitive expression (lacking a definition). $)
$( $j primitive 'wal'; $)


$(
-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
Expand Down Expand Up @@ -17303,6 +17307,9 @@ arbitrary numbers of universal quantifiers in the consequent (the series
wcel $a wff A e. B $.
$}

$( Register class membership as a primitive expression. $)
$( $j primitive 'wcel'; $)

$( Extend wff definition to include atomic formulas with the membership
predicate. This is read " ` x ` is an element of ` y ` ", " ` x ` is a
member of ` y ` ", " ` x ` belongs to ` y ` ", or " ` y ` contains
Expand Down Expand Up @@ -17334,12 +17341,6 @@ arbitrary numbers of universal quantifiers in the consequent (the series
wel $p wff x e. y $=
( cv wcel ) ACBCD $.

$( Register class-to-set promotion and class equality and membership as
primitive expressions. Although these are actually definitions, the above
ambiguity prevention necessitates our taking class equality as the
primitive, instead of set equality. $)
$( $j primitive 'weq' 'wel'; $)

tirix marked this conversation as resolved.
Show resolved Hide resolved

$(
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
Expand Down Expand Up @@ -24145,7 +24146,7 @@ Class abstractions (a.k.a. class builders)
assignment of setvar variables to class variables via the use of ~ cv . $)
cab $a class { x | ph } $.

$( $j primitive 'cv' 'wceq' 'wcel' 'cab'; $)
$( $j primitive 'cab'; $)

$( Let ` A ` be a class variable. $)
cA $f class A $.
Expand Down Expand Up @@ -436045,8 +436046,6 @@ orthogonal vectors (i.e. whose inner product is 0) is the sum of the
latexdef "/Qp" as "/_{\mathbb{Q}_p}";
htmldef "Qp" as "Qp"; althtmldef "Qp" as "Qp";
latexdef "Qp" as "\mathbb{Q}_p";
htmldef "QpOLD" as "QpOLD"; althtmldef "QpOLD" as "QpOLD";
latexdef "QpOLD" as "\mathbb{Q}_p";
htmldef "Zp" as "Zp"; althtmldef "Zp" as "Zp";
latexdef "Zp" as "\mathbb{Z}_p";
htmldef "_Qp" as "_Qp"; althtmldef "_Qp" as "_Qp";
Expand Down Expand Up @@ -438898,7 +438897,7 @@ have been translated into extensible structure versions (or are not useful).
definition of an ordered pair ~ df-op . $)
csp $a class .ih $.

$( $j primitive 'cva' 'csm' 'csp'; $)
$( $j primitive 'chba' 'cva' 'csm' 'csp'; $)

$( Extend class notation with the norm function in Hilbert space. In the
literature, the norm of ` A ` is usually written "|| ` A ` ||", but we use
Expand Down Expand Up @@ -503601,7 +503600,7 @@ valuation of the variables (v_0 ` = ( S `` (/) ) ` , v_1 ` = ( S `` 1o
df-m0s $a |- m0St = ( a e. _V |-> <. (/) , (/) , a >. ) $.

${
$d a d e h m o p r s t x y $.
$d a c d e h m o p r s t x y $.
$( Define the set of syntax axioms. (Contributed by Mario Carneiro,
14-Jul-2016.) $)
df-msa $a |- mSA = ( t e. _V |-> { a e. ( mEx ` t ) |
Expand All @@ -503618,6 +503617,21 @@ valuation of the variables (v_0 ` = ( S `` (/) ) ` , v_1 ` = ( S `` 1o
14-Jul-2016.) $)
df-msyn $a |- mSyn = Slot 6 $.

$( Define the syntax typecode function for expressions. (Contributed by
Mario Carneiro, 12-Jun-2023.) $)
df-mesyn $a |- mESyn = ( t e. _V |->
( c e. ( mTC ` t ) , e e. ( mREx ` t ) |->
( ( ( mSyn ` t ) ` c ) m0St e ) ) ) $.

$( Define the set of grammatical formal systems. (Contributed by Mario
Carneiro, 12-Jun-2023.) $)
df-mgfs $a |- mGFS = { t e. mWGFS |
( ( mSyn ` t ) : ( mTC ` t ) --> ( mVT ` t ) /\
A. c e. ( mVT ` t ) ( ( mSyn ` t ) ` c ) = c /\
A. d A. h A. a ( <. d , h , a >. e. ( mAx ` t ) ->
A. e e. ( h u. { a } )
( ( mESyn ` t ) ` e ) e. ( mPPSt ` t ) ) ) } $.

$( Define the set of proof trees. (Contributed by Mario Carneiro,
14-Jul-2016.) $)
df-mtree $a |- mTree = ( t e. _V |->
Expand Down Expand Up @@ -503969,7 +503983,7 @@ h C_ ( dom n " { m } ) ) -> m dom n a ) ) ) /\
$c GF_oo $. $( Galois limit field $)
$c ~Qp $. $( Equivalence relation for Qp $)
$c /Qp $. $( Representative of equivalence relation $)
$c Qp QpOLD $. $( p-adic rational numbers $)
$c Qp $. $( p-adic rational numbers $)
$c Zp $. $( p-adic integers $)
$c _Qp $. $( Algebraic completion of Qp $)
$c Cp $. $( Metric completion of _Qp $)
Expand All @@ -503992,9 +504006,6 @@ h C_ ( dom n " { m } ) ) -> m dom n a ) ) ) /\
$( The set of ` p ` -adic rational numbers. $)
cqp $a class Qp $.

$( The set of ` p ` -adic rational numbers. (New usage is discouraged.) $)
cqpOLD $a class QpOLD $.

$( The set of ` p ` -adic integers. (Not to be confused with ~ czn .) $)
czp $a class Zp $.

Expand Down Expand Up @@ -521193,6 +521204,9 @@ theory containing Robinson arithmetic (a fragment of Peano arithmetic), one
$( Syntax for the provability predicate. $)
cprvb $a wff Prv ph $.

$( We take 'Prv ph' as a primitive expression (lacking a definition). $)
$( $j primitive 'cprvb'; $)

${
ax-prv1.1 $e |- ph $.
$( First property of three of the provability predicate. (Contributed by
Expand Down Expand Up @@ -531399,6 +531413,7 @@ can be simplified (see ~ wl-dfrexf , ~ wl-dfrexv ).
$( Redefine ` e. ` in a class context to avoid overloading and syntax check
errors in mmj2. This operator requires ` x ` and ` B ` distinct. $)
wcel-wl $a wff x wl-el B $.
$( $j primitive 'wcel-wl'; $)
$( Redefine ` e. ` in a set context to avoid syntax check errors in mmj2.
` x ` and ` y ` must be distinct. (Contributed by Wolf Lammen,
27-Nov-2021.) $)
Expand All @@ -531408,6 +531423,7 @@ can be simplified (see ~ wl-dfrexf , ~ wl-dfrexv ).
$( Redefine ` e. ` in a class context to avoid overloading and syntax check
errors in mmj2. ` x ` and ` B ` may not be distinct. $)
wcel2-wl $a wff x wl-el2 B $.
$( $j primitive 'wcel2-wl'; $)
$( Redefine ` e. ` in a set context to avoid syntax check errors in mmj2. It
is no syntactic error to assign the same variable to ` x ` and ` y ` .
(Contributed by Wolf Lammen, 27-Nov-2021.) $)
Expand Down Expand Up @@ -644831,45 +644847,6 @@ Why not create a separate database (setg.mm) of proofs in G1, avoiding
( wvhc3 wvd1 w3a wi dfvd3an mpbir ) ABCFDGABCHDIEABCDJK $.
$}

$( Syntax for a 4-element virtual hypotheses collection. (Contributed by
Alan Sare, 17-Oct-2017.) (New usage is discouraged.) $)
wvhc4 $a wff (. ph ,. ps ,. ch ,. th ). $.

$( Syntax for a 5-element virtual hypotheses collection. (Contributed by
Alan Sare, 17-Oct-2017.) (New usage is discouraged.) $)
wvhc5 $a wff (. ph ,. ps ,. ch ,. th ,. ta ). $.

$( Syntax for a 6-element virtual hypotheses collection. (Contributed by
Alan Sare, 17-Oct-2017.) (New usage is discouraged.) $)
wvhc6 $a wff (. ph ,. ps ,. ch ,. th ,. ta ,. et ). $.

$( Syntax for a 7-element virtual hypotheses collection. (Contributed by
Alan Sare, 17-Oct-2017.) (New usage is discouraged.) $)
wvhc7 $a wff (. ph ,. ps ,. ch ,. th ,. ta ,. et ,. ze ). $.

$( Syntax for an 8-element virtual hypotheses collection. (Contributed by
Alan Sare, 17-Oct-2017.) (New usage is discouraged.) $)
wvhc8 $a wff (. ph ,. ps ,. ch ,. th ,. ta ,. et ,. ze ,. si ). $.

$( Syntax for a 9-element virtual hypotheses collection. (Contributed by
Alan Sare, 17-Oct-2017.) (New usage is discouraged.) $)
wvhc9 $a wff (. ph ,. ps ,. ch ,. th ,. ta ,. et ,. ze ,. si ,. rh ). $.

$( Syntax for a 10-element virtual hypotheses collection. (Contributed by
Alan Sare, 17-Oct-2017.) (New usage is discouraged.) $)
wvhc10 $a wff (. ph ,. ps ,. ch ,. th ,. ta ,. et ,.
ze ,. si ,. rh ,. mu ). $.

$( Syntax for an 11-element virtual hypotheses collection. (Contributed by
Alan Sare, 17-Oct-2017.) (New usage is discouraged.) $)
wvhc11 $a wff (. ph ,. ps ,. ch ,. th ,. ta ,. et ,.
ze ,. si ,. rh ,. mu ,. la ). $.

$( Syntax for a 12-element virtual hypotheses collection. (Contributed by
Alan Sare, 17-Oct-2017.) (New usage is discouraged.) $)
wvhc12 $a wff (. ph ,. ps ,. ch ,. th ,. ta ,. et ,.
ze ,. si ,. rh ,. mu ,. la ,. ka ). $.

${
vd01.1 $e |- ph $.
$( A virtual hypothesis virtually infers a theorem. (Contributed by Alan
Expand Down