Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  newsreader  groups  login

Message-ID:  

HOST SYSTEM NOT RESPONDING, PROBABLY DOWN. DO YOU WANT TO WAIT? (Y/N)


tech / sci.math / Re: How to do meta mathematics in a theorem prover (DC Proof, etc..)

SubjectAuthor
* Re: How to do meta mathematics in a theorem prover (DC Proof, etc..)bassam karzeddin
`- Re: How to do meta mathematics in a theorem prover (DC Proof, etc..)Python

1
Re: How to do meta mathematics in a theorem prover (DC Proof, etc..)

<a350f9e0-6452-49de-a1f2-b5bb41cfc43bn@googlegroups.com>

  copy mid

https://www.novabbs.com/tech/article-flat.php?id=148850&group=sci.math#148850

  copy link   Newsgroups: sci.math
X-Received: by 2002:a05:622a:4e:b0:417:b90d:2d4 with SMTP id y14-20020a05622a004e00b00417b90d02d4mr53424qtw.5.1695249077253;
Wed, 20 Sep 2023 15:31:17 -0700 (PDT)
X-Received: by 2002:a05:6871:612:b0:1d6:c714:786d with SMTP id
w18-20020a056871061200b001d6c714786dmr3013318oan.5.1695249076404; Wed, 20 Sep
2023 15:31:16 -0700 (PDT)
Path: i2pn2.org!i2pn.org!usenet.blueworldhosting.com!diablo1.usenet.blueworldhosting.com!peer01.iad!feed-me.highwinds-media.com!news.highwinds-media.com!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: sci.math
Date: Wed, 20 Sep 2023 15:31:15 -0700 (PDT)
In-Reply-To: <bd4c7e3b-7b9b-4ea2-b9a7-5d17e5d1bf87@googlegroups.com>
Injection-Info: google-groups.googlegroups.com; posting-host=91.186.226.12; posting-account=WJi6EQoAAADOKYQDqLrSgadtdMk3xQwo
NNTP-Posting-Host: 91.186.226.12
References: <07d8383e-7dd6-4351-983a-03b521b34fb0@googlegroups.com>
<28f616cb-3965-49bc-92ac-78e8021e14ff@googlegroups.com> <a485b129-12ee-4eaa-9047-d31df355866d@googlegroups.com>
<d794928f-cb53-4d47-81f5-e3d4f5708f46@googlegroups.com> <bd4c7e3b-7b9b-4ea2-b9a7-5d17e5d1bf87@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <a350f9e0-6452-49de-a1f2-b5bb41cfc43bn@googlegroups.com>
Subject: Re: How to do meta mathematics in a theorem prover (DC Proof, etc..)
From: b.karzed...@yahoo.com (bassam karzeddin)
Injection-Date: Wed, 20 Sep 2023 22:31:17 +0000
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
X-Received-Bytes: 7497
 by: bassam karzeddin - Wed, 20 Sep 2023 22:31 UTC

On Thursday, November 23, 2017 at 6:04:43 PM UTC+2, bassam king karzeddin wrote:
> On Thursday, November 23, 2017 at 3:58:03 PM UTC+3, burs...@gmail.com wrote:
> > Maybe use this booklet:
> >
> > 30: A Tour through Mathematical Logic
> > (Carus Mathematical Monographs) Paperback – 10 Mar 2005
> > by Robert S. Wolf (Author)
> > http://www.jstor.org/stable/27641911
> >
> > Am Donnerstag, 23. November 2017 13:49:06 UTC+1 schrieb burs...@gmail.com:
> > > Whats very easy is for example ZFC minus empty
> > > set axiom, and empty set skolemized:
> > >
> > > forall x (~ x in 0) AxEmpty
> > >
> > > We then see for structures S=<V,∈,0>,
> > > If T is a substructure of S and both
> > > model of ZFC\AxEmpty, and S model of
> > >
> > > AxEmpty, then T also model of AxEmpty.
> > >
> > > Am Donnerstag, 23. November 2017 13:42:44 UTC+1 schrieb burs...@gmail..com:
> > > > A good start to study model theory, and to
> > > > avoid psychotic schizophrenia, is to start with
> > > > a formalization of elementary substructure.
> > > > We know a structure for set theory is a pair:
> > > >
> > > > <V, ∈> where ∈ : V x V
> > > >
> > > > we can do some classical model theory, where
> > > > we would assume V and ∈ just set on the meta level.
> > > > Now what is a elementary substructure? Well
> > > > we can translate substructure to subset, and
> > > >
> > > > start with another structure:
> > > >
> > > > <W, η> where η : W x W
> > > >
> > > > And we can say it is a direct substructure if, not
> > > > using the more complicated embedding but directly:
> > > >
> > > > W subset V (1)
> > > >
> > > > η subset ∈ (2)
> > > >
> > > > Well (2) is a little too weak, we could have too few
> > > > elements η , so whats actually required:
> > > >
> > > > η = ∈ intersect W x W
> > > >
> > > > For such an embedding there are already high chances that
> > > > its elementary, in the sense that ZFC axioms are preserved.
> > > > Many axioms contain forall quantifier, so that the submodel
> > > > property helps. But not all embeddings are elementary.
> > > >
> > > > The Skolem paradox says, there is an elementary embedding
> > > > into a countable model.
> > > >
> > > > For preservation under submodels see here:
> > > > https://en.wikipedia.org/wiki/%C5%81o%C5%9B%E2%80%93Tarski_preservation_theorem
> > > >
> > > > For embedding see here:
> > > > https://en.wikipedia.org/wiki/Embedding#Universal_algebra_and_model_theory
> > > >
> > > > Am Donnerstag, 23. November 2017 02:24:00 UTC+1 schrieb burs...@gmail.com:
> > > > > Brain storming: You could try the following:
> > > > >
> > > > > a) Classical object level modelling
> > > > > - Use the native wff and proof/model theory
> > > > > of the prover for the meta level
> > > > > - Create an extra object level define things such as
> > > > > - Wff formulas of the logic
> > > > > - Proof theory of the logic
> > > > > - Model theory of the logic
> > > > > - Some interesting theory in the logic
> > > > >
> > > > > Ex.:
> > > > > HOL/Isabelle is already itself an object level in
> > > > > some more pure meta level, but nevertheless
> > > > > many proof archives it seems use this approach so
> > > > > the HOL object level becomes the meta level, and
> > > > > a new object level is created.
> > > > >
> > > > > b) Some middle ground
> > > > > - Extend your prover so that it supports
> > > > > sets and classes
> > > > > - A lot of native proof/model theory can be
> > > > > reused, there is little difference between
> > > > > a class:
> > > > > { x | A(x) }
> > > > > and a set:
> > > > > { x in y | A(x) }
> > > > > There is overlap for the wff A(x), and the
> > > > > "elements" of a class are alreaDY sets.
> > > > >
> > > > > Ex.:
> > > > > It seems to me that metamath.org
> > > > > is an example here.
> > > > >
> > > > > What are the obstacles? what can you show? How
> > > > > much trust will you have?
> Because most of the modern mathematics had been recently proven wrong and baseles beyond beileafs and beyond any little doubts, mainly after the Pythagorean era, where this discovered theorem contradicts absolutely most of our current famous results in mathematics, and because mathematicians for many long centuries had not yet realized fully what did PT mean exactly then this implies immediately that most of those meaningless references you keep providing with all those manufactured notations they usually use are actually pure tools of cheating and very deep juggling that are used to deceive and abuse the innocent human minds, where normal people usually run away thinking that they are inferior to those who are actually a punch of mad people
>
> But mathematics is merely and so simply are very rare pure discoveries that are strictly related to the existing physical reality of space dimensions, whereas that human-made juggling mathematics was never any pure discoveries but pure foolish decisions of madman brain fart that keeps deliberately contradicting perpetual discovered absolute facts so obviously under the sunlight, for sure
>
> All Irrefutable claims of mine as (Theorems, Conjectures, Formulas, Unsolved puzzles, ...etc) were PUBLISHED FREELY and PROVED RIGOROUSLY here at sci.math and elsewhere by me and by few others for sure
>
> And there was no other choice to me by Traditional Peer-Review old manners since this is a big revolution against the global ignorance, where this must be performed publically and no other way for sure
>
> Bassam King Karzeddin
> Nov. 23ed, 2017

Re: How to do meta mathematics in a theorem prover (DC Proof, etc..)

<uefssv$354ns$5@dont-email.me>

  copy mid

https://www.novabbs.com/tech/article-flat.php?id=148853&group=sci.math#148853

  copy link   Newsgroups: sci.math
Path: i2pn2.org!i2pn.org!eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: pyt...@invalid.org (Python)
Newsgroups: sci.math
Subject: Re: How to do meta mathematics in a theorem prover (DC Proof, etc..)
Date: Thu, 21 Sep 2023 00:49:03 +0200
Organization: A noiseless patient Spider
Lines: 118
Message-ID: <uefssv$354ns$5@dont-email.me>
References: <07d8383e-7dd6-4351-983a-03b521b34fb0@googlegroups.com>
<28f616cb-3965-49bc-92ac-78e8021e14ff@googlegroups.com>
<a485b129-12ee-4eaa-9047-d31df355866d@googlegroups.com>
<d794928f-cb53-4d47-81f5-e3d4f5708f46@googlegroups.com>
<bd4c7e3b-7b9b-4ea2-b9a7-5d17e5d1bf87@googlegroups.com>
<a350f9e0-6452-49de-a1f2-b5bb41cfc43bn@googlegroups.com>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Wed, 20 Sep 2023 22:49:03 -0000 (UTC)
Injection-Info: dont-email.me; posting-host="2a20f7057a1704d4a8f2351e41eeedde";
logging-data="3314428"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+debs+GhZqM92wK5pgj/A+"
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:102.0) Gecko/20100101
Thunderbird/102.3.3
Cancel-Lock: sha1:0Korc+/tTHbpanOxfa/j6giPO4s=
In-Reply-To: <a350f9e0-6452-49de-a1f2-b5bb41cfc43bn@googlegroups.com>
Content-Language: en-US
 by: Python - Wed, 20 Sep 2023 22:49 UTC

Le 21/09/2023 à 00:31, bassam karzeddin a écrit :
> On Thursday, November 23, 2017 at 6:04:43 PM UTC+2, bassam king karzeddin wrote:
>> On Thursday, November 23, 2017 at 3:58:03 PM UTC+3, burs...@gmail.com wrote:
>>> Maybe use this booklet:
>>>
>>> 30: A Tour through Mathematical Logic
>>> (Carus Mathematical Monographs) Paperback – 10 Mar 2005
>>> by Robert S. Wolf (Author)
>>> http://www.jstor.org/stable/27641911
>>>
>>> Am Donnerstag, 23. November 2017 13:49:06 UTC+1 schrieb burs...@gmail.com:
>>>> Whats very easy is for example ZFC minus empty
>>>> set axiom, and empty set skolemized:
>>>>
>>>> forall x (~ x in 0) AxEmpty
>>>>
>>>> We then see for structures S=<V,∈,0>,
>>>> If T is a substructure of S and both
>>>> model of ZFC\AxEmpty, and S model of
>>>>
>>>> AxEmpty, then T also model of AxEmpty.
>>>>
>>>> Am Donnerstag, 23. November 2017 13:42:44 UTC+1 schrieb burs...@gmail.com:
>>>>> A good start to study model theory, and to
>>>>> avoid psychotic schizophrenia, is to start with
>>>>> a formalization of elementary substructure.
>>>>> We know a structure for set theory is a pair:
>>>>>
>>>>> <V, ∈> where ∈ : V x V
>>>>>
>>>>> we can do some classical model theory, where
>>>>> we would assume V and ∈ just set on the meta level.
>>>>> Now what is a elementary substructure? Well
>>>>> we can translate substructure to subset, and
>>>>>
>>>>> start with another structure:
>>>>>
>>>>> <W, η> where η : W x W
>>>>>
>>>>> And we can say it is a direct substructure if, not
>>>>> using the more complicated embedding but directly:
>>>>>
>>>>> W subset V (1)
>>>>>
>>>>> η subset ∈ (2)
>>>>>
>>>>> Well (2) is a little too weak, we could have too few
>>>>> elements η , so whats actually required:
>>>>>
>>>>> η = ∈ intersect W x W
>>>>>
>>>>> For such an embedding there are already high chances that
>>>>> its elementary, in the sense that ZFC axioms are preserved.
>>>>> Many axioms contain forall quantifier, so that the submodel
>>>>> property helps. But not all embeddings are elementary.
>>>>>
>>>>> The Skolem paradox says, there is an elementary embedding
>>>>> into a countable model.
>>>>>
>>>>> For preservation under submodels see here:
>>>>> https://en.wikipedia.org/wiki/%C5%81o%C5%9B%E2%80%93Tarski_preservation_theorem
>>>>>
>>>>> For embedding see here:
>>>>> https://en.wikipedia.org/wiki/Embedding#Universal_algebra_and_model_theory
>>>>>
>>>>> Am Donnerstag, 23. November 2017 02:24:00 UTC+1 schrieb burs...@gmail.com:
>>>>>> Brain storming: You could try the following:
>>>>>>
>>>>>> a) Classical object level modelling
>>>>>> - Use the native wff and proof/model theory
>>>>>> of the prover for the meta level
>>>>>> - Create an extra object level define things such as
>>>>>> - Wff formulas of the logic
>>>>>> - Proof theory of the logic
>>>>>> - Model theory of the logic
>>>>>> - Some interesting theory in the logic
>>>>>>
>>>>>> Ex.:
>>>>>> HOL/Isabelle is already itself an object level in
>>>>>> some more pure meta level, but nevertheless
>>>>>> many proof archives it seems use this approach so
>>>>>> the HOL object level becomes the meta level, and
>>>>>> a new object level is created.
>>>>>>
>>>>>> b) Some middle ground
>>>>>> - Extend your prover so that it supports
>>>>>> sets and classes
>>>>>> - A lot of native proof/model theory can be
>>>>>> reused, there is little difference between
>>>>>> a class:
>>>>>> { x | A(x) }
>>>>>> and a set:
>>>>>> { x in y | A(x) }
>>>>>> There is overlap for the wff A(x), and the
>>>>>> "elements" of a class are alreaDY sets.
>>>>>>
>>>>>> Ex.:
>>>>>> It seems to me that metamath.org
>>>>>> is an example here.
>>>>>>
>>>>>> What are the obstacles? what can you show? How
>>>>>> much trust will you have?
>> Because most of the modern mathematics had been recently proven wrong and baseles beyond beileafs and beyond any little doubts, mainly after the Pythagorean era, where this discovered theorem contradicts absolutely most of our current famous results in mathematics, and because mathematicians for many long centuries had not yet realized fully what did PT mean exactly then this implies immediately that most of those meaningless references you keep providing with all those manufactured notations they usually use are actually pure tools of cheating and very deep juggling that are used to deceive and abuse the innocent human minds, where normal people usually run away thinking that they are inferior to those who are actually a punch of mad people
>>
>> But mathematics is merely and so simply are very rare pure discoveries that are strictly related to the existing physical reality of space dimensions, whereas that human-made juggling mathematics was never any pure discoveries but pure foolish decisions of madman brain fart that keeps deliberately contradicting perpetual discovered absolute facts so obviously under the sunlight, for sure
>>
>> All Irrefutable claims of mine as (Theorems, Conjectures, Formulas, Unsolved puzzles, ...etc) were PUBLISHED FREELY and PROVED RIGOROUSLY here at sci.math and elsewhere by me and by few others for sure
>>
>> And there was no other choice to me by Traditional Peer-Review old manners since this is a big revolution against the global ignorance, where this must be performed publically and no other way for sure
>>
>> Bassam King Karzeddin
>> Nov. 23ed, 2017

So what bASSam? Stupid in 2017, still stupid in 2023.

Find another hobby, math is not your thing.

1
server_pubkey.txt

rocksolid light 0.9.8
clearnet tor