From 6bf744f66e9b90ce6273c2ca44bb7a97709d1a0f Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Thu, 31 Aug 2023 14:15:16 -0500 Subject: [PATCH] fix definition bugs (#3247) * fix definition bugs * actually a bug in the definition checker * wcel2-wl isn't primitive * Remove typesetting definition for wl-in --------- Co-authored-by: Thierry Arnoux <5831830+tirix@users.noreply.github.com> --- discouraged | 10 ------ set.mm | 87 +++++++++++++++++++---------------------------------- 2 files changed, 31 insertions(+), 66 deletions(-) diff --git a/discouraged b/discouraged index cd753e3941..2da0f735fa 100755 --- a/discouraged +++ b/discouraged @@ -14743,7 +14743,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 "crhmsubcALTV" is discouraged (1 uses). New usage of "cringcALTV" is discouraged (9 uses). New usage of "cringcatALTV" is discouraged (0 uses). @@ -18194,17 +18193,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). diff --git a/set.mm b/set.mm index 720cac75fc..8542a9c0b9 100644 --- a/set.mm +++ b/set.mm @@ -11715,6 +11715,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'; $) + $( -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- @@ -11798,6 +11801,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'; $) + $( -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- @@ -14311,9 +14318,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'; $) - $( -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- @@ -17212,6 +17216,9 @@ disjoint variable condition ( ~ sb2 ). Theorem ~ sb6f replaces the 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 @@ -17243,12 +17250,6 @@ disjoint variable condition ( ~ sb2 ). Theorem ~ sb6f replaces the 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'; $) - $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= @@ -24608,7 +24609,7 @@ range over class builders (implicitly in the case of defined class terms 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 $. @@ -437920,8 +437921,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"; @@ -507465,7 +507464,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 ) | @@ -507482,6 +507481,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 |-> @@ -507833,7 +507847,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 $) @@ -507856,9 +507870,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 $. @@ -525045,6 +525056,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 @@ -651620,45 +651634,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