Proper Treatment of Set-Like Functions contra DC Proof

[Mostowski Collapse]

I just stepped over a nice proper treatment of Set-Like functions.
In DC Proof often set theory proofs are carried out using FOL
function symbols f and the FOL application f(x).

This might on the surface match what we find in text books.
But when we approach a text book with a set theory foundation,
we need to translate the surface f(x) away from FOL.

One way is to use f[x]. This guy has a charming "macro", which
allows to define the notation _ [ _ ]:

f[x] == CHOOSE y : <<x, y>> \in f

It looks to me that the notation _ [ _ ] is a FOL binary function
symbol, I would call it "apply". Which gets expanded by his "macro" into:

CONSTANT _ [ _ ]
AXIOM \A f : \A x : (\E y : <<x,y>> \in f) => <<x,f[x]>> \in f

I am not sure whether its optimal. It caters for that apply will
be of arity 2, and both the first argument f and the second argument
x will be sets. But as a FOL function symbol, apply will still yield a

value in a model when x is outside of the domain of f. But neverheless
it doesn't interfer with the FOL function symbols and its syntax f(x), and
it doesn't quantify over FOL function symbols.

See also:
https://github.com/VincentSe/HilbertProofs

[Ross A. Finlayson]

Heh, "proper".

[Mostowski Collapse]

Ha Ha, room-temperature IQ knobhead.

Ross A. Finlayson schrieb am Dienstag, 15. Dezember 2020 um 13:59:59 UTC+1:
> Heh, "proper".

[Ross A. Finlayson]

Yeah, I suppose the medium is pretty dead.

So long, sci.logic! I'll be mining you for quotes!

Basically my goal is to convince a FredJeffries that
a triangle has a computable area, and a JimBurns
that flying rainbow sparkle ponies have at least
two models: I'm pretty well convinced of it, myself.

Heh: proper.

Good luck with your box, there, Burse. Good luck.

George, et alia, ..., all I really have for you at this
point is what I've written here is _sincere_.

Well good luck then and hopefully when there's news
on sci.logic it will actually be news.

Au revoir! (Yeah, I'm simply amused and might go
back to a usual more usual comments.)

Auf wiederhoeren! So long!

[Mostowski Collapse]

Your vessel, the flying rainbow sparkle ponies?
Juuuhuuuhuuu Ross the Floss, word salad icarus.

LoL

[Ross A. Finlayson]

Heh, Mostowski Collapse.

Mostowski of course along with Levy and Skolem
make for usual completeness results in projection.

It's a usual enough atomism.

I made it clear what now foundations, is so usual
and anonymous enough, already, applications abound.

I.e. at the end no different than any other sound theory.


I guess the entire point of "usenet dead, news at 11",
since of course some twenty years what that
already "the finalizer 'usenet is dead', is dead".

I.e., why this medium is so poor and basically
full of open access commons the usenet -
then I fell on it what for mathematics, logic,
then for physics, it's probably natural.

Or, maybe, "was".

I saw uncountable foundations as a huge opportunity.

I suppose it's not an HTTP port what NNTP is pretty usual.

This is all left for to be found.

Looking at sci.physics.relativity I'm not really wondering
about it, the usual today's picture of GTR and QM together,
in a field theory then for example with the Standard Model,
for kinetics in particles, that electro-weak is hadronic here
for the magnetic flux, and, optical flux, besides a unified field
theory there is of course all the field of dynamics. I.e., that
"the" unified field theory, here of the thermo as for dynamics
in kinetics, besides inertia, of course in charge or flux in potential,
about electromotive and electrostatic and magnetomotive,
"torque is static", is of course usually its wave theory.

I.e. "what's today's picture of GTR and QM together", it's a
unified picture, for each of those as sharing classical equilibrium.

I.e. the constants are as under the universe is "static",
while of course it's all altogether under dynamics, as static.

Then my fall gravity fits in quite well and all neatly altogether
in classical equilibrium from fundamentals, including then
for a final notion of mechanism, as out from under that the
particle's mass, or moment, gravitates, that instead all its
contribution, fundamentally, is geometrically unified in its
models of other forces.

I.e., there is one.

This I find easier to satisfy first, then fill in with derivations
proof and simple, besides whether it's not satisfying at all
if not fully satisfied already, the derivations, here that the
descriptive in properties, suffices, only for terms.

I.e. it much doesn't meet the requirements of a "scientific
theory", though in the usual tendencies it proves in all models.

Which would be never wrong....


Thanks reading, it is an outlet.

The usual ideas are writing into the proof systems with
reconciliations and apologetics, disclaimers, the slate
into the proof systems, and notes of fundamental results,
even just archival and report-following.

Modernizing the medium: standards.

Then, the slate is sound making for sincere modern classical
mathematics, modern classical as after modern and classical
again, as super-classical!, what satisfies and suffices the classical,
modern, and super-classical requirements of modern theory.

(Modern classical theory.)



"Proper".

Heh, "Set-Like" functions, this is a function theory with
Cartesian and Cantorian sets already - modern,
that Spinoza and Duns Scotus are modern classical already,
classical, that the Cartesian is classical and for the "Set-Like",
which is otherwise already "modeled by set theory", these
of course fall out of set results set in the frames under their
properties, a non-Cartesian with no "entire space of functions",
combinatorially under pair-wise instead of infinite[-wise] union,
"pair-wise or all-wise", there is Des Cartes' classical is both,
so being "Set-Like" besides a usual "set model, of a function".

Then, in something so usual as forward inference
that would be the descriptive as proper.

I.e., the "descriptive" is presumed to suffice, as to how it's
satisfied, soundness in guarantee, what's assumed to suffice,
being fully descriptive, as matter-of-fact.

So, it's non-logical and basically made strong in a system of
following usual non-circular normal syllogistic rules.

Or, "always-not-not-circular", that "ex falso" has _not_
being non-circular, instead of _any_ non-circularity or
non-linearity usually enough.

I.e., it's to be assumed under the system how soundness
always holds, too. The guarantees are built here that the
set-like is proper thus suffices fully for the descriptive.

This is that the descriptive includes "function theory",
"set theory", these are for example about categories
and also types, categories as "fully descriptive" for he
types as "fully modeled", it is so though that categories
and types are so related, if not the "function theory"
and "set theory" are actually "above" as so "below"
the category and type theory and the descriptive.

Usually though the descriptive means for the set theory,
the constructive in the set theory what results from the
properties of the topology, where the combinatorial
would otherwise suffice, that the topological establishes
the combinatorial for the geometrical, as it would be more total.

That it suffices for the true theory to be total....


Burse, for the box in the box, put the vessel in the vessel.

I think that's good enough advice that in terms, is
what is results in terms, that suffice and to satisfy,
the "properties" of the box, and the "property" of the vessel.


This is far as I know "news" in logic.

[Mostowski Collapse]

Ha Ha, room-temperature IQ knobhead.

The longer the post, the more gibberish.

Ross A. Finlayson schrieb am Samstag, 19. Dezember 2020 um 20:14:40 UTC+1:
> ...look see, I can juggle with the word circular...
> ...look see, I can even name drop topology...
> ...look see, I even got a orgasm from my brain masturbation...

[Ross A. Finlayson]

I suppose this is as much for me as anybody else -
it's for me, though.

Yup, simple adherence to the charter, at least _seems_ good faith.

The circular bit, or "On Circularity", that seems most helpful.

It helps remind that deductive inference closes over conditions.

That the usual deductive and inductive inference, complement
each other thus closing, is for usual constructive means in referent.

Then it's a "Stoic Revival" for example that under means it's progress.

Having a "Stoic revival" then "all the way to question word",
makes most sense for performance with writing it out.

I.e., "performance of a limited means".

Heh, advising Burse's rhyming couplets,
the success of limited means has "name drop topology":
simpler in referent than the school in the name: "so easy".

That the "non-circular in forward inference, together",
makes for rotating means and the combination, composition,
simpler and easier together in adding terms, or not,
is part of an apparatus - the proof terms together.

The ascription of properties and transitive closure of
types so declared in the syllogistic, that types are abstract,
is for a neat small mechanism of deductive sanity.

Here "sanity" means more or less "sound", because it's "only logic".

The "deduction of sanity", besides of course "induction of sanity",
here is that the natural algebras of types over and under deduction,
that it's usual affirmatory types what establish conclusion, rel., data.

Which deductive elements and inductive elements both have....

So, it's not so hard to say that the gibberish, is elements.

This seems as simple as only having "question words solved"
instead of intensionality - for proof terms.

I.e., where the rules are written out that way first, the
quantifier ordering is "natural" insofar as it's "sound".

That the proof terms write....

Elements of proof then have these usual assumptions and conclusions.


Thanks though the comment on circular elements is profound.

"The Space of Words"

There are words....

This is almost looking like "ex falso veritas".

There's truth and modeling....

That the truth is the model not the model is the truth.

This is then that truth satisfies the model.

(I.e. to ascribe it properties under types,
making for soundness guarantee, truth
and its model.)

Of course, the model is still "its own truth",
there's no denying it only no affirming it.

Which truth does....


Well then readers I guess I could apologize,
if it's always sincere soundness guarantee,
agreeing all what's so is true.

For set theory and models of course or the
close and intimate application of sets, so defined,
as models, under interpretations of their parts,
in combinatorics and counting most regularly,
here of course is for whole monism besides,
counting parts besides, and sweeping or collecting
them.

I.e., "the usual ubiquitous success of set theory
and its applications in mathematics, makes for
why quantity and quality are under counting and
over collecting."

There's though that "counting" and "collecting"
are so direcly anti- or contra-, in terms, what for
example is not counted though collected, and in
terms of what's counted is not collected.

Looking this way to tag theorems with why they
apply via counting, for example, or via collecting,
when that is at all different, makes for the disjoint
space that collecting implies, about maintaining
"1/2" or the mean - that the collected is always
counted again, or not, and the counted is always
collected again. (Or not.)

Quantity is a quality.

Geometrically though all is quantity.

Here: of course, to define it in terms of quality,
geometry, descriptive set theory applied to topology
makes quality for geometry.

This is under type in theory - here "set-type".

set-type: type of a set (the type that a set has)
set-like: model of a set (eg category of a non-set class, a set)

For applying set theory then here of course is that the
proof terms: what out what exist in the models thus the
sets, that counting and collecting are in set-theoretic terms.

This then is usually applied directly to or from geometry.

Good luck!

Making foundations for applications helps to have for
example pure set theory as foundations, besides just for
example the self-implicit truth of any counting or after
the combinatorial: usual cases for inference.

Looking to really establish what in ten or twenty pages
makes a logic, agreeable in terms, starts for example
under types, in example under derivation of consequent.

That is, agreeable in terms, a logic, besides data and covention,
has that either there's all controversy at once or none - filling in
always the consequences the proof terms, themselves.

Then, "theoretical elements", here are pure as sets in type,
for example, making of course for why applications are
entirely closed themselves in their own semantics of course
under all the combined semantics, the space of combined semantics.

Then "semantics of theoretical elements" and "theory of semantic
elements" are not so different. Theoretical elements are constrained
to exist what maintain their affirmatory reference. This way adding
them is free: they're "intensionally pure" (or, where not, "wrong"),
theoretical elements to the theory. The theory of semantic elements
then has that semantics have their own theories, what might be true.
Then, to be extensionally pure, it's the constraint of the real theoretical
elements, what instead would be hypothetical elements (including
the falsified, as contradicting theoretical elements).

That the entire distinction is "non-logical applications are not
extensionally pure to a pure intensionality", the distinction between
"pure" and "applied", as that the "pure applied", is always hypothetical,
it's science.

That's at least pure, in theory.

When theories are pure enough to be generally applied,
those are facts in mathematics.

I.e., naive set theory is "pure" as an "application of set theory,
to set theory".

Goedel capstones the famous paradoxes of mathematical logic,
how there's a pure theory, in paradox. (Also usual deductive
consequences after axiomatizing the regularity of sets and
the regularity of the infinity of sets, or an inductive set.)

Then I put up my slate for the capstone that for the
elements of mathematical paradox, or counting and
collecting, makes for at least a monism, then what it
happens for the real character in continuity and the
geometry, that foundations of geometry are pure.

Then that though would be the geometry slate after
the countability slate and the quantification slate.

"A spiral space-filling curve founds a natural geometry...."



I wonder what Burse's "gibberish golem" by now makes
free gibberish - in rhyme.

Good luck, gibberish golem!

If you feed the golem a bit more of the reference gibberish,
I wouldn't be surprised it starts sounding closer and closer apart.

Here it's that there's a reference gibberish establishing a space
of words.

Including what proof terms are....

What with my three slates here for mathematics, suppose
the idea's that there is one, in usual terms, modern classical.

Or, ..., modern.


Good luck!

Countability, collection, and coordinate, in slate:
new classical modern, I didn't know they had one before,
mathematics as what it does.

Now I know there is one.

It's axiomatics of a usual sort up to Goedel then back down.

Basically this is about deductive closures over inductive totality.

What makes for free (i.e., free as sound, and free), inference.

Having these slates around then it's not so much
"can't do without them" as "can do with them",
the slates establishing countability, collection,
and coordinate, continuity in form.

For the classical....


Cantor Universe <- words, universe
Finlayson slate <- ORD <- numbers, universe
Finlayson slate
Finlayson slate
ZFC
Finlayson slate
Finlayson slate
Finlayson slate
Geometry
Euclid Universe <- points, universe

^- "sound" theory, universe

This has Euclid is classical and Cantor is modern.

ZFC with "regular infinity" (Cantor) and "regular ORD" (Cohen),
or rather for Zermelo-Frankel set theory for the regular and
Cantor's theorems, for the modern, and after Goedel and Cohen
for the independence of the Continuum Hypothesis to ZF, and ZFC,
this these days is called "modern", as, early to mid- 20'th century
and since.

Then of course the classical for technical logic includes in a usual
sense all the canon - here for example a "Stoic revival" as simply
that then this "modern classical" in terms generally equi-interprets,
soundly, what with the classical and modern and classical again:
new modern classical.

These days univalency is the usual suggestion after ZF(C) and
theories in types, in axiomatics in foundations. (Universal.)

[Mostowski Collapse]

Ha Ha, room-temperature IQ knobhead.

[Ross Finlayson]

''This seems as simple as only having "question words solved"
instead of intensionality - for proof terms. ''

More about question words ....