Theorem pm2.61ne is:
● pm2.61ne.1
|- ( A = B -> ( ps <-> ch ) )
● pm2.61ne.2
|- ( ( ph /\ A =/= B ) -> ps )
● pm2.61ne.3
|- ( ph -> ch )
pm2.61ne
|- ( ph -> ps )
Question 1. Why isn't the first premise weakened to: ( A = B -> ( ch -> ps
) )
Question 2. Is this is a "new foundation" theorem r
Theorem pm2.61ne is the following:
Hypotheses:
pm2.61ne.1 |- ( A = B -> ( ps <-> ch ) )
pm2.61ne.2 |- ( ( ph and A =/= B ) -> ps )
pm2.61ne/3 |- ( ph -> ch )
Assertion:
pm2.61ne |- ( ph -> ps )
Question 1. Why isn't the first hypothesis given in the weaker condition:
pm2.61ne.1weaker |- ( A = B
m is true in any classical logic, so it holds in both NF and
> ZFC. (It does not hold in iset.mm, which uses intuitionistic logic,
> because there is a case distinction on A = B in this theorem.) New
> Foundations is an axiomatic system with a lot in common with ZFC, and basic
&g
The given definition of magma is:
df-mgm |- Mgm = { g | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b
A. y e. b ( x o y ) e. b }
Would it be ok to define magma as follows:
df-mgm |- Mgm = { g | A. x e. ( Base ` g ) A. y e. ( Base ` g ) ( x ( +g
` g ) y ) e. ( Base ` g ) }
If so, wh
Base ` g ) and o := ( +g ` g ) . The substitutions are
> there to make the definition more readable (and usually shorter, although
> it might be a wash in a short definition like this one). For a more
> elaborate example check out https://us.metamath.org/mpeuni/df-lmod.html .
>
>
over the length of the extraction theorem, because the former is
> an axiom and the latter is not.
>
> On Thu, Oct 12, 2023 at 12:46 AM bil...@gmail.com
> wrote:
>
>> You say that the definitions are the same, but to me "substitution" needs
>> to be proved in
@Glauco said "would it mean, either the next token in a wff or the next
label in a proof?"
I would think it would be easier to use the full expression for a statement
rather than just its label in a proof.
That is, the text would be a sequence of expressions that constitute the
hypotheses, an
There is a youtube video about using AI to create mathematical proofs for
Lean.
You can find it by searching for "Google DeepMind's AlphaProof MASSIVE MATH
BREAKTHROUGH - AI teaches itself mathematical proofs"
--
You received this message because you are subscribed to the Google Groups
"Metam
Metamath corpus that I generated from Python.
On Saturday, February 8, 2025 at 9:28:17 AM UTC-6 Glauco wrote:
> Hi Bill,
>
> Il giorno venerdì 7 febbraio 2025 alle 21:57:48 UTC+1 bil...@gmail.com
> wrote:
>
>
> I think I gave the wrong reference to the video by Andrej Karpathy
Wheeler wrote:
>
>
> > On Feb 6, 2025, at 9:29 PM, bil...@gmail.com wrote:
> >
> > I started a GitHub repository for an AI Generative Pretrained
> Transformer model for Metamath. It is base on a youtube video by Andrej
> Karpathy (Building makemore Part 2: MLP).
&g
I started a GitHub repository for an AI Generative Pretrained Transformer
model for Metamath. It is base on a youtube video by Andrej Karpathy
(Building makemore Part 2: MLP).
An example prompt and reply by the model is:
You: <|start_claim|> <|given|> |- G : _om -1-1-onto-> Z <|given|> |- ( G :
I forgot the link: https://github.com/billh0420/ClaimGPT250203.git
On Thursday, February 6, 2025 at 8:29:51 PM UTC-6 bil...@gmail.com wrote:
> I started a GitHub repository for an AI Generative Pretrained Transformer
> model for Metamath. It is base on a youtube video by Andrej Ka
Theorem rspc has the allowed substitution hint ps(x).
Is this correct? Doesn't the hypothesis rspc.1 say that x does not depend
on x?
--
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,
There is an open source GitHub site called Open Thoughts with link:
https://github.com/open-thoughts/open-thoughts
It has a chatbot called OpenThinker free to use (at least for one shot
which can be repeated by reloading the web page).
It shows its chain of thought when asked a question.
We have the assertion: copab $a class { < x , y > | ph } $.
My question is how does one know that < x , y > refers to: cop $a class < A
, B > $.
Couldn't the "<" and ">" be just notational constants to syntactically form
the class expression being introduced?
In particular, just like the intro
yntactical expression { < x , y > |
ph }.
The user might not know the "meaning" of "< x , y >" on the right hand
side, so could request a lookup for its meaning (which is has by df-op).
On Friday, May 30, 2025 at 2:10:21 PM UTC-5 di@gmail.com wrote:
>
16 matches
Mail list logo
