Re: [Metamath] Question abouot indistopon

['B. Wilson' via Metamath]

Thank you for the pointer, Mario. Is this negative vs. positive position
terminology something you neologized on the fly? Or does it have precedent? If
I'm grokking you correctly, the positive positions plug into the negative
positions, which jibes with your explanation and the Is-a-set convention you
reference.

Thanks for the clarity.


Mario Carneiro  wrote:
> There is a convention, which is to use "( A e. V -> ..." in antecedents to
> theorems and deduction-form statements and |- A e. _V in inference-form
> theorems. In "positive position", you often need to use A e. _V, i.e. in
> fvex there is no other reasonable option for what set to say that function
> value is a member of without any assumptions. In "negative position", it's
> a question of whether to spend one extra elex step in some cases (e.g. 2 e.
> RR therefore 2 e. _V therefore I can apply this lemma about sets to 2), or
> one extra syntax step to instantiate the V argument (which also takes some
> space in proofs). I believe the above convention is derived from some
> analysis along these lines, but it's also somewhat historical (it's more
> important to have a consistent convention). See the "Is-a-set." section of
> https://us.metamath.org/mpeuni/conventions.html for more information.
> 
> On Wed, Apr 24, 2024 at 3:52 AM heiphohmia via Metamath <
> metamath@googlegroups.com> wrote:
> 
> > > It functions much like A e. _V would. A proof using this theorem can
> > always
> > > plug in _V for V but it also could plug in On, RR, or whatever is
> > convenient.
> > > Perhaps looking at  makes it
> > clear.
> >
> > Okay, elements of ZF classes are always sets, so A e. V restricts A from
> > being
> > proper classes. That begs the question why one would ever use A e. _V
> > though.
> > Is this just a case where there's no particular convention?
> >
> > --
> > You received this message because you are subscribed to the Google Groups
> > "Metamath" group.
> > To unsubscribe from this group and stop receiving emails from it, send an
> > email to metamath+unsubscr...@googlegroups.com.
> > To view this discussion on the web visit
> > https://groups.google.com/d/msgid/metamath/272R9VKF3UZLE.34NMDVUCB3A1P%40wilsonb.com
> > .
> >


-- 
You received this message because you are subscribed to the Google Groups 
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to metamath+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/2VC9HKX4Q39T0.1ZIJO4RNZ5BIT%40wilsonb.com.

[Metamath] Mnemonic of Fr

['B. Wilson' via Metamath]

This has been bugging me midly for a while, but I couldn't figure out what the
Fr symbol in df-fr stood for:

19201 df-fr $a |- ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x 
A. z e. x -. z R y ) ) $.

I finally bothered to look up the Takeuti and Zaring reference, which also uses
"Fr" and calls R a "foundational relation". It's not super important, but would
it be worth mentioning this in df-fr's comment?

Cheers,
B. Wilson

-- 
You received this message because you are subscribed to the Google Groups 
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to metamath+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/2F5KIFFJJY2KH.28Z6N87TP90O2%40wilsonb.com.

[Metamath] Question abouot indistopon

['B. Wilson' via Metamath]

The A e. V antecedent is confusing me. Might I ask for a quick pointer?

85195 indistopon $p |- ( A e. V -> { (/) , A } e. ( TopOn ` A ) ) $= ... $.

It looks suspiciously close to A e. _V which reas as "A is a set", but in this
case the V is just floating. What are the semantics here?

-- 
You received this message because you are subscribed to the Google Groups 
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to metamath+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/3UBII6CP7S76N.3E59KU168XFGI%40wilsonb.com.

Re: [Metamath] Proposed installation conventions so things will be easier to install

['B. Wilson' via Metamath]

Here are some brainstorming questions and thoughts:

Would it make sense to have "search path" variables for metamath and mmj2?

The FHS describes /var/lib and /var/local/lib as places for "variable data" 
associated with programs in /usr and /usr/local, respectively. Ostensibly, 
the purpose of /var is so that /usr can be make read-only. In this respect, 
it makes sense to me for the set.mm repo to be checked out in a directory 
like /var/lib/metamath.  
What about mmj2? I haven't tried out mmj2 yet, but would the above apply 
there
too?

My eyes are certainly Linux-tinted, but is there some sort of analogue to 
the above for Windows?

There also seems to be some tension about installation expectations. Some 
people like the fact that metamath Just Works by downloading and extracting 
an archive to wherever. Others, like myself, seem to prefer that metamath 
Just Works by installing it like any other program on your platform.

Upstream build and distribution burden notwithstanding, it seems like both 
of these installation methods are mutually compatible.


2020年5月6日水曜日 5時25分48秒 UTC+9 Norman Megill:
>
>  Forwarded Message 
> Subject: Current problem
> Date: Tue, 5 May 2020 20:19:24 +0200 (CEST)
> From: fl
> To: Megill Norman
>
>  Hi Norm,
>
> Can you post this.
>
> I don't know how you do, but my own version of mmj2 has no problems to 
> find set.mm in the current directory.
>
> -- 
> FL
>
> On Tuesday, May 5, 2020 at 10:44:18 AM UTC-4, David A. Wheeler wrote:
>>
>> FL: 
>> > For me it's not "/usr/bin" it's "/usr/local/bin" 
>>
>> That's true for many people. Metamath-exe actually already supports this, 
>> just use "make install" with autoconf (as always that's the default). 
>> If you want /usr/bin (as is common for packages installed with a 
>> package manager), use "PREFIX=/usr/bin make install" 
>>
>> ... 
>>
>> > and set.mm is not a library it's a file of data. 
>> > You have to be able to browse it and modify it with an editor. 
>>
>> Agreed. 
>>
>> > And the applications must look for it in the current directory "." not 
>> in $HOME. 
>>
>> The bigger problem is mmj2. 
>> GUIs don't really have the concept of "current directory", and mmj2 
>> needs to know where its current database is. 
>>
>> --- David A. Wheeler
>
>

-- 
You received this message because you are subscribed to the Google Groups 
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to metamath+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/1f36efa8-a57f-4186-ab97-176fa92b31a5%40googlegroups.com.

Re: [Metamath] Proposed installation conventions so things will be easier to install

['B. Wilson' via Metamath]

Thank you for starting this discussion. As a package manager, I certainly 
empathsize strongly with efforts to make the current installation more 
standards-compliant. In that vein, I would recommend against defaulting to 
$HOME installations. Programs which do this are not common, play badly with 
packaging tools, and are generally considered bad citizens from a system 
administrator perspective. Instead, how about following the Filesystem 
Hierarchy Standard, instead?

http://www.pathname.com/fhs/pub/fhs-2.3.html

Something like the following conventions would make metamath play along 
well with the rest of the system:

/usr/bin for metamath-exe, mmj2 etc.
/var/lib/metamath for set.mm and any other databases

Similarly, by using the convention of a PREFIX variable at installation, 
one could install these tools in your local home directory by setting 
PREFIX=$HOME/.local. Metamath-exe, as an autotools build automatically 
supports this. This would make a *local* installation look like

$HOME/.local/usr/bin contains metamath-exe, mmj2 etc.
$HOME/.local/var/lib/metamath contains set.mm etc.

It's not uncommon for PATH to already contain $HOME/.local/bin, so in many 
cases a local installation would Just Work, without requiring a 
metamath-specific entry. At worst, instructing users to add this entry 
simply instructs them to follow existing conventions, which means that it 
has a better chance of working in home directories that have locked-down 
executable permissions.

Locally, I have a wrapper script around metamath that follows the above, 
letting one easily list, read, and update databases. For reference, I will 
attach it.

The above is just a rough sketch of my ideas, so if anything is unclear, 
please poke and prod with abandon. Looking forward to where this discussion 
goes!

Cheers,


2020年5月4日月曜日 2時16分07秒 UTC+9 David A. Wheeler:
>
> I want to clarify a key point in my earlier post, 
> "[Metamath] Proposed installation conventions so things will be easier to 
> install". 
>
> To make it easier to install mmj2 and other tools, I want to change the 
> conventions 
> so that "set.mm" is by default stored in its *own* directory 
> (I recommend ~/set.mm for non-Windows, C:\set.mm for Windows). 
> Separating code from data, when they're not updated at the same time, 
> makes 
> updates & many other operations much simpler. 
>
> If you really want to, you can continue to do things the old way. I just 
> want to change 
> the instructions & scripts so this is the *default*. 
>
> --- David A. Wheeler 
>

-- 
You received this message because you are subscribed to the Google Groups 
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to metamath+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/53534b3c-caa7-4512-b95f-390bcf825832%40googlegroups.com.
#!/usr/bin/env sh

METAMATH_DIR=${METAMATH_DIR-${HOME}/.local/var/lib/metamath}
METAMATH_GIT=${METAMATH_GIT-https://github.com/metamath/set.mm}
METAMATH_RC=${METAMATH_RC-${HOME}/.metamathrc}

command -v rlwrap >/dev/null && rlwrap=enabled
command -v tput >/dev/null && tput=enabled


show_usage() {
>&2 cat <<-USAGE
Usage: mm [-hlu] [-d ] [-g ] [-r ] [-s ]

Wrapper around the metamath executable, setting up the metamath
environment for easy use. The following options also provide convenient
management of metamath databases.

OPTIONS
  -h Display this help message
  -l List available databases
  -u Update databases from METAMATH_GIT into METAMATH_DIR

  -d   Path directory containing metamath databases
  -g   URL of remote git repo from which to update databases
  -r   Read  into metamath on startup
  -s Submit commands in  to metamath on startup

  -R Disable readline support with rlwrap
  -T Disable automatic height and width setting from tput

ENVIRONMENT VARIABLES
  METAMATH_DIR=${METAMATH_DIR}
Path of directory containing metamath databases
  METAMATH_GIT=${METAMATH_GIT}
URL from which to update the databases git repository
  METAMATH_RC=${METAMATH_RC}
Path to file containing metamath commands
USAGE
}

error() {
	errno=${1}
	msg=${2}

	>&2 echo "${msg}"
	show_usage
	exit "${errno}"
}

mm_update() {
	url=${1}
	dir=${2}

	command -v git >/dev/null || return 1
	[ -d "${dir}" ] || mkdir -vp "${dir}"

	if [ -d "${dir}/.git" ]; then
		git -C "${dir}" pull
	else
		git clone "${url}" "${dir}"
	fi
}


mmdir=${METAMATH_DIR}
mmgit=${METAMATH_GIT}
[ -r "${METAMATH_RC}" ] && mmrc=${METAMATH_RC}

while getopts ':hluRTd:g:r:s:' opt "${@}"; do
	case "${opt}" in
	h) show_usage; exit 0;;
	l) find "${mmdir}" -name '*.mm' -printf '%P\n'; exit;;
	u) mm_update "${mmgit}" "${mmdir}"; exit $?;;

	d) mmdir=${OPTARG};;
	g) mmgit=${OPTARG};;
	r) mmdb=${OPTARG};;
	s) mmrc=${OPTARG};;

	R) unset tput;;
	T) unset rlwrap;;

	:) error 1 "Expected argument: -${OPTARG}";;
	*) error 1 "Unknown 

Re: [Metamath] oveq2i has logical hypothesis named oveq1i.1

['B. Wilson' via Metamath]

Excellent. So I just happened to stumble upon a nice method used to organize 
related deductions. Much appreciated.

On Fri, Oct 25, 2019 at 06:24:40AM -0700, Jim Kingdon wrote:
> This is relatively common when people want related theorems to have the same
> hypothesis.
> 
> If you look at set.mm, you'll see that oveq1i.1 only appears once, but in a
> ${ $} block which includes both oveq1i and oveq2i .
> 
> On 10/25/19 2:51 AM, heiphoh...@wilsonb.com wrote:
> > Hello,
> > 
> > The logical hypothesis for theorem oveq2i has the same name as that for 
> > oveq1i. This tripped me up, but is the naming intentional?
> > 
> > In particular, I was writing up my own proof of 2p2e4 when I noticed the 
> > clash. In fact, the proof of 2p2e4 exhibits the same exact issue: the first 
> > unification is oveq1i.1=df-2, which is followed by it's parent 
> > eqtr4i.1=oveq2i. Given that 2p2e4 is used as an pedagogical example in MPE, 
> > I feel like I must just be missing something obvious.
> > 
> > Just in case, I also confirmed the above against HEAD on the develop branch 
> > (commit 2ebe15d3 at the time).
> > 
> > Forgive the spam if I am just overlooking something
> > 
> > Cheers,
> > B. Wilson
> > 
> 
> -- 
> You received this message because you are subscribed to the Google Groups 
> "Metamath" group.
> To unsubscribe from this group and stop receiving emails from it, send an 
> email to metamath+unsubscr...@googlegroups.com.
> To view this discussion on the web visit 
> https://groups.google.com/d/msgid/metamath/eddf8e5b-8733-4ebd-26fd-598253221bb3%40panix.com.

-- 
You received this message because you are subscribed to the Google Groups 
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to metamath+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/20191026034250.GB15709%40lang.