Generalization principle: full presentation

162 views
Skip to first unread message

Zuhair

unread,
Nov 21, 2015, 1:59:13 PM11/21/15
to
Here I'll post this principle in full, just in case the link won't work. A link to this full work is presented below:

The extensional well founded hereditarily finite set (abbreviated as hereditarily finite sets in the rest of this account) realm appears to be the most natural set realm, and so if we can figure out some way of generalizing some kinds of results from it to the whole realm of sets, then this might be of help in both understanding sets and possibly guides derivation of some stronge set principles that have a natural look.
The naive idea is that some properties that are closed over the class of all hereditarily finite sets would also close over the class of all sets. We need to define a theory that helps us decide on some of these properties.
To tackle this I'll define a notion of "elevation" on formulas:
A formula Q+ would be called an elevated formula of Q if and only if Q+ is obtained from just replacing each occurrence of "HF" in Q by V, where HF is the symbol given to the class of all hereditarily finite sets, and V is the symbol denoting the class of all sets.
Now the development is to define a notion of "existential equivalence" between formulas Q and Q+ as follows:
Q is existentially equivalent to Q+ <-> for every subformula pi(y,x1,..,xn) of Q: Ax1 e HF,.., Axn e HF[Ey (pi(y,x1,..,xn))] <-> Ax1 e V,.., Axn e V [Ey (pi+(y,x1,..,xn))].
Where n is the total number of parameters in pi.
(notation: "A" denotes "for all", while "E" denotes "exists", and "e" denotes membership)
In English every subformula pi of Q with all of its parameters being relativised to hereditarily finite sets must hold of an object if and only if its elevated form pi+ with all of its parameters being relativised to sets must hold of an object.
HF is defined as the union of the intersectional class of all power-inductive classes (classes containing the empty set among their elements, that are closed under existence of power sets).
I'll denote existential equivalence by "<-E->".
My holding assumption is that existentially equivalent formulas can generalize results from the hereditarily finite set realm to the whole realm of sets.
So to formally capture that, we write:
Principle of Generalization: for n=1,2,3,..; if Q(y,x1,..,xn) is a formula in which only y,x1,..,xn occur free, then:
(Q <-E-> Q+) & (Ax1 e HF .. Axn e HF [Ay (Q(y,x1,..,xn) -> y e HF)]) -> (Ax1 e V .. Axn e V [Ay (Q+(y,x1,..,xn) -> y e V)])
is an axiom.
Now this principle when added to Extensionality, Impredicative class comprehension of MK, and an axiom of existence of a power-inductive class and an axiom of infinity, then the result is a theory that can interpret ZF over the realm of sets (members of classes) of it.
A nice corollary of this is that any formula using no more than three subformulas that is closed on the hereditarily finite set realm would also close on the whole realm of sets, and just using those formulas one can prove all axioms of Zermelo set theory "Z".

EXAMPLES:
To run an example of this method lets try to prove Singletons.
So here we take Q(y,x) to be

Az (z e y <-> z=x)

Now for this case the formula is itself its elevated form since
it contains no HF symbol, and so all of its subformas are their elevated
forms.

Now we check the subformula z=x
first take x to be the paramter and check whether
Ax e HF Ez (z=x) <-> Ax e V Ez (z=x)
which is true.

Now take z to be the paramter and check whether
Az e HF Ex (z=x) <-> Az e V Ex (z=x)
Which is true.

Now we check the subformula z e y:
Az e HF Ey (z e y) <-> Az e V Ey (z e y)
Ay e HF Ez (z e y) <-> Ay e V Ez (z e y)
which are true.


Now we check the formula z e y <-> z=x:
Az,x e HF Ey (z e y <-> z=x) <-> Az,x e V Ey (z e y <->z=x)
Az,y e HF Ex (z e y <-> z=x) <-> Az,y e V Ex (z e y <->z=x)
Ay,x e HF Ez (z e y <-> z=x) <-> Ay,x e V Ez (z e y <->z=x)
which are true.


At last we need to check the formula: Az (z e y <-> z=x) itself:
Ax e HF Ey (Az (z e y <-> z=x)) <-> Ax e V Ey (Az(z e y <-> z=x))
Ay e HF Ex (Az (z e y <-> z=x)) <-> Ay e V Ex (Az(z e y <-> z=x))
which are true.

So Q is existentially equivalent to its elevated form.

So we can apply the generalization principle, and since we have:

Q <-E-> Q+ & Ax e HF: Ay [Az(z e y <-> z=x) -> y e HF]

then it follows

Ax e V Ay [Az(z e y <-> z=x) -> y e V]

which is Singletons!

Another example is to prove Separation:
So Q would be the formula Az (z e y -> z e x)
The checks are:
Az e HF Ex (z e x) <-> Az e V Ex (z e x)
Ax e HF Ez (z e x) <-> Ax e V Ez (z e x)
Same checks would apply to z e y
Az,y e HF Ex (z e y -> z e x) <-> Az,y e V Ex (z e y -> z e x)
Az,x e HF Ey (z e y -> z e x) <-> Az,x e V Ey (z e y -> z e x)
Ax,y e HF Ez (z e y -> z e x) <-> Ax,y e V Ez (z e y -> z e x)
And at last:
Ax e HF Ey Az (z e y -> z e x) <-> Ax e V Ey Az (z e y -> z e x)
Ay e HF Ex Az (z e y -> z e x) <-> Ay e V Ex Az (z e y -> z e x)
Clearly all above checks hold. And since we have:
Q <-E-> Q+ & Ax e HF: Ay [Az(z e y -> z e x) -> y e HF]
Then by Generalization principle it would follow that:
Ax e V: Ay [Az(z e y -> z e x) -> y e V]
Which is Separation.

Zuhair

For clearer veiw see:
https://sites.google.com/site/zuhairaljohar/the-generalization-principle

Rupert

unread,
Nov 21, 2015, 5:26:11 PM11/21/15
to
On Saturday, November 21, 2015 at 7:59:13 PM UTC+1, Zuhair wrote:
> Here I'll post this principle in full, just in case the link won't work. A link to this full work is presented below:
>
> The extensional well founded hereditarily finite set (abbreviated as hereditarily finite sets in the rest of this account) realm appears to be the most natural set realm, and so if we can figure out some way of generalizing some kinds of results from it to the whole realm of sets, then this might be of help in both understanding sets and possibly guides derivation of some stronge set principles that have a natural look.
> The naive idea is that some properties that are closed over the class of all hereditarily finite sets would also close over the class of all sets. We need to define a theory that helps us decide on some of these properties.
> To tackle this I'll define a notion of "elevation" on formulas:
> A formula Q+ would be called an elevated formula of Q if and only if Q+ is obtained from just replacing each occurrence of "HF" in Q by V, where HF is the symbol given to the class of all hereditarily finite sets, and V is the symbol denoting the class of all sets.

Let's analyse this further. You said the language of the theory was the mono-sorted first-order language of set theory. Are you saying that you are using a version of this language such that an abstraction term can occur in an unabbreviated formula? Or are you assuming some effective procedure whereby given an unabbreviated formula Q we can tell whether or not there is some abbreviated version of it of an appropriate kind in which an abstraction term which could be abbreviated by "HF" occurs?

Justin Thyme

unread,
Nov 22, 2015, 8:24:19 AM11/22/15
to
It's interesting but not very readable. How about proper maths type
setting for the web page?

--
Nam Nguyen: *As we speak*, MS and NN would understand what "blue" would
mean.
Martin Shobe: No I don't. You could mean the color, the feeling, or
given your past history, something entirely different.
Nam Nguyen: Go and get fucked.

sci.logic 24/10/2015

Nam Nguyen

unread,
Nov 22, 2015, 11:21:40 AM11/22/15
to
On 22/11/2015 6:24 AM, Justin Thyme wrote:
<snipped>

Idiotic trolling.

See: https://groups.google.com/d/msg/sci.logic/8r3LRfHLWpk/FJAjQRZsEAAJ

--
Nam Nguyen (on professor Daniel Isaacson's paper):

But you ignored what he pointed (alluded) to as the non-transient
sense of his "unknown"! So your argument is incorrect, unsound.

Justin Thyme: Fuck what he alluded to!

sci.logic 19/08/2015
--
Nam Nguyen: The English "unknown" just means "not known"

Justin Thyme (being an intellectual pervert):

did you get through school with anything more than the
teacher's gratitude for those few days when you didn't
wet yourself?

sci.logic 19/08/2015

Zuhair

unread,
Nov 22, 2015, 3:34:24 PM11/22/15
to
First of all the language is mono-sorted first order language of CLASS theory, all variable symbols stand for CLASSES.

Of course the symbols HF and V are "defined" symbols, and so formulas using them are of course "abbreviated formulas" in the usual sense much as 0 is a defined symbol representing the empty set, so when we way for example
~Exist x. x e 0, this is in reality an abbreviation for
for all k (for all y (y e k <-> ~y=y) -> ~Exist x. x e k).

To answer your second question, if I understood it, then the answer is NO.
More explicitly: I'm NOT assuming some effective procedure whereby given an unabbreviated formula Q we can tell whether or not there is some abbreviated version of it of an appropriate kind in which an abstraction term which could be abbreviated by "HF" occurs?

The occurrence of HF in the formula Q(y,x1,..,xn) that I was speaking about in the generalization scheme means that Q is an abbreviated formula since HF is an abbreviation.

Zuhair

Zuhair

unread,
Nov 23, 2015, 7:32:26 AM11/23/15
to
On Sunday, November 22, 2015 at 4:24:19 PM UTC+3, Justin Thyme wrote:
> It's interesting but not very readable. How about proper maths type
> setting for the web page?
>

OK, I've changed the type setting to the usual one. Hope its readable.

Zuhair

Zuhair

unread,
Nov 23, 2015, 7:35:27 AM11/23/15
to
On Sunday, November 22, 2015 at 1:26:11 AM UTC+3, Rupert wrote:
See my earlier response to this. I just wanted to add that all what is needed is for the elevated formula of phi to be decidable from phi, and this is easily done, just replace every symbol HF in phi by V and you get its elevated form. IF there was no HF symbol in phi then phi is itself its elevated form.

Zuhair

Charlie-Boo

unread,
Nov 29, 2015, 5:36:44 PM11/29/15
to
Zuhair, I think it would help if you started with one or two examples of specific problems that you are trying to address, then go into your approach, it's generality and its formalization (for me, anyway.)

E.g. "The naive idea is that some properties that are closed over the class of all hereditarily finite sets would also close over the class of all sets. We need to define a theory that helps us decide on some of these properties."

Why not give examples of properties, show that some are closed and others are not, and some of the closed ones are closed under all sets and others aren't? Then you show the list and state how you intend to show it is closed in a different manner than you used to justify their state in the list (if I understand you correctly.)

With all due respect, it seems that you are anxious to present the generalization and its formalization before the specific cases, which is somewhat backwards. :)

Makes sense?

C-B

Zuhair

unread,
Nov 29, 2015, 9:05:33 PM11/29/15
to
It makes sense but it is trivial

Zuhair

Rupert

unread,
Nov 30, 2015, 11:31:45 AM11/30/15
to
All right then. So Q and Q+ are abbreviated formulas. Then you go on to speak of a subformula of Q. Does that mean a subformula of the unabbreviated version of Q, or if not then what is meant by a subformula of an abbreviated formula exactly?

Charlie-Boo

unread,
Dec 1, 2015, 1:04:35 AM12/1/15
to
On Sunday, November 29, 2015 at 9:05:33 PM UTC-5, Zuhair wrote:
> It makes sense but it is trivial
>
> Zuhair

Whether it is trivial or not, you haven't done it. It is just a bunch of formalisms with no examples of how it accomplishes anything - very typical of you. Have you read my posts? I prove actual theorems about incompleteness, give shorter proofs than are published. These are real results. A bunch of formalisms and an occasional claim that it represents something or includes something doesn't mean it has any value. It is "a solution in search of a problem."

And your logic is usually very weak. I have pointed out a number of times how you have missed a simple point. You miss the fact that what you are comparing your representation of a pair to is simply the 2 values reversed with set enclosure removed. You miss a trivial proof that the undecidable sentences are not r.e. - it is simply Turing's result using proof instead of halting.

Are you good in mathematics? Mathematics is for real. You can't BS answers to math problems. I won every math contest throughout high school - only perfect college board score in math ever in my school - first place in the county in the annual Mathematics Association of America Mathematics competition. I am for real, Zuhair. You give a bunch of expressions and end it with how great it is, but don't justify that claim.

Do you know what your IQ is, Zuhair? Take a math IQ test and tell us, ok? Mine is 155. You should listen to intelligent people, rather than trying to imitate BS professors with fancy sounding terms that do not demonstrate any value.

Real examples would show real value.

C-B

Ross A. Finlayson

unread,
Dec 1, 2015, 1:27:35 AM12/1/15
to
Zuhair's a neurosurgeon.

Zuhair

unread,
Dec 1, 2015, 3:01:14 PM12/1/15
to
Q is an abbreviated formula only if it contains the symbol HF or the symbol V
in it otherwise the other symbols in Q are all non abbreviated. Now if Q doesn't contain those symbols then it is exactly Q+. What is meant by a subformula of Q is a substring of Q the meets the qualification of a formula. This is decidable and it can be recursively defined by incorporating the symbols V and HF in the formula formation rules, so we have:

for any variable symbols xi,xj:
xi e xj is a formula
xi=xj is a formula
xi e HF is a formula
HF e xi is a formula
xi=HF is a formula
HF=xi is a formula

Those are the 'atomic' formulas.

Now if phi and pi are formulas then phi connective symbol pi
is a formula.

if phi(x) is a formula in which x occurs then Ax(phi) is a formula
and Ex(phi) is a formula

If phi is a formula in which HF occurs then replacing V instead of HF
yields a formula (which is phi+).

Those were the formation rules of formulas.

From those rules then it is clear that if we are presented with a formula phi then we can totally decide on where a string of symbols pi is a subformula of phi or not. We simply take the set of all atomic subformulas of phi and then formulas built from those atomic subformulas along the above formation rules are totally decidable and of course it is decidable whether a string is a substring of a formula or not. So a substring of a formula Q (whether Q contains the abbreviated symbols HF and V in it or not) that is a formula
along the above recursive formation rules, is what is meant by a subformula of Q.

Zuhair

Message has been deleted

Zuhair

unread,
Dec 1, 2015, 3:21:13 PM12/1/15
to
OK, I'll mention some of those but not in detail.

The hereditarily finite sets are sets that are finite and every element of them is finite and every element of element of them is finite and in turn every element of those is finite and so forth....

Define E_n as "n_th deep element" relation, so y E_n x means y is an n_th deep element of x to mean that there exists x1,x2,..,xn such that x1 in x2 in x3 in...in xn and xn in x and y=x1, then we say that x is hereditarily finite if
every n_th element of x is finite, and also x itself is finite.

Now it is clear that there are some properties that are closed over the hereditarily finite world, for example pairing, since for every a,b that are hereditarily finite then {a,b} is also hereditarily finite, similarly union is also closed over the hereditarily finite world since for every hereditarily finite set x the set U(x) (i.e. the set of all elements of elements of x) is also hereditarily finite. Same applies to power. Also it is clear that a subset of a hereditarily finite set is also hereditarily finite which entails that separation is closed over the hereditarily finite world, also replacing each element of a hereditarily finite set by a hereditarily finite set results in a hereditarily finite set, which entails that replacement is also closed over the hereditarily finite set world.

Now generalize all those above rules and you get ZF-infinity.

However there are some properties that although closed over the hereditarily finite world but yet cannot be generalized to the whole set realm since they would cause contradictions if so generalized, that's why I adopted the restriction of 'existential equivalence' in order to pick up those formulas that describe properties that can be generalized from the hereditarily finite world to the whole realm of sets, and that's the purpose of the above theory.

Zuhair

Zuhair

unread,
Dec 1, 2015, 5:37:44 PM12/1/15
to
Just to clarify matters, the symbols V and HF are definable zero place
function symbols in other words "constants" so they can replace
any variable symbol in a formula and the result would be a formula.
So already the usual formula formation rules of first order logic can
decide on whether a string of symbols containing constants (definable or not)
is formula or not. So a sub-formula of Q is:

a substing of Q that is a formula.

Zuhair

Zuhair

unread,
Dec 1, 2015, 5:47:43 PM12/1/15
to
no I'm a Neurologist.

Zuhair

Ross A. Finlayson

unread,
Dec 1, 2015, 6:38:39 PM12/1/15
to
On Tuesday, December 1, 2015 at 2:47:43 PM UTC-8, Zuhair wrote:
> no I'm a Neurologist.
>
> Zuhair

Excuse me, thank you. Zuhair's a genius.

Charlie-Boo

unread,
Dec 1, 2015, 9:26:46 PM12/1/15
to
So? Does that change his ineptitude in analyzing simple problems of logic like the 2 that I cite above?

Do you think the 2 problems that he failed to understand and solve were difficult? They both were discussed the last time I spent a few days checking out SCI.LOGIC. They are not select examples from a huge number of problems. They were the current problems being discussed when I checked in.

I once wrote software for a successful, well-known surgeon, and the first thing he said to me when I met him in person was "Why can't they print a damn medical record?"

I wrote an enhancement to a huge public domain (free) electronic medical records system for him that I obtained a copy of for him - dumping a patient's data to a thumb drive - and he immediately sent out 200 emails to people saying he was a vendor of a fantastic "mobile medical records system" for which he was announcing its "national rollout". I told him that he would need to know how to install, use, train, maintain, enhance etc. this massive system for customers which he knew nothing about. (The documentation is at least 1,000 pages.)

I asked "What are they going to do when they have a question about how to use it?" since he knew nothing about how to use it. His answer, "They call the help desk!!"

He called himself a "visionary" because he had a system for people to carry around thumb drives with their medical records on them - when various health plans have been storing medical records on cards for a decade.

Are you thinking there's a correlation between having a steady hand and knowing Mathematics? I think Zuhair refutes that. My customer had a very steady hand and made a lot of money from it. But was he technically talented? You decide.

How about if we decide on an IQ test or set of puzzles and we can all see how smart we really are? I don't like to brag and I normally do so only in jest. But when someone acts like they have an endless stream of fantastic innovations by displaying various expressions and definitions, and when I ask why they are valuable I get a one sentence response, shouldn't I wonder?

Maybe you can explain what his latest invention accomplishes.

"He who seeks for methods without having a definite problem in mind seeks in the most part in vain." - David Hilbert

C-B

Charlie-Boo

unread,
Dec 1, 2015, 9:32:34 PM12/1/15
to
Oh, good. I'll take a look. Thanks, Zuhair.

C-B

Charlie-Boo

unread,
Dec 1, 2015, 9:33:36 PM12/1/15
to
On Tuesday, December 1, 2015 at 5:47:43 PM UTC-5, Zuhair wrote:
> no I'm a Neurologist.
>
> Zuhair

How much mathematics have you taken?

C-B

Ross A. Finlayson

unread,
Dec 1, 2015, 9:33:58 PM12/1/15
to
How about instead we work on the Hilbert Program
together. I see that as Zuhair, for example, regularly
emits axiomatics about usual systems that are as suited
(under "equi-interpretability", the usual coinage) as
others formally, that then concretely are variously suited
for their "performance", "efficiency" or "power", elegance
and etcetera. You seem interested in the bounds of formal
systems and the differences between recursion limits and
quantification limits, of a sort. I put forth the null axiom
theory and demand that mathematics includes real infinitesimals
for application and for foundations.

So, we each find neat use of sci.logic for that it's cheap
and runs on the Internet (and is thus surprisingly under-
utilized), why not.

I'm not suggesting that we work together so much as
that we do.

Charlie-Boo

unread,
Dec 1, 2015, 9:35:41 PM12/1/15
to
A genius in mathematical logic? How's that?

C-B

Charlie-Boo

unread,
Dec 1, 2015, 10:07:43 PM12/1/15
to
What does "generalize all those above rules and you get ZF-infinity" mean? E.g. what do you get if you generalize: {HF1,HF2} is HF ?

C-B

Charlie-Boo

unread,
Dec 1, 2015, 10:20:05 PM12/1/15
to
In what sense can we work on Hilbert's Program since it is unattainable?

> I see that as Zuhair, for example, regularly
> emits axiomatics about usual systems that are as suited
> (under "equi-interpretability", the usual coinage) as
> others formally, that then concretely are variously suited
> for their "performance", "efficiency" or "power", elegance
> and etcetera. You seem interested in the bounds of formal

The system itself meets that spec doesn't it? Or by changing syntax and other incidentals. What sense is that if there is no improvement - or am I missing something?

Are you aware of any improvement in a Zuhair system over what has been published? (btw perhaps you have noticed the relationship between what I exhibit here and other forums e.g. FOM vs. these same published systems. Anything like that from Zuhair? That I would be interested in.)

C-B

Charlie-Boo

unread,
Dec 1, 2015, 10:24:27 PM12/1/15
to
I think you're just saying that they are inconsistent with ZF when the HF condition is dropped.

C-B

Charlie-Boo

unread,
Dec 1, 2015, 10:35:01 PM12/1/15
to
Can you give some "properties" (rules) that are not closed over the hereditary finite world?

C-B

Charlie-Boo

unread,
Dec 1, 2015, 10:52:23 PM12/1/15
to
I can think of 1 rule not closed over HF sets, actually, but I wonder if you have any significantly different than this 1 obvious trick.

My immediate take was that you have trees with a finite number of branches at each node and each of your examples of rules closed over HF are properties of finiteness F: F+F , F*F , F^F , F-F are all F (finite.)

So far it's not much different from what I've seen from you before, Zuhair. Like the previous times when I said "But that's just...which is trivial." such as comparing {a,b} with {{b},{a}} for some a and b, and wondering why he did it (with the answer being obvious.)

There's nothing wrong with that, of course. Who hasn't? But to go on and on about it before people have a chance to point out it is equivalent to something trivial is a bit much - won't you agree (as a principle)? :)

I sincerely hope that I didn't offend anyone, but when someone's child is a brat I think it is best to just say "Your kid's a brat." and hope he isn't too prideful.

I think some may agree that I routinely ridicule myself and may be a bit above this pride stuff. Like my (in)famous water bottle!!! LOL

C-B

Zuhair

unread,
Dec 2, 2015, 1:59:24 AM12/2/15
to
Provided that Variable symbols in quantifier strings (i.e., of the form Ex and Ax) not to be replaced by constant symbols.
Zuhair

Zuhair

unread,
Dec 2, 2015, 2:22:53 AM12/2/15
to
Oh yes there are lots of them if not most of them are not closed
Over the hereditarily finite world, but first you need to know what is
Meant by closure here, a property Q(y,x1,...,xn) would be closed over
The set HF if the following condition is met

For all x1 in HF ... For all xn in HF [for all y (Q(y,x1,..,xn) -> y in HF)]

Now I'll provide you with an example of a property that is not closed
Over HF, take the property x1 in y so here you see that the following is not
True

For all x1 in HF [for all y (x1 in y -> y in HF)]

Since HF itself fulfills x1 in y for any x1 that is hereditarily finite but
HF is itself of course not hereditarily finite.

Zuhair

Zuhair

unread,
Dec 2, 2015, 2:57:35 AM12/2/15
to
Ok what I meant by generalization is that the closure statement would still hold when relativized to the
Class V of all sets, let me recall the definition of closure of a property Q over a class S,
This is:

Define: Q is closed over S iff
For all x1 in S .. For all xn in S [for all y (Q(y,x1,..,xn) -> y in S)]

Now we say that a property Q would generalize from HF to V iff
Q closed over HF -> Q is closed over V

Of course V is the class of all sets, while HF is the class of all hereditarily finite sets.

Unfortunately not all properties can generalize from HF to V. Thats why I adopted the
Restriction of existential equivalence on properties that can generalize from HF to V.

Hope that helps

Zuhair

Zuhair

unread,
Dec 2, 2015, 5:18:37 AM12/2/15
to
See my earlier two messages in which I've explained what is meant by closure of a property Q over a set S, and what is meant by generalizing a closing property over HF to be a closing property over V, which is simply denoted as generalizing from HF to V. However here I'll address a third question of yours, that you've asked about in your replies in this thread and that is:


Which properties close over HF yet cannot close over V?

I'll give two examples:

Q(y,x) <-> for all z (z in y <-> Exist k (k is infinite & k in x & k subset_of z))

Now clearly when x is hereditarily finite then y is empty and thus y is hereditarily finite and so Q closes over HF. However some x that is not hereditarily finite we may have an element that is infinite and by then y would be the class of all supersets of infinite elements of x, now y cannot be a set in this case because otherwise its union would be the set of all sets
which is contradictive.

Another similar example:

Q(y,x) <-> for all z (z in y <-> for all s (s is finite ^ s=x -> z={s}))

Now clearly for every x in HF we have y={{x}}, thus y in HF, so Q closes over HF.

But can Q close over V, the answer is to the negative, why?

Because take x in V and x is infinite then clearly y becomes V, so if Q close over V then this mean that V in V, i.e. V is the set of all sets which is a contradiction.

If we examine closely both of those examples we'll see problems emerged because some subformulas of the formula defining property Q when their parameters are relativised to HF won't hold of any class but when their parameters are relativised to V then they hold of some classes (like with the first example), and also because of the opposite scenario where some subformulas of the formula defining property Q when their parameters are relativised to HF would hold of some classes but when their parameters are relativised to V they won't hold of any class (like with second example).

To fix that I added the restriction that in order for a property Q that closes over HF to generalize to V (i.e. also close over V), then the above situation must not raise.

After that I saw that in order to prove replacement we need to check Q against its elevated form Q+ (the formula Q but with V replacing each occurrence of HF) and not just against itself with varying relativization from HF to V.

So in nutshell if S is a sentence describing closure of a property Q over HF
and if Q is proved to be existentially equivalent to its elevated form Q+, then

S -> S+

i.e. the truth of S implied the truth of its elevated form.

Zuhair



Zuhair

unread,
Dec 2, 2015, 5:22:40 AM12/2/15
to
I concentrate on mathematical logic, and did read a lot of it over the years,
the problem is that I barely find time.

Zuhair

Zuhair

unread,
Dec 2, 2015, 5:27:35 AM12/2/15
to
On Wednesday, December 2, 2015 at 6:35:01 AM UTC+3, Charlie-Boo wrote:
I need to say something here, I do know that your (i.e.; C-B) questions are very sensible, and I quite frequently just give the formalizations without much explanation, and this is a main drawback of my posts, I'm surely guilty of that. The problem is that I barely have the time to do the whole work, but I'll answer when asked.

Zuhair

Charlie-Boo

unread,
Dec 2, 2015, 7:21:19 AM12/2/15
to
Hi Zuhair,

Always a pleasure to see interesting ideas from those so dedicated to topics of interest to this forum. Are you open to suggestions and critique?

1. Does this contribute to any existing problem that has been identified regarding set theory or for that matter mathematical logic in general?

2. Can you formally define Hereditarily Finite Set i.e. without use of "etc." ?

3. Do you know of any rules that are not closed over those Hereditarily Finite Sets that provably exist in ZF?

Regards,

C-B

On Saturday, November 21, 2015 at 1:59:13 PM UTC-5, Zuhair wrote:
> Here I'll post this principle in full, just in case the link won't work. A link to this full work is presented below:
>
> The extensional well founded hereditarily finite set (abbreviated as hereditarily finite sets in the rest of this account) realm appears to be the most natural set realm, and so if we can figure out some way of generalizing some kinds of results from it to the whole realm of sets, then this might be of help in both understanding sets and possibly guides derivation of some stronge set principles that have a natural look.
> The naive idea is that some properties that are closed over the class of all hereditarily finite sets would also close over the class of all sets. We need to define a theory that helps us decide on some of these properties.
> To tackle this I'll define a notion of "elevation" on formulas:
> A formula Q+ would be called an elevated formula of Q if and only if Q+ is obtained from just replacing each occurrence of "HF" in Q by V, where HF is the symbol given to the class of all hereditarily finite sets, and V is the symbol denoting the class of all sets.
> Now the development is to define a notion of "existential equivalence" between formulas Q and Q+ as follows:
> Q is existentially equivalent to Q+ <-> for every subformula pi(y,x1,..,xn) of Q: Ax1 e HF,.., Axn e HF[Ey (pi(y,x1,..,xn))] <-> Ax1 e V,.., Axn e V [Ey (pi+(y,x1,..,xn))].
> Where n is the total number of parameters in pi.
> (notation: "A" denotes "for all", while "E" denotes "exists", and "e" denotes membership)
> In English every subformula pi of Q with all of its parameters being relativised to hereditarily finite sets must hold of an object if and only if its elevated form pi+ with all of its parameters being relativised to sets must hold of an object.
> HF is defined as the union of the intersectional class of all power-inductive classes (classes containing the empty set among their elements, that are closed under existence of power sets).
> I'll denote existential equivalence by "<-E->".
> My holding assumption is that existentially equivalent formulas can generalize results from the hereditarily finite set realm to the whole realm of sets.
> So to formally capture that, we write:
> Principle of Generalization: for n=1,2,3,..; if Q(y,x1,..,xn) is a formula in which only y,x1,..,xn occur free, then:
> (Q <-E-> Q+) & (Ax1 e HF .. Axn e HF [Ay (Q(y,x1,..,xn) -> y e HF)]) -> (Ax1 e V .. Axn e V [Ay (Q+(y,x1,..,xn) -> y e V)])
> is an axiom.
> Now this principle when added to Extensionality, Impredicative class comprehension of MK, and an axiom of existence of a power-inductive class and an axiom of infinity, then the result is a theory that can interpret ZF over the realm of sets (members of classes) of it.
> A nice corollary of this is that any formula using no more than three subformulas that is closed on the hereditarily finite set realm would also close on the whole realm of sets, and just using those formulas one can prove all axioms of Zermelo set theory "Z".
>
> EXAMPLES:
> To run an example of this method lets try to prove Singletons.
> So here we take Q(y,x) to be
>
> Az (z e y <-> z=x)
>
> Now for this case the formula is itself its elevated form since
> it contains no HF symbol, and so all of its subformas are their elevated
> forms.
>
> Now we check the subformula z=x
> first take x to be the paramter and check whether
> Ax e HF Ez (z=x) <-> Ax e V Ez (z=x)
> which is true.
>
> Now take z to be the paramter and check whether
> Az e HF Ex (z=x) <-> Az e V Ex (z=x)
> Which is true.
>
> Now we check the subformula z e y:
> Az e HF Ey (z e y) <-> Az e V Ey (z e y)
> Ay e HF Ez (z e y) <-> Ay e V Ez (z e y)
> which are true.
>
>
> Now we check the formula z e y <-> z=x:
> Az,x e HF Ey (z e y <-> z=x) <-> Az,x e V Ey (z e y <->z=x)
> Az,y e HF Ex (z e y <-> z=x) <-> Az,y e V Ex (z e y <->z=x)
> Ay,x e HF Ez (z e y <-> z=x) <-> Ay,x e V Ez (z e y <->z=x)
> which are true.
>
>
> At last we need to check the formula: Az (z e y <-> z=x) itself:
> Ax e HF Ey (Az (z e y <-> z=x)) <-> Ax e V Ey (Az(z e y <-> z=x))
> Ay e HF Ex (Az (z e y <-> z=x)) <-> Ay e V Ex (Az(z e y <-> z=x))
> which are true.
>
> So Q is existentially equivalent to its elevated form.
>
> So we can apply the generalization principle, and since we have:
>
> Q <-E-> Q+ & Ax e HF: Ay [Az(z e y <-> z=x) -> y e HF]
>
> then it follows
>
> Ax e V Ay [Az(z e y <-> z=x) -> y e V]
>
> which is Singletons!
>
> Another example is to prove Separation:
> So Q would be the formula Az (z e y -> z e x)
> The checks are:
> Az e HF Ex (z e x) <-> Az e V Ex (z e x)
> Ax e HF Ez (z e x) <-> Ax e V Ez (z e x)
> Same checks would apply to z e y
> Az,y e HF Ex (z e y -> z e x) <-> Az,y e V Ex (z e y -> z e x)
> Az,x e HF Ey (z e y -> z e x) <-> Az,x e V Ey (z e y -> z e x)
> Ax,y e HF Ez (z e y -> z e x) <-> Ax,y e V Ez (z e y -> z e x)
> And at last:
> Ax e HF Ey Az (z e y -> z e x) <-> Ax e V Ey Az (z e y -> z e x)
> Ay e HF Ex Az (z e y -> z e x) <-> Ay e V Ex Az (z e y -> z e x)
> Clearly all above checks hold. And since we have:
> Q <-E-> Q+ & Ax e HF: Ay [Az(z e y -> z e x) -> y e HF]
> Then by Generalization principle it would follow that:
> Ax e V: Ay [Az(z e y -> z e x) -> y e V]
> Which is Separation.
>
> Zuhair
>
> For clearer veiw see:
> https://sites.google.com/site/zuhairaljohar/the-generalization-principle

Charlie-Boo

unread,
Dec 2, 2015, 7:30:13 AM12/2/15
to
That is very thoughtful of you, Zuhair.

Have you heard of the expression "Garbage in, garbage out" (a take on "First in, first out" lists)? One instance is when a user (or even an analyst) presents a computer programmer with a description of a new software application that is ill defined and of no apparent value. Can you sympathize with the programmer who would rather continue work on the specifications rather than begin work on implementing them?

But still, let us all realize and not forget that simply having an interest and devotion to Mathematical Logic is the bulk of the elusive requirements for being a productive member of the SCI.LOGIC community.

C-B

Zuhair

unread,
Dec 2, 2015, 8:53:02 AM12/2/15
to
Yes the property "hereditarily finite" is definable without the need using "etc"

Also the method might yield a solution to finding natural extensions of ZF

And yes there are rules in ZF that are not generalizations of properties closed on HF,
The obvious example is axiom of infinity. Also ZF proves existence of the set of
All sets that are hereditarily sub-numerous to x and that rule cannot
Be seen as a generalization from HF. That's why infinity was aximatized here.
The theory presented in my website does interpret all of ZF rules.

Zuhair

Ross A. Finlayson

unread,
Dec 2, 2015, 12:08:46 PM12/2/15
to
It is similar to forcing, box/circle,
univalency, and sweep. In fact these
are very similar notions about trans-
finite Dirichlet (as forcing is) and
also compactness of the naturals.

Zuhair

unread,
Dec 2, 2015, 12:25:17 PM12/2/15
to
There is a clear purpose behind this methodology, namely that we want
to breed axioms for set theory and set theory in turn would serve to found mathematics. Now if we view ZF as stemming from generalizing closed properties over HF to the whole of V, then we can develop generalization principles that might help guide development of strong set principles that have a natural look, and thus naturally extending ZF.

Zuhair

Charlie-Boo

unread,
Dec 2, 2015, 9:33:20 PM12/2/15
to
On Wednesday, December 2, 2015 at 8:53:02 AM UTC-5, Zuhair wrote:
> Yes the property "hereditarily finite" is definable without the need using "etc"

Obviously. So that was not my question. My question was whether or not you can define it without etc. since you never did (I haven't read more than 2 or 3 of these posts - sorry if I'm wrong on that!) It is easily defined without etc if one has a tiny bit of skill in logic. Can you define it without etc? Wouldn't that make for a better presentation ("etc" can be ambiguous)?

> Also the method might yield a solution to finding natural extensions of ZF
>
> And yes there are rules in ZF that are not generalizations of properties closed on HF,
> The obvious example is axiom of infinity.

Infinity is not a generalization of any property because it is not a property of sets. It is the statement that a certain set exists. It doesn't say anything about the other sets.

In other words, what's the difference between the statement that "infinity is closed over ZF sets" and "infinity is closed over HF sets." or "infinity is closed over sets both HF and in ZF."? There is none, because the other sets play no role in infinity. It is not a property of the class (or whatever) of all sets.

Zuhair, I don't think you really understand what you're doing. Do you see the difference between infinity and the rules (axioms) in your examples?

I don't think there is any actual rule that is not closed over HF sets. Only an artificial one that isn't really a property of sets could violate that.

Can you see why? What would be an actual property of a class of sets that isn't closed over the sets that are both HF and in ZF?

I would also like to discuss the fundamental flaw in how you present your ideas. Programming language committees sometimes make the same mistake. How about a new thread where you ask for praise and criticism on you work and its presentation - good idea? Or are you only interested in impressing others and especially yourself? I'd like to hear that about my occasional spurts of posts (which occur when I'm itching to get rowdy) so feel free to include me in as a target, ok?

All the best,

C-B

Charlie-Boo

unread,
Dec 2, 2015, 10:06:31 PM12/2/15
to
First let's at least correctly formalize what you're saying (or trying to say.)

You are talking about functions over sets. A function is closed over a set if when its inputs are in the set then its output (value) is in the set. Some axioms of Set theory are of the form (all A)(exists B)... and are thus functions in effect. The function takes A and maps it to a B. Of course, there in general may be more than one B per A, but that's not occurring so that problem so far hasn't occurred.

Infinity is not of the form (all A)(exists B)... but rather is of the form (exists A)... . It is a constant, a degenerate function.

So you can't ask your question of every axiom of Set Theory. It doesn't apply to the infinity axiom.

Ok? (Waiting for your thread asking for help where we can clean up your ill-conceived ideas.)

C-B

On Wednesday, December 2, 2015 at 8:53:02 AM UTC-5, Zuhair wrote:

Virgil

unread,
Dec 2, 2015, 11:02:28 PM12/2/15
to
In article <de1c5dbd-40c9-49bf...@googlegroups.com>,
Charlie-Boo <shyma...@gmail.com> wrote:

> First let's at least correctly formalize what you're saying (or trying to
> say.)
>
> You are talking about functions over sets. A function is closed over a set
> if when its inputs are in the set then its output (value) is in the set.
> Some axioms of Set theory are of the form (all A)(exists B)... and are thus
> functions in effect. The function takes A and maps it to a B. Of course,
> there in general may be more than one B per A, but that's not occurring so
> that problem so far hasn't occurred.
>
> Infinity is not of the form (all A)(exists B)... but rather is of the form
> (exists A)... .

It IS of the form
(there exists an A and for each A there exists another A)
>
--
Virgil
"Mit der Dummheit kampfen Gotter selbst vergebens." (Schiller)

Zuhair

unread,
Dec 3, 2015, 2:26:17 AM12/3/15
to
On Thursday, December 3, 2015 at 5:33:20 AM UTC+3, Charlie-Boo wrote:
> On Wednesday, December 2, 2015 at 8:53:02 AM UTC-5, Zuhair wrote:
> > Yes the property "hereditarily finite" is definable without the need using "etc"
>
> Obviously. So that was not my question. My question was whether or not you can define it without etc. since you never did (I haven't read more than 2 or 3 of these posts - sorry if I'm wrong on that!) It is easily defined without etc if one has a tiny bit of skill in logic. Can you define it without etc? Wouldn't that make for a better presentation ("etc" can be ambiguous)?


HF is the intersection of all power inductive classes.

A power inductive class is a class closed under power that have the empty set among its elements, formally this is

Define: x is power inductive <-> 0 in x & for all m in x Exist n in x (n=P(m))

where "P" stands for power.

so x is hereditarily finite <-> x in HF.

Zuhair

unread,
Dec 3, 2015, 2:41:38 AM12/3/15
to
On Thursday, December 3, 2015 at 6:06:31 AM UTC+3, Charlie-Boo wrote:
> First let's at least correctly formalize what you're saying (or trying to say.)
>
> You are talking about functions over sets. A function is closed over a set if when its inputs are in the set then its output (value) is in the set. Some axioms of Set theory are of the form (all A)(exists B)... and are thus functions in effect. The function takes A and maps it to a B. Of course, there in general may be more than one B per A, but that's not occurring so that problem so far hasn't occurred.


It did occur, this occurred about the property "subclass":

You see it is closed over HF since we do have:

For all x in HF (for all y (y C x -> y is hereditarily finite))

where C denotes 'subclass relation' defined in usual manner.

Now for each input x that is non empty we do have more than one output here is for any non empty object the number of subclasses of it is more than one.

What I meant by the word "property" is simply an n+1_ary relation Q(y,x1,..,xn)
where x1,..,xn are the inputs to that relation and y is the output, but y
is not necessarily unique per each particular string of inputs, so in the above
example we take Q(y,x1) to be "for all z (z in y -> z in x1)" which is of course y C x1, now for each object substituting x1 that is not an empty set
you do have multiple outputs substituting y.

There are many properties (i.e. n_ary relations) that are not closed over the set HF of all herediarily finite sets, of course there are and I gave a simple example that of x1 in y, since not every class y having a hereditarily finite object x1 as element would necessarily be hereditarily finite, that is clear one example is HF itself.

IF you want a property in your sense (of the function form for all A exist B ..) that do not generalize from HF that is proven in ZF, I've already gave you one, and that was the property:

For all A Exist B (for all y (y in B <-> y is hereditarily subnumerous to A))

now this is a functional property in your sense that is proven in ZF and yet
cannot be conceived as a generalization from the hereditarily finite world.

I think you have some misunderstanding of the word "property" here which I only
meant it to be an n_ary relation, just that, it need not be a function, it need not have the specification you have in your mind.

Zuhair

Julio Di Egidio

unread,
Dec 3, 2015, 8:15:23 AM12/3/15
to
On Wednesday, December 2, 2015 at 3:20:05 AM UTC, Charlie-Boo wrote:
> On Tuesday, December 1, 2015 at 9:33:58 PM UTC-5, Ross A. Finlayson wrote:
<snip>
> > How about instead we work on the Hilbert Program together.
>
> In what sense can we work on Hilbert's Program since it is unattainable?

Fair objection...

Julio

Virgil

unread,
Dec 3, 2015, 11:43:03 AM12/3/15
to
In article <1ffa8a1e-dbed-4af1...@googlegroups.com>,
What seems unattainable to putzers like Ross and Julio may well be
attainable by actual mathematicians.

Alan Smaill

unread,
Dec 3, 2015, 12:45:03 PM12/3/15
to
Virgil <VIR...@VIRGIL.com> writes:

> In article <1ffa8a1e-dbed-4af1...@googlegroups.com>,
> Julio Di Egidio <ju...@diegidio.name> wrote:
>
>> On Wednesday, December 2, 2015 at 3:20:05 AM UTC, Charlie-Boo wrote:
>> > On Tuesday, December 1, 2015 at 9:33:58 PM UTC-5, Ross A. Finlayson
>> > wrote:
>> <snip>
>> > > How about instead we work on the Hilbert Program together.
>> >
>> > In what sense can we work on Hilbert's Program since it is
>> > unattainable?
>>
>> Fair objection...
>>
>> Julio
>
>
> What seems unattainable to putzers like Ross and Julio may well be
> attainable by actual mathematicians.

Plenty of folk think that Hilbert's programme is unattainable,
given Goedel's results:

http://plato.stanford.edu/entries/hilbert-program/

--
Alan Smaill

Virgil

unread,
Dec 3, 2015, 1:00:23 PM12/3/15
to
In article <fwelh9b...@foxtrot.inf.ed.ac.uk>,
But I have come to the point of not accepting anything claimed by JDE o
or WM or AP or JG without firm external evidence of its validity!

Justin Thyme

unread,
Dec 3, 2015, 2:55:52 PM12/3/15
to
Charlie-Boo wrote:
> On Sunday, November 29, 2015 at 9:05:33 PM UTC-5, Zuhair wrote:
>> It makes sense but it is trivial
>>
>> Zuhair
>
> Whether it is trivial or not, you haven't done it. It is just a
> bunch of formalisms with no examples of how it accomplishes anything
> - very typical of you. Have you read my posts? I prove actual
> theorems about incompleteness, give shorter proofs than are
> published. These are real results. A bunch of formalisms and an
> occasional claim that it represents something or includes something
> doesn't mean it has any value. It is "a solution in search of a
> problem."

Who has peer-reviewed publications in well-known journals, you or Zuhair?


--
Nam Nguyen: *As we speak*, MS and NN would understand what "blue" would
mean.
Martin Shobe: No I don't. You could mean the color, the feeling, or
given your past history, something entirely different.
Nam Nguyen: Go and get fucked.

sci.logic 24/10/2015

Ross A. Finlayson

unread,
Dec 3, 2015, 9:53:30 PM12/3/15
to
A system with "not finitely-many" axioms,
eg infinity-many or _ZERO_, is not subject
to Goedel's exclusive incompleteness or
inconsistency of a theory strong enough
for arithmetic.

The Null Axiom Theory or Void Axiom Theory
is this way.

Julio Di Egidio

unread,
Dec 4, 2015, 5:16:49 AM12/4/15
to
On Friday, December 4, 2015 at 2:53:30 AM UTC, Ross A. Finlayson wrote:
> On Thursday, December 3, 2015 at 5:15:23 AM UTC-8, Julio Di Egidio wrote:
> > On Wednesday, December 2, 2015 at 3:20:05 AM UTC, Charlie-Boo wrote:
> > > On Tuesday, December 1, 2015 at 9:33:58 PM UTC-5, Ross A. Finlayson wrote:
> > <snip>
> > > > How about instead we work on the Hilbert Program together.
> > >
> > > In what sense can we work on Hilbert's Program since it is unattainable?
> >
> > Fair objection...
>
> A system with "not finitely-many" axioms,
> eg infinity-many or _ZERO_, is not subject
> to Goedel's exclusive incompleteness or
> inconsistency of a theory strong enough
> for arithmetic.

But such a system has hardly anything to do with Hilbert's program, whose very justification is rooted into the use of essentially finitary reasoning only. Anyway, and more importantly IMO, Hilbert's program, the first as well as the second, cannot but fail because it is reductionism that is a failure, in fact just good for our cultures and politics of enslavement...

For example, Hilbert 1928, "Die Grundlagen der Mathematik" (as quoted by the Stanford Encyclopedia article): "This formula game is carried out according to certain definite rules, in which the technique of our thinking is expressed. [...] The fundamental idea of my proof theory is none other than to describe the activity of our understanding, to make a protocol of the rules according to which our thinking actually proceeds", but the mind is not just the brain, man is not just a machine, and our understanding cannot just be reduced to "cognitive processes". And so on.

> The Null Axiom Theory or Void Axiom Theory
> is this way.

But only you know what that is... :)

Julio

Rupert

unread,
Dec 5, 2015, 6:25:36 AM12/5/15
to
On Tuesday, December 1, 2015 at 9:01:14 PM UTC+1, Zuhair wrote:
> On Monday, November 30, 2015 at 7:31:45 PM UTC+3, Rupert wrote:
> > On Sunday, November 22, 2015 at 9:34:24 PM UTC+1, Zuhair wrote:
> > > On Sunday, November 22, 2015 at 1:26:11 AM UTC+3, Rupert wrote:
> > > > On Saturday, November 21, 2015 at 7:59:13 PM UTC+1, Zuhair wrote:
> > > > > Here I'll post this principle in full, just in case the link won't work. A link to this full work is presented below:
> > > > >
> > > > > The extensional well founded hereditarily finite set (abbreviated as hereditarily finite sets in the rest of this account) realm appears to be the most natural set realm, and so if we can figure out some way of generalizing some kinds of results from it to the whole realm of sets, then this might be of help in both understanding sets and possibly guides derivation of some stronge set principles that have a natural look.
> > > > > The naive idea is that some properties that are closed over the class of all hereditarily finite sets would also close over the class of all sets. We need to define a theory that helps us decide on some of these properties.
> > > > > To tackle this I'll define a notion of "elevation" on formulas:
> > > > > A formula Q+ would be called an elevated formula of Q if and only if Q+ is obtained from just replacing each occurrence of "HF" in Q by V, where HF is the symbol given to the class of all hereditarily finite sets, and V is the symbol denoting the class of all sets.
> > > >
> > > > Let's analyse this further. You said the language of the theory was the mono-sorted first-order language of set theory. Are you saying that you are using a version of this language such that an abstraction term can occur in an unabbreviated formula? Or are you assuming some effective procedure whereby given an unabbreviated formula Q we can tell whether or not there is some abbreviated version of it of an appropriate kind in which an abstraction term which could be abbreviated by "HF" occurs?
> > >
> > > First of all the language is mono-sorted first order language of CLASS theory, all variable symbols stand for CLASSES.
> > >
> > > Of course the symbols HF and V are "defined" symbols, and so formulas using them are of course "abbreviated formulas" in the usual sense much as 0 is a defined symbol representing the empty set, so when we way for example
> > > ~Exist x. x e 0, this is in reality an abbreviation for
> > > for all k (for all y (y e k <-> ~y=y) -> ~Exist x. x e k).
> > >
> > > To answer your second question, if I understood it, then the answer is NO.
> > > More explicitly: I'm NOT assuming some effective procedure whereby given an unabbreviated formula Q we can tell whether or not there is some abbreviated version of it of an appropriate kind in which an abstraction term which could be abbreviated by "HF" occurs?
> > >
> > > The occurrence of HF in the formula Q(y,x1,..,xn) that I was speaking about in the generalization scheme means that Q is an abbreviated formula since HF is an abbreviation.
> >
> > All right then. So Q and Q+ are abbreviated formulas. Then you go on to speak of a subformula of Q. Does that mean a subformula of the unabbreviated version of Q, or if not then what is meant by a subformula of an abbreviated formula exactly?
>
> Q is an abbreviated formula only if it contains the symbol HF or the symbol V
> in it otherwise the other symbols in Q are all non abbreviated. Now if Q doesn't contain those symbols then it is exactly Q+. What is meant by a subformula of Q is a substring of Q the meets the qualification of a formula. This is decidable and it can be recursively defined by incorporating the symbols V and HF in the formula formation rules, so we have:
>
> for any variable symbols xi,xj:
> xi e xj is a formula
> xi=xj is a formula
> xi e HF is a formula
> HF e xi is a formula
> xi=HF is a formula
> HF=xi is a formula
>
> Those are the 'atomic' formulas.
>
> Now if phi and pi are formulas then phi connective symbol pi
> is a formula.
>
> if phi(x) is a formula in which x occurs then Ax(phi) is a formula
> and Ex(phi) is a formula
>
> If phi is a formula in which HF occurs then replacing V instead of HF
> yields a formula (which is phi+).
>
> Those were the formation rules of formulas.
>
> From those rules then it is clear that if we are presented with a formula phi then we can totally decide on where a string of symbols pi is a subformula of phi or not. We simply take the set of all atomic subformulas of phi and then formulas built from those atomic subformulas along the above formation rules are totally decidable and of course it is decidable whether a string is a substring of a formula or not. So a substring of a formula Q (whether Q contains the abbreviated symbols HF and V in it or not) that is a formula
> along the above recursive formation rules, is what is meant by a subformula of Q.

You write

Q is existentially equivalent to Q+ <-> for every subformula pi(y,x1,..,xn) of Q: Ax1 e HF,.., Axn e HF[Ey (pi(y,x1,..,xn))] <-> Ax1 e V,.., Axn e V [Ey (pi+(y,x1,..,xn))].

The quantifiers Ey are not meant to be bounded by HF and V respectively?

Zuhair

unread,
Dec 5, 2015, 12:59:31 PM12/5/15
to
The quantifier Ey is NOT bounded.

Dear Rupert, please see my latest update on this at my latest posting of mine to this Usenet titled: a near naive explanation for the generalization principle, present at:

https://groups.google.com/forum/#!topic/sci.logic/sJBBL4LWqJE

I think it clarifies matters.

Zuhair

Zuhair

unread,
Dec 5, 2015, 1:03:00 PM12/5/15
to
Also I'll refer you to my website page of the naive explanation, i think it is better readable.

https://sites.google.com/site/zuhairaljohar/the-generalization-principle/naive-explanation-of-the-generalized-principle


Zuhair

Ross A. Finlayson

unread,
Dec 5, 2015, 1:09:26 PM12/5/15
to
No, it's the same as naive theory that is
consistent and complete.

Here, it's just written out why that is so
for then usual useful tools for formal
methods with rigor for consistency and
completeness for arithmetic and what follows,
including for some a strong and concrete
Mathematical Platonism toward a "mathematical
universe hypothesis" (thus scientific).

It is a reductionist course, to final
cause as first principles, here as the
zero-eth principle of dually-self-infra-
consistency.

Reply all
Reply to author
Forward
0 new messages