Order theory in foundations

[mitch]

This is the top post for a group of posts. Before
explaining the subject, note that there will be
two long (~300 lines) technical posts. These will
also be broken up into smaller pieces for those
with bandwidth or reader limitations.

There are issues surrounding the identity of
indiscernibles in the foundations of mathematics.
Traditional foundations denies it as a logical
principle. Currently, the HOTT community is
offering an alternative to traditional foundations.
This is attractive to mathematicians who do not
focus on traditional foundations. Many participants
in HOTT assert that the principle of identity of
indiscernibles is a logical principle. And, among
other things, the HOTT book discusses definitions
and a "rediscovering" of Frege's ideas.

For some time now, I have known of a specific
quote from Leibniz in which he describes his
own logic. He uses an order-theoretic analogy.
One of the subposts will contain this quote.

For comparison, there is a subpost from Aristotle
discussing parts and wholes. The mathematical
community is certainly aware that a system of
parts and wholes is interpretable as an order
relation. This is the system to which Leibniz
is referring when he uses the expression
"inversion".

With regard to the two long technical posts, one
might consider saving each to a file on the
local operating system and running a "diff" on
the files. What one will find is that they are
basically "cut-and-paste" copies of one another
whose only changes result from the exchange of
antecedent and consequent in one axiom. What I
have done is to reduce the statement of Leibniz
to the direction of a conditional.

With respect to terminology, I speak of "Fregean
object identity" and "Fregean concept identity".
These expressions are from his statements in
"Comments on Sense and Referents". The Fregean
concept identity is familiar from the axiom of
extension from set theory. As a defined identity,
it would be written as

AxAy( x :: y <-> Az( z in x <-> z in y ) )

The Fregean object identity is the "second-order"
form, and it coincides with the principle of
identity of indiscernibles when properties are
identified with collections. As a defined
identity, it would be written as

AxAy( x :: y <-> Az( x in z <-> y in z ) )


The files contain a short foreword to remind
readers that my logic is not first-order logic.

My treatment of identity distinguishes between
identity and indiscernibility. For a much
better account than I can give, consider
the section of "Relative Identity" in the
SEP link,

https://plato.stanford.edu/entries/identity-relative/#1

But, Deutsch is defining an indiscernibility
relation with respect to a model-theoretic
notion. My account is compatible with what
Quine did in "Set Theory and Its Logic". I am
considering how a defined identity that is "good
enough" really is not when the arguments against
the principle of identity of indiscernibles are
taken into account. I have presumed that those
arguments "support" the reasoning behind set
theorists deferring to predicate logic. But,
the axiom of extension is really just an instance
of the principle of identity of indiscernibles
specific to the language primitive,

AxAy( Az( z in x <-> z in y ) -> x = y )

That is, it utilizes a dyadic predicate to
warrant identity statements for use in the
logical calculus.

In Max Black's famous paper on the identity of
indiscernibles,

home.sandiego.edu/~baber/analytic/blackballs.pdf

you will find the antagonist making the following
assertion,

< begin quote >

"B. No, I object to the triviality of the
conclusion. If you want to have an interesting
principle to defend, you must interpret
'property' more narrowly -- enough so, at any
rate, for 'identity' and 'difference' not to
count as properties."

< end quote >

If you examine what I am doing with "identity"
and "apartness" in these files, you will see
that I am answering this challenge.

mitch

[mitch]

On 03/01/2017 05:23 PM, mitch wrote:

< snip >


The following passage from Aristotle is his account
of logic as a "part-whole" relation:

< begin quote >

"A's being included in B as a part in a whole
is the same as B's being predicated of every
A. We say that B is predicated of every A
whenever it is impossible to take any A of
which B is not said, and the same applies to
B's being predicated of no A."

Prior Analytics 24b28

Aristotle: Selections
Terrence Irwin and Gail Fine
Hackett Publishing, Indianapolis/Cambridge, 1995

< end quote >

Observe that the universal "every A" is
defined with respect to the impossibility of
producing a counterexample.

The same is true of its contrary "no A".

Also, the universal and its contrary differ
in that the contrary is symmetric because

( No A is B ) -> ( No B is A )

has no counterexamples. By contrast,

( Every A is B ) -> ( Every B is A )

has counterexamples.

The coordinatization of Aristotelian term
logic is such that a "species" is a part of
a "genus". That coordinatization, however,
is not based upon bifurcations,

< begin quote >

"Coordinates of the same genus are also said
to be simultaneous by nature. Those resulting
from the same division are said to be coordinate
to one another -- for instance, winged, footed,
and aquatic. These are from the same genus and
coordinate to one another; for animal is divided
into these -- into winged, footed, and aquatic --
and none of these is prior or posterior, but
such things seem to be simultaneous by nature.
Each of these -- winged, footed, aquatic -- might
be further divided into species; these species,
then, will also be simultaneous by nature, because
they are from the same genus by the same division."

Categories 14b34

Aristotle: Selections
Terrence Irwin and Gail Fine
Hackett Publishing, Indianapolis/Cambridge, 1995

< end quote >

To the extent that the identity of indiscernibles
is based upon the coordinatization of Aristotelian
term logic, it is based upon partition lattices.

mitch

[mitch]

On 03/01/2017 05:23 PM, mitch wrote:

< snip >

Leibniz clearly describes his own logic as inverting
the particular order of Aristotle's part-whole
relation. Although he does not mention Aristotle, his
description of the Scholastic account clearly
coincides with the substantiation hierarchy of
Aristotelian term logic. By the substantiation
hierarchy I refer to Aristotle's description of
individuals as primary substance. Species and
genus are secondary substance composed of
primary substance.

Here is the quote from Leibniz describing his
own understanding of his logic,

< begin quote >

"Two terms which contain each other but do not
coincide are commonly called 'genus' and
'species'. These, in so far as they compose
concepts or terms (which is how I regard them
here) differ as part and whole, in such a way
that the concept of the genus is a part and
that of the species is a whole, since it is
composed of genus and differentia. For example,
the concept of gold and the concept of metal
differ as part and whole; for in the concept of
gold there is contained the concept of metal
and something else -- e.g., the concept of the
heaviest among metals. Consequently, the
concept of gold is greater than the concept
of metal.

"The Scholastics speak differently; for they
consider, not concepts, but instances which
are brought under universal concepts. So they
say that metal is wider than gold, since it
contains more species than gold, and if we wish
to enumerate the individuals made of gold on
the one hand and those made of metal on the
other, the latter will be more than the former,
which will therefore be contained in the latter
as a part in the whole. By the use of this
observation, and with suitable symbols, we
could prove all the rules of logic by a calculus
somewhat different from the present one -- that
is, simply by a kind of inversion of it.
However, I have preferred to consider universal
concepts, i.e. ideas, and their combinations,
as they do not depend upon the existence of
individuals."

Elements of a Calculus

Leibniz Logical Papers: A Selection
G. H. R. Parkinson
Oxford University Press, New York, 1966

< end quote >

Since what I am interested in here is the expression
of order theory, let me emphasize the expression,

"..., simply by a kind of inversion of it."

in the fifth line from the bottom. He is saying that
the the relation between his "ideas" (linguistic
forms) and the quantitative interpretation which
grounds the modern notion of extensions may be
understood with respect to converse orders.

mitch

[mitch]

On 03/01/2017 05:23 PM, mitch wrote:

< snip >

This theory will use a non-eliminable identity
relation introduced by recursive definition and
an eliminable indiscernibility relation introduced
by constructive definition. With respect to the
non-eliminable identity relation, it is assumed
that the logic includes the axiom,

AxAy( Ez( x = z /\ z = y ) -> x = y )

and the schema

A_{phi}A_{x,y}[ ( Ex( phi(x) ) -> ( phi(y) /\ y = y ) ]

where y does not occur free in phi(x)

governing the introduction of bare identity statements
into a proof. Any such logic will require additional
changes to other quantifier rules because it is assumed
that occurrences of free singular terms in a proof is
governed by correspondence with the identity statements
in a proof.

======================================
Recursively defined relations
======================================

01)
An apartness relation

AxAy( x # y <-> ( ~( x # x ) /\ ( ( ~( x # x ) -> y # x ) /\ ( y # x ->
x # y ) ) ) )

When apartness is asserted in the standard fashion, it
is given by the rules,

Ax~( x # x )

Ax( x # y -> y # x )

AxAy( x # y -> Az( x # z \/ z # y ) )

As can be seen by examination, the first two rules
are explicitly expressed in the definiendum above,
although the symmetry rule is represented by its
converse. The third rule is easily seen to be
the contrapositive form of the sentence which is
assumed to govern the introduction of bare
informative identity statements in logical
deductions,

AxAy( Ez( x = z /\ z = y ) -> x = y )

The sentence above will be related to this logical
axiom through a relation with the non-eliminable
identity stipulated through axioms in the theory.


-----

02) A non-eliminable identity relation

AxAy( x = y <-> Ez( x = z /\ z = y ) )

It is through this relation that the indiscernibility
of singular terms with respect to the non-logical
symbols may be assumed to correspond with the
interpretation of singular terms as individuals.


-----

03)
Subsitutivity with respect to the language primitive

AxAy( x not-in y <-> ( Az( ~( z = y ) \/ ( z = y /\ x not-in z ) ) \/
Az( ~( x = z) \/ ( x = z /\ z not-in y ) ) ) )

This appears confusing because it is using the intended
negation of the primitive to implement substitutivity.
It is easier to understand in terms of the formulas,

Ez( z = y /\ ( z = y -> x in z ) )

Ez( x = z /\ ( x = z -> z in y ) )

These formulas certainly make

x in y

true whenever the two existence assertions are
satisfied.

Substitutivity for the language primitives must be
explicitly provided for because the indiscernibility
of identicals,

A_{phi}A_{x,y}[ x = y -> ( phi(x) -> phi(y) ]

is not available until a bare identity statement has
been introduced.


======================================
Constructively defined relations
======================================

04) An eliminable indiscernibility relation

AxAy( x :: y <-> ( Az( x in z <-> y in z ) /\ Az( z in x <-> z in y ) ) )

Anyone familiar with Quine's analysis in "Set
Theory and Its Logic" should recognize this form.
One may call this a "defined identity". With
respect to the philosophy behind the standard
account of identity, this is a "relative
identity". As such, it expresses no more than
indiscernibility. It cannot support the
individuality which underlies the purported
interpretation of singular terms.

It is the simple assertion that one cannot
discern between singular terms on the basis of
the language primitive. More correctly, it
enforces that condition as a constraint.


======================================
Axioms
======================================

05)
Introduction of the primitive relation

AxAy~( x in y <-> x not-in y )

Observe that an exclusive disjunction has been
used here. This reflects classical logic as
a limit of partial systems. If a unary negation
had been used,

AxAy( x in y <-> ~x not-in y )

then it would be more correct to call this a
constructive definition with respect to symbols
that have already been defined.


-----

06)
A true apartness relation only holds for existents

AxAy( x # y -> ( x = x /\ y = y ) )


-----

07)
A true trivial identity relation must deny a trivial
apartness relation

Ax( x = x -> ~( x # x ) )


-----

08)
A false informative identity relation must affirm an
apartness relation

AxAy( ~( x = y ) -> x # y )


-----

09)
Fregean concept identity denies apartness

AxAy( Az( z in x <-> z in y ) -> ~( x # y ) )

It is important to compare this antecedent with
the consequent of the axiom in 11). When that
consequent is satisfied, this axiom is satified.


-----

10)
Denying Fregean object identity denies identity

AxAy( Ez~( x in z <-> y in z ) -> ~( x = y ) )

It is important to compare this antecedent with
the antecedent of the axiom in 11). When that
antecedent is not satisfied, this axiom is satified.


-----

11)
Fregean object identity affirms Fregean concept
identity

AxAy( Az( x in z <-> y in z ) -> Az( z in x <-> z in y ) )


======================================
Theorems
======================================

12)
Indiscernible terms may be presumed to denote the same
individual

AxAy( x :: y -> x = y )


-----

13)
Discernible terms may be presumed to denote different
individuals

AxAy( ~( x :: y ) -> x # y )


======================================
Proofs
======================================

14) Theorem 1: AxAy( x :: y -> x = y )

Let x and y be arbitrary such that x :: y. This
establishes the premise. From

AxAy( x :: y <-> ( Az( x in z <-> y in z ) /\ Az( z in x <-> z in y ) ) )

it follows that

( Az( x in z <-> y in z ) /\ Az( z in x <-> z in y ) ) )

By the elimination of the conjunction, one may
further conclude

Az( z in x <-> z in y )

But, this is just the premise for the axiom,

AxAy( Az( z in x <-> z in y ) -> ~( x # y ) )

Thus, ~( x # y ). Given the axiom,

AxAy( ~( x = y ) -> x # y )

one obtains

x = y

from the contrapositive.

This completes the proof.


-----

15) Theorem 2: AxAy( ~( x :: y ) -> x # y )

Let x and y be arbitrary such that ~( x :: y ). This
establishes the premise. From

AxAy( x :: y <-> ( Az( x in z <-> y in z ) /\ Az( z in x <-> z in y ) ) )

it follows that ~( x :: y ) has three cases,


Ez~( x in z <-> y in z ) /\ Az( z in x <-> z in y )

Ez~( x in z <-> y in z ) /\ Ez~( z in x <-> z in y )

Az( x in z <-> y in z ) /\ Ez~( z in x <-> z in y )


By the axiom,

AxAy( Az( x in z <-> y in z ) -> Az( z in x <-> z in y ) )

one can exclude the third case. This leaves,


Ez~( x in z <-> y in z ) /\ Az( z in x <-> z in y )

Ez~( x in z <-> y in z ) /\ Ez~( z in x <-> z in y )


But,

Ez~( x in z <-> y in z )

holds in both of these case after elimination of
the conjunctions. Moreover, this is just the
premise for the axiom,

AxAy( Ez~( x in z <-> y in z ) -> ~( x = y ) )

Thus ~( x = y ) holds. Given the axiom,

AxAy( ~( x = y ) -> x # y )

one obtains x # y from ~( x = y )

This completes the proof.

[mitch]

Fregean object identity denies apartness

AxAy( Az( x in z <-> y in z ) -> ~( x # y ) )

It is important to compare this antecedent with
the consequent of the axiom in 11). When that
consequent is satisfied, this axiom is satified.


-----

10)

Denying Fregean concept identity denies identity

AxAy( Ez~( z in x <-> z in y ) -> ~( x = y ) )

It is important to compare this antecedent with
the antecedent of the axiom in 11). When that
antecedent is not satisfied, this axiom is satified.


-----

11)

Fregean concept identity affirms Fregean object
identity

AxAy( Az( z in x <-> z in y ) -> Az( x in z <-> y in z ) )

======================================
Theorems
======================================

12)
Indiscernible terms may be presumed to denote the same
individual

AxAy( x :: y -> x = y )


-----

13)
Discernible terms may be presumed to denote different
individuals

AxAy( ~( x :: y ) -> x # y )


======================================
Proofs
======================================

14) Theorem 1: AxAy( x :: y -> x = y )

Let x and y be arbitrary such that x :: y. This
establishes the premise. From

AxAy( x :: y <-> ( Az( x in z <-> y in z ) /\ Az( z in x <-> z in y ) ) )

it follows that

( Az( x in z <-> y in z ) /\ Az( z in x <-> z in y ) ) )

By the elimination of the conjunction, one may
further conclude

Az( x in z <-> y in z )

But, this is just the premise for the axiom,

AxAy( Az( x in z <-> y in z ) -> ~( x # y ) )

Thus, ~( x # y ). Given the axiom,

AxAy( ~( x = y ) -> x # y )

one obtains

x = y

from the contrapositive.

This completes the proof.


-----

15) Theorem 2: AxAy( ~( x :: y ) -> x # y )

Let x and y be arbitrary such that ~( x :: y ). This
establishes the premise. From

AxAy( x :: y <-> ( Az( x in z <-> y in z ) /\ Az( z in x <-> z in y ) ) )

it follows that ~( x :: y ) has three cases,

Ez~( x in z <-> y in z ) /\ Az( z in x <-> z in y )

Ez~( x in z <-> y in z ) /\ Ez~( z in x <-> z in y )

Az( x in z <-> y in z ) /\ Ez~( z in x <-> z in y )


By the axiom,

AxAy( Az( z in x <-> z in y ) -> Az( x in z <-> y in z ) )

one can exclude the first case. This leaves,


Ez~( x in z <-> y in z ) /\ Ez~( z in x <-> z in y )

Az( x in z <-> y in z ) /\ Ez~( z in x <-> z in y )


But,

Ez~( z in x <-> z in y )

holds in both of these case after elimination of
the conjunctions. Moreover, this is just the
premise for the axiom,

AxAy( Ez~( z in x <-> z in y ) -> ~( x = y ) )

[mitch]

On 03/01/2017 05:23 PM, mitch wrote:

< snip >


This theory will use a non-eliminable identity
relation introduced by recursive definition and
an eliminable indiscernibility relation introduced
by constructive definition. With respect to the
non-eliminable identity relation, it is assumed
that the logic includes the axiom,

AxAy( Ez( x = z /\ z = y ) -> x = y )

and the schema

A_{phi}A_{x,y}[ ( Ex( phi(x) ) -> ( phi(y) /\ y = y ) ]

where y does not occur free in phi(x)

governing the introduction of bare identity statements
into a proof. Any such logic will require additional
changes to other quantifier rules because it is assumed
that occurrences of free singular terms in a proof is
governed by correspondence with the identity statements
in a proof.

mitch

[mitch]

On 03/01/2017 05:23 PM, mitch wrote:

< snip >

[mitch]

On 03/01/2017 05:23 PM, mitch wrote:

< snip >



======================================

AxAy( ~( x = y ) -> x # y )

mitch

[mitch]

On 03/01/2017 05:23 PM, mitch wrote:

< snip >

09)
Fregean concept identity denies apartness

AxAy( Az( z in x <-> z in y ) -> ~( x # y ) )

It is important to compare this antecedent with
the consequent of the axiom in 11). When that
consequent is satisfied, this axiom is satified.


-----

10)

Denying Fregean object identity denies identity

AxAy( Ez~( x in z <-> y in z ) -> ~( x = y ) )

It is important to compare this antecedent with
the antecedent of the axiom in 11). When that
antecedent is not satisfied, this axiom is satified.


-----

11)

Fregean object identity affirms Fregean concept
identity

AxAy( Az( x in z <-> y in z ) -> Az( z in x <-> z in y ) )



mitch

[mitch]

On 03/01/2017 05:23 PM, mitch wrote:

< snip >

======================================
Theorems
======================================

12)
Indiscernible terms may be presumed to denote the same
individual

AxAy( x :: y -> x = y )


-----

13)
Discernible terms may be presumed to denote different
individuals

AxAy( ~( x :: y ) -> x # y )


======================================
Proofs
======================================

14) Theorem 1: AxAy( x :: y -> x = y )

Let x and y be arbitrary such that x :: y. This
establishes the premise. From

AxAy( x :: y <-> ( Az( x in z <-> y in z ) /\ Az( z in x <-> z in y ) ) )

it follows that

( Az( x in z <-> y in z ) /\ Az( z in x <-> z in y ) ) )

By the elimination of the conjunction, one may
further conclude

Az( z in x <-> z in y )

But, this is just the premise for the axiom,

AxAy( Az( z in x <-> z in y ) -> ~( x # y ) )

Thus, ~( x # y ). Given the axiom,

AxAy( ~( x = y ) -> x # y )

[mitch]

On 03/01/2017 05:23 PM, mitch wrote:

< snip >


======================================
Theorems
======================================

12)
Indiscernible terms may be presumed to denote the same
individual

AxAy( x :: y -> x = y )


-----

13)
Discernible terms may be presumed to denote different
individuals

AxAy( ~( x :: y ) -> x # y )


======================================
Proofs
======================================

15) Theorem 2: AxAy( ~( x :: y ) -> x # y )

Let x and y be arbitrary such that ~( x :: y ). This
establishes the premise. From

AxAy( x :: y <-> ( Az( x in z <-> y in z ) /\ Az( z in x <-> z in y ) ) )

it follows that ~( x :: y ) has three cases,

Ez~( x in z <-> y in z ) /\ Az( z in x <-> z in y )

Ez~( x in z <-> y in z ) /\ Ez~( z in x <-> z in y )

Az( x in z <-> y in z ) /\ Ez~( z in x <-> z in y )


By the axiom,

AxAy( Az( x in z <-> y in z ) -> Az( z in x <-> z in y ) )

one can exclude the third case. This leaves,

Ez~( x in z <-> y in z ) /\ Az( z in x <-> z in y )

Ez~( x in z <-> y in z ) /\ Ez~( z in x <-> z in y )


But,

Ez~( x in z <-> y in z )

holds in both of these case after elimination of

the conjunctions. Moreover, this is just the
premise for the axiom,

AxAy( Ez~( x in z <-> y in z ) -> ~( x = y ) )

Thus ~( x = y ) holds. Given the axiom,

AxAy( ~( x = y ) -> x # y )

one obtains x # y from ~( x = y )

This completes the proof.



mitch

[mitch]

On 03/01/2017 05:23 PM, mitch wrote:

< snip >

-----

09)
Fregean object identity denies apartness

AxAy( Az( x in z <-> y in z ) -> ~( x # y ) )

It is important to compare this antecedent with
the consequent of the axiom in 11). When that
consequent is satisfied, this axiom is satified.


-----

10)

Denying Fregean concept identity denies identity

AxAy( Ez~( z in x <-> z in y ) -> ~( x = y ) )

It is important to compare this antecedent with
the antecedent of the axiom in 11). When that
antecedent is not satisfied, this axiom is satified.


-----

11)

Fregean concept identity affirms Fregean object
identity

AxAy( Az( z in x <-> z in y ) -> Az( x in z <-> y in z ) )



mitch

[mitch]

On 03/01/2017 05:23 PM, mitch wrote:

< snip >

======================================
Theorems
======================================

12)
Indiscernible terms may be presumed to denote the same
individual

AxAy( x :: y -> x = y )


-----

13)
Discernible terms may be presumed to denote different
individuals

AxAy( ~( x :: y ) -> x # y )


======================================
Proofs
======================================

14) Theorem 1: AxAy( x :: y -> x = y )

Let x and y be arbitrary such that x :: y. This
establishes the premise. From

AxAy( x :: y <-> ( Az( x in z <-> y in z ) /\ Az( z in x <-> z in y ) ) )

it follows that

( Az( x in z <-> y in z ) /\ Az( z in x <-> z in y ) ) )

By the elimination of the conjunction, one may
further conclude

Az( x in z <-> y in z )

But, this is just the premise for the axiom,

AxAy( Az( x in z <-> y in z ) -> ~( x # y ) )

Thus, ~( x # y ). Given the axiom,

AxAy( ~( x = y ) -> x # y )

one obtains

[mitch]

On 03/01/2017 05:23 PM, mitch wrote:

< snip >


======================================
Theorems
======================================

12)
Indiscernible terms may be presumed to denote the same
individual

AxAy( x :: y -> x = y )


-----

13)
Discernible terms may be presumed to denote different
individuals

AxAy( ~( x :: y ) -> x # y )


======================================
Proofs
======================================

15) Theorem 2: AxAy( ~( x :: y ) -> x # y )

Let x and y be arbitrary such that ~( x :: y ). This
establishes the premise. From

AxAy( x :: y <-> ( Az( x in z <-> y in z ) /\ Az( z in x <-> z in y ) ) )

it follows that ~( x :: y ) has three cases,

Ez~( x in z <-> y in z ) /\ Az( z in x <-> z in y )

Ez~( x in z <-> y in z ) /\ Ez~( z in x <-> z in y )

Az( x in z <-> y in z ) /\ Ez~( z in x <-> z in y )


By the axiom,

AxAy( Az( z in x <-> z in y ) -> Az( x in z <-> y in z ) )

one can exclude the first case. This leaves,

Ez~( x in z <-> y in z ) /\ Ez~( z in x <-> z in y )

Az( x in z <-> y in z ) /\ Ez~( z in x <-> z in y )


But,

Ez~( z in x <-> z in y )

holds in both of these case after elimination of

the conjunctions. Moreover, this is just the
premise for the axiom,

AxAy( Ez~( z in x <-> z in y ) -> ~( x = y ) )

Thus ~( x = y ) holds. Given the axiom,

AxAy( ~( x = y ) -> x # y )

[Ross A. Finlayson]

About sameness(=), apartness(#), and differentness(::)
it seems there are, for example, various cases for the
vacuous or extreme (when one of x or y is null) that is not
necessarily seeing apartness when there is differentness
though you have it as conclusive. So, it seems among
examples particular structural forms as of special cases.


You mention Homotopy Type Theory as "alternative" to
traditional foundations (eg, Russell's type theory)
but HoTT is compared to ramified types just a neat
direct formalism for transitivity of type equality
just outside of the usual structural semantics to
some values semantics of types. Then HoTT is not so
alternative except for some case of the extreme
like the "univalency", a bridge or transfer result
built into HoTT, which otherwise has the "proof
strength of ZFC plus two inaccessible cardinals"
(i.e., a model and its model or "Cohen's cousins").

Otherwise ramified and stratified types allow
building the relevant transitive type semantics,
well-foundedly or regularly as it were.

Then HoTT seems to, add "expansion of comprehension"
with the "universe of universe universes" but as well
some other "restriction of comprehension" as "well,
you know, as long as it doesn't break something else
and don't look too closely at that result or carry
over carrying it over". That "restriction of comprehension"
I haven't seen stated as part of HoTT, which seems as
bad as Russell was to Frege.

As a formalism for a neat mechanical treatment then
HoTT is a terse syntax with the well-directed proof
strength (more terse than ZF's plain type theory
with the same proof strength) but it doesn't seem to
allow gaining "more" than ZF without being inconsistent.

Russell wins again. But, that's not so much a gainer
until Goedel wins, too.


Predicates of = and <>, #, ::, =/=, ~ might look to
have different semantics in a set theory's hierarchical
types (eg, ZFC) and a category theory's universalized
types, (eg, HoTT).

[George Greene]

On Wednesday, March 1, 2017 at 6:23:33 PM UTC-5, mitch wrote:
> There are issues surrounding the identity of
> indiscernibles in the foundations of mathematics.
> Traditional foundations denies it as a logical
> principle.

"Traditional foundations" also includes SET THEORY, which,
while it does (traditionally) deny i.i as a *logical* principle,
is therefore able to assert actual semantic content in AFFIRMING
identity of indiscernibles via the Axiom of Extensionality.

Since set theory BASICALLY IS the "traditional foundation" and
since it has an axiom EXPLICITLY ASSERTING identity of indiscernibles,
well....

[mitch]

Well what?

I acknowledge that the axiom of extensionality
is an implementation of the principle in the
post.

By "traditional foundations" I refer to the influence
of Wittgenstein toward the rejection of the principle
as a logical principal.

By "traditional foundations" I also refer to Skolem's
criticism of Zermelo which relegated set theory to
just another theory. In effect, that makes something
like universal algebra foundational. More precisely,
that transforms "traditional foundations" to solely
syntactic studies. There are books on my shelves that
assert how model theory is not appropriate for
foundational studies. Also, there is a steady, but
infrequent, flow of questions to MSE questioning the
relevance of set theory to mathematics in general.
So, set theory is not BASICALLY anything. It is
BELIEVED by some to be something. And, when belief
is the basis of foundation, well....

The treatment of identity in the theory had been one
of the changes to the theory attributed to Skolem's
criticism. Although Zermelo had no specific account
of a definite property in his original paper, he had
been clear about the interpretation of identity in
the theory.

Simply put, "a = b" had been a relation between names
supported by the axiom of singletons. Zermelo used this
mechanism to support urelements. Asserting the existence
of a null set ensured that there was an object which
would not be a urelement even though it contained no
members.

It is difficult for me to explain this to you because
of our different backgrounds. In topology, there is
the notion of a principal filter. Every singleton is
associated with a principal filter. It is the collection
of all of the sets which have it as an element. More
generally, the notion of a proper filter is
order-theoretic.

The fact of the matter is, however, that every subset
generates a principal filter. So, simply descending through
an order chain to some locus that generates a principal
filter does not necessarily yield a singleton.

This can be very explicitly understood in terms of
Cantor's nested set theorem for closed sets. The
theorem depends upon *vanishing diameters* to generate
a singleton. But if one specifies a positive diameter,
one obtains a closed ball of that diameter. A logical
system, however has no "diameters" governing the
situation.

In the system to which you have so strenuously objected,
the first sentence may be thought of as asserting a
system of parts,

AxAy( x ppart y <-> ( Az( y ppart z -> x ppart z ) /\ Ez( x ppart z /\
~( y ppart z ) ) ) )

[ Wittgenstein: *The world* divides into *parts*. ]

Meanwhile the second sentence prepares for the differentiation
of singletons within that system,

AxAy( x in y <-> ( Az( y ppart z -> x in z ) /\ Ez( x in z /\ ~( y ppart
z ) ) ) )

If the two relations are taken to coincide, you have what
Paley calls a hallmark of the mereological view. He is
referring to Dedekind when he says that.

It is very difficult working with sentences like these,
and for a long time I thought it to be enough to use those
sentences to formulate a defined identity. But, I now think
the descending order chain must be asserted as an explicit
consequence of a true membership relation,

AxAy( x in y -> Ez( x in z /\ ( x in z -> ( z ppart y \/ Aw( z ppart w
-> y ppart w ) ) ) ) )

The definition,

AxAy( x part y <-> Az( y ppart z -> x ppart z ) )

is reflexive by virtue of the conditional in the definiendum. So
the statement above says that z is a proper part or z is a part.

Suppose

Az( ~( x in z ) \/ ( x in z /\ ( ~( z ppart y ) /\ Ew( z ppart w /\ ~( y
ppart w ) ) ) )

This is the negation of the consequent. It makes a statement
about when x in z. First, ~( z ppart y ) must hold. But, it
is the case that ~( z ppart y ) does not exclude z part y. The
existential subformula refers to the principal filter of z.
And, it states that it must be different from the principal
filter of y. So, this excludes the possibility of x in y.

Analyzing the order-theoretic account of Leibniz shows how
the relationship between Fregean object identity and Fregean
concept identity is encapsulated in the directionality
of conditionals. Here, it is the next step which establishes
the relationship between converse orders.

Let the subset relation be defined by

AxAy( x sub y <-> Ez( x part z /\ z part y ) )

with the axiom,

AxAy( x sub y -> Az( z in x -> z in y ) )

Also, let the proper subset be defined in a purely extensional
manner,

AxAy( x psub y <-> ( Az( z in x -> z in y ) /\ Ez( z in y /\ ~( z in x )
) ) )

So, once one handles the issues of indiscernibility and
individuality, the usual sense of a cumulative hierarchy
can be given.

What has been done above deals with the notion of indiscernibility
in the order-theoretic sense. It supports the notion of a
singleton in so far as it relates membership and principal
filters. But, it cannot assert the numerical identity attached
to the notion of an individual.

Similarly, a defined identity,

AxAy( x :: y <-> ... )

in terms of 'in' and 'ppart' is also merely indiscernibility
in a grammatical sense.

When Aristotle discusses the four ways by which on thing can
be prior to another, he uses numbers to explain the second
account,

< begin quote >

"Second, what does not reciprocate in implication of
being. One, for instance, is prior to two; for if there
are two, it follows immediately that there are one, whereas
if there is one, it is not necessary that there are two,
so that from one the implication of the other's being
does not hold reciprocally; and the sort of thing that
seems to be prior is that from which there is no reciprocal
implication of being."

< end quote >


The arithmetical strength of set theory comes from
the membership relation. But the relationship to
individuals has to come through existential
quantifiers. So, even here one needs to establish
a relationship with Tarski's axiom,

AxAy( x = y <-> Ez( x = z /\ z = y ) )

One does not get this for free.

mitch

[George Greene]

On Saturday, March 4, 2017 at 10:18:21 AM UTC-5, mitch wrote:
> Well what?

Well you are not doing anything DIFFERENT from anything USUAL, THAT'S what.

> I acknowledge that the axiom of extensionality
> is an implementation of the principle in the
> post.

But it is NOT done at a LOGICAL level.
This implies that the standard traditional logic in question is agnostic
on the question of whether indiscernibles are or are not "identical".
If you want to make them so, you HAVE TO ADD an AXIOM MAKING them so.
Traditionally, it is logically possible for them not to be. Equally traditionally, however, SET THEORY IS *THE* traditional foundation.

> By "traditional foundations" I refer to the influence
> of Wittgenstein toward the rejection of the principle
> as a logical principal.

Wittgenstein DOES NOT *HAVE*ANY* influence in foundations of math, YOU IDIOT!!

> > By "traditional foundations" I also refer to Skolem's
> criticism of Zermelo which relegated set theory to
> just another theory.

Said relegation was NOT permanent and DESPITE said alleged relegation,
set theory OBVIOUSLY IS *NOT* just another theory. IT IS, IN FACT,
in everybody's current practice, THE TRADITIONAL foundation and has been
ever since Cohen's independence results were proved IN THAT theory in the 1960s.
How can you be SO UNfamiliar with WHAT IS traditional??

[mitch]

On 03/04/2017 04:02 PM, George Greene wrote:
> On Saturday, March 4, 2017 at 10:18:21 AM UTC-5, mitch wrote:
>> Well what?
>
> Well you are not doing anything DIFFERENT from anything USUAL, THAT'S what.
>

As usual, opinion without anything useful
or helpful.

Same shit.

Bye.

mitch

[Ross A. Finlayson]

It seems like set theory is a traditional (and useful) descriptive
milieu. Foundations of numbers or geometry or parts or categories
or wholes or universes might so vary from set theory in terms of
their primary objects, that it results they have much the same
content eventually as can be extracted in logical and stipulated
non-logical terms.

The question of "what is the foundation" does involve philosophy,
also the question of what it does, how it is, and so on.

Higher order logic, zero-th order logic, at some point it has to
resolve how those are all a first order logic.

Goedel found a critical valve in (regular, ordinary) set theory:
there's more to it than its regular, ordinary self.

It seems to involve symmetry in complement, not that they start
the same, opposites, but that the end the same.

[George Greene]

On Wednesday, March 1, 2017 at 6:29:58 PM UTC-5, mitch wrote:
> This theory will use a non-eliminable identity
> relation introduced by recursive definition and
> an eliminable indiscernibility relation introduced
> by constructive definition.

Traditional foundations embraces identity of indiscernibles.
Even though it is not a logical principle of the traditional approach,
it is affirmed, semantically, in the traditional approach, through
the axiom of extensinnality. By drawing the distinction you are drawing
here, are you explicitly rejecting identity of indiscernibles?

[Jim Burns]

On 3/1/2017 6:32 PM, mitch wrote:
> On 03/01/2017 05:23 PM, mitch wrote:

> This theory will use a non-eliminable identity
> relation introduced by recursive definition and
> an eliminable indiscernibility relation introduced
> by constructive definition. With respect to the
> non-eliminable identity relation, it is assumed
> that the logic includes the axiom,
>
> AxAy( Ez( x = z /\ z = y ) -> x = y )
>
> and the schema
>
> A_{phi}A_{x,y}[ ( Ex( phi(x) ) -> ( phi(y) /\ y = y ) ]
>
> where y does not occur free in phi(x)
>
> governing the introduction of bare identity statements
> into a proof. Any such logic will require additional
> changes to other quantifier rules because it is assumed
> that occurrences of free singular terms in a proof is
> governed by correspondence with the identity statements
> in a proof.

I've been waiting to put my hand up and offer a comment
or a question until after I've done the required reading.
But by the time I get around to doing that, I'm sure
the conversation will have moved on, down the block,
across the city, to another country, perhaps.

So, I know it's not fair to ask you to read my thoughts
when I haven't figured out what you have to say yet,
but... Well, no buts. I'm just impatient, that's all.

----
It seems to me that formalizing indiscernability gives
us a second order definition of first order equality.

Ax,Ay, x = y <->
( AAp, p(x, ... ) <-> p(y, ... )
& AAf, f(x, ... ) = f(y, ... ) )

where the '...' mean "otherwise the same",
p is a predicate variable, f is a function variable,
and the equality of f-values can be cashed out as
further statements of logically equivalence.

(And from this second order definition, we derive
first order substitution schema, reflexivity, symmetry
and transitivity, and leave second order behind.)

Maybe I'm not understanding (I wouldn't be surprised),
but I think you (mitch) are trying to explore primitive
_identity_ as opposed to _indiscernability_ . I don't
want to persuade you to give up (if I do understand),
but, in my opinion, indiscernability is the best that
we can do _in principle_ .

It seems to me that what we mean by
"b is indiscernable from c"
is
"whatever we say about c, we can say about b"
which is a statement about _what we can say_ ,
not a statement about _what is_ .

One way of looking at our logical/mathematical foundations
is as semantics described in set theory. That's a reasonable
enough position, because to go lower than that would be
too trivial. But really, isn't the ground level entrance
to our stack of theories propositional logic, and slightly
above that predicate logic? Once we have those, we can
start to talk about sets.

If we want to do better than indiscernability, we have to
go _below_ propositional logic in our stack of theories,
it seems to me. The best that we can do with propositional
logic and everything that stands on it is to have everything
_it says_ be the same: indiscernable.

But I don't have a clue what "below [or prior to]
propositional logic" would even mean, much less how to go
there.

----
I've been reflecting on the power of the phrase "in the
language of".

If one has a formula defining exponentiation
_in the language of_ arithmetic, one has, in a sense, the
True Name of exponentiation. (All the spooky, conjuring
connotations are entirely intentional.)

If anything ,were what we think of as a proper name for
mathematical objects, I would think it would have to be a
defining formula _in the language of_ whatever language is for
our foundation. But, as I'm sure you know, there are multiple
(infinite!) interpretations of that True Name/formula.

(Not really to my point, but I can't resist. Part of what
Goedel did was figure out how to give the True Name
[the formula _in the language of_ arithmetic] of
recursively defined functions. Wow! Is that powerful!)

----
Okay, a maybe-weird thought:

Suppose Alan Turing was right, and there are programs that
can play his Imitation Game and win (that is, not lose
too badly) against humans. Suppose such programs get really,
_really_ good. Then the enormous formula _in the language of_
arithmetic that is equivalent that human-like program
would be its True Name.

I'm not sure what that means, if anything. Just weird.

[mitch]

On 03/07/2017 12:15 PM, Jim Burns wrote:
>
> But I don't have a clue what "below [or prior to]
> propositional logic" would even mean, much less how to go
> there.
>

I will reply to other statements in your
response. But, I returned to work this
week and time is now at a premium.

Because of the continuum hypothesis, I
asked myself what could be wrong with
logic that leads to the independence of
this question. I focused on two things.

One had been the question of undefined
language primitives.

The other had been the fact that unary
negation is eliminable by virtue of the
complete connectives. Moreover, unary
negation is not a connective in the sense
of a binary connective.

By studying "negation" and "de Morgan
conjugation" as involutions over the
entire set of truth tables, I generated
a pattern which I did not recognize.

Years later I found "Projective Geometry"
by Veblen and Young. When reading a
theorem statement, I recognized that pattern
from what was being asserted.

The truth tables relate to one another
as a finite affine geometry.

So my next step had been to ask how
16 named points become functions.

Who knew?

Of course, no one can follow what I
am doing as I pursue this. The combinatorial
complexity is immediate. And, at present, it
does not solve any problems.

Nor does it have any appeal to logicians (it
shouldn't). But, it seems as if it should
have some significance in foundations.

mitch

[Ross A. Finlayson]

About "why" +-(G)CH, that "why" whether or not
the affirmative or negative of the (generalized)
continuum hypothesis is undecided, it seems that
there are to be established the various results
as so establish the consistency (or non-contradiction,
where there isn't really a constructivist's "witness"
to the consistency as it would preclude the alternative),
that the results by their form or extension so advise
"why" the generalized continuum hypothesis is quite
most likely or demonstrably quite most reasonably so,
and how there can be independence results, from before
that, after that, when the resulting model is a model
of ZF(C), that deciding (G)CH either way then does
admit a witness in the resulting model of ZF(C) +-
(G)CH.

Then, that there are both, implies directly that there
are features of the relevant ordinals and cardinals as
are extra or beyond or "different" or that a model of
ZF is not the intended standard model but instead that
the real, ground model is non-standard or extra-standard,
that speaks to the "consistency" of ZF (which for all
other statements in the language of ZF is still true)
vis-a-vis its completeness that on the resulting examination
necessarily sees witnesses of both independent models,
and how they are models of each other.


It seems you think that +-(G)CH advises the structure
of permutations (as on "the order of" subsets, or
cardinality which is the only tractable limit in
this cardinal arithmetic, where finite unbounded
structures would have these variously), that there
is some applicability of the foundation have either,
or, or both models of +-(G)CH.


Otherwise the logical significance is a rather usual
reminder as of Russell about Frege, or Cantor about
Frege, or Quine about Cantor, (and what should also be
Russell about Cantor after Zermelo, Fraenkel, and von
Neumann,) and Goedel about ZFC that given the completeness
theorems of ZFC that there are incompleteness theorems of
ZFC that illustrate that a real model of ZFC is extra
ZFC and otherwise quite extra-ordinary and beyond ZFC,
but just that much.

This has rather concretely that the real model of ZFC
is and isn't its own extension, and that's OK.

Then, ZFC is just the regular ordinary fragment of
set theory, with ordinals for cardinals, vis-a-vis,
a theory with cardinals for ordinals, that order
and combinatorial richness are complementary,
alternative fundamental properties of succession
and progression.

A bounded fragment of ZF models finite combinatorics,
completely, then besides that Goedel and Cohen have
+(G)CH and -(G)CH "consistent" (non-contradictory)
with ZFC, Goedel reminds that ZF is incomplete and
here then that the density of cardinals is both so
and not so, that thus advising concrete properties
of the relevant structures as witness that the
real model is extra-ordinary.

Then (and this is my view) there's that ubiquitous
ordinals alternates with large cardinals then for
solving the similar problem that ordinals are through
Ord, an ordinal, while cardinals are through the
cumulative hierarchy, a universe of sets (and those
are the same).

Just like the primary object is either of the empty,
or, the universal, all the intermediate objects are
the successive and progressive (or cumulative), this
"symmetry flex" lets the eventual consequences of the
structure of theory not break itself.

For, eventually the foundation is sound to and from
all angles, and at any point.

[mitch]

On 03/07/2017 12:15 PM, Jim Burns wrote:

> On 3/1/2017 6:32 PM, mitch wrote:
>> On 03/01/2017 05:23 PM, mitch wrote:
>
>> This theory will use a non-eliminable identity
>> relation introduced by recursive definition and
>> an eliminable indiscernibility relation introduced
>> by constructive definition. With respect to the
>> non-eliminable identity relation, it is assumed
>> that the logic includes the axiom,
>>
>> AxAy( Ez( x = z /\ z = y ) -> x = y )
>>
>> and the schema
>>
>> A_{phi}A_{x,y}[ ( Ex( phi(x) ) -> ( phi(y) /\ y = y ) ]
>>
>> where y does not occur free in phi(x)
>>
>> governing the introduction of bare identity statements
>> into a proof. Any such logic will require additional
>> changes to other quantifier rules because it is assumed
>> that occurrences of free singular terms in a proof is
>> governed by correspondence with the identity statements
>> in a proof.
>
> I've been waiting to put my hand up and offer a comment
> or a question until after I've done the required reading.
> But by the time I get around to doing that, I'm sure
> the conversation will have moved on, down the block,
> across the city, to another country, perhaps.

I have been studying the same axioms for twenty-five
years. I am an auto-didact beyond some basic
undergraduate courses because of that. As for "required
reading", do not worry. It helps me to write things
out. Any responses to my (difficult) posts are helpful
to me. I killfile Mr. Greene these days. But the fact
is that his flame during 2003 and 2004 opened my eyes
to the reality of philosophy departments teaching
mathematics -- and it is not the same as what one learns
in a standard curriculum at most mathematics departments.

>
> So, I know it's not fair to ask you to read my thoughts
> when I haven't figured out what you have to say yet,
> but... Well, no buts. I'm just impatient, that's all.
>
> ----
> It seems to me that formalizing indiscernability gives
> us a second order definition of first order equality.
>
> Ax,Ay, x = y <->
> ( AAp, p(x, ... ) <-> p(y, ... )
> & AAf, f(x, ... ) = f(y, ... ) )
>
> where the '...' mean "otherwise the same",
> p is a predicate variable, f is a function variable,
> and the equality of f-values can be cashed out as
> further statements of logically equivalence.
>

I like this sentence very much. It exemplifies what
the focus of studies on formal systems requires. By
this, I mean the level of generalization.

However, to the extent that past generations are taught
that Zermelo-Fraenkel set theory is "the foundational
theory of mathematics", that level of generalization
becomes unwarranted. In such a (debatable) context,
one need only concern one's self with a specific
application.

That is why the significance of Skolem's criticisms of
Zermelo become an issue. If set theory is "just another
theory" then it cannot be "the foundational theory". On
the other hand, if one takes it to be "the foundational
theory", then the generality of your sentence is an
appropriate topic of formal systems that is secondary
to foundational analysis.

The SEP entry on "Skolem's Paradox" seems fairly balanced
on the issues. In Section 3.2,

https://plato.stanford.edu/entries/paradox-skolem/#3.2

it discusses skepticism toward Skolemite views. This
section includes the quote,

< begin quote >

"On the surface, after all, any sufficiently general
criticism of realism would apply to the Skolemite's own
model theory as much as it does to classical set theory.

< end quote >

So, it is certainly plausible for someone whose sole
question about the legitimacy of the mathematics being
taught lies with the model theory of Zermelo-Fraenkel
set theory ends up questioning the extent to which
the study of formal systems is actually relevant to
what has been taught as "foundations".

There is a second reason I like this sentence.

When I began posting again (by pinging you), I wrote

< begin quote >

"Suppose one required that the stipulated
meaning of non-logical symbols was required
as part of formalizing a mathematical proof."

< end quote >

followed by a brief historical discussion in
the same paragraph. With the next paragraph,
I wrote

< begin quote >

"Now consider what I have suggested for a moment
with respect to functions and constants. A formal
definition would be of the form,

Ax( x = null() <-> Ay( Az( z in x -> z in y ) /\ ~( y in x ) ) )

AxAy( x = P(y) <-> Az( Aw( w in z -> w in x ) -> z in y ) )

In both cases, the definiens depends upon a relation.
So, one must deal with relations before one
deals with singular terms."

< end quote >

Now, recall your formula from above,

>
> Ax,Ay, x = y <->
> ( AAp, p(x, ... ) <-> p(y, ... )
> & AAf, f(x, ... ) = f(y, ... ) )
>

You have occurrences of the sign of equality
on both sides of the biconditional.

This is one of the problems I have with any
analysis leading to universal algebras and
language signatures. They seem to be mere
stipulations that non-logical symbols are of
three types (constants, functions, and
predicates). For me, this is just a surface
analysis that does not take the structure of
proofs as a sequence of ordered assertions
into account. So, if proofs are to include
accounts of the non-logical symbols, stipulations
must precede general assertions, and, the
stipulations introducing relations must precede
the stipulations introducing functions and
constants.

Of course, that is just my personal aesthetic
in accord with the responsibility to offer an
alternative view when questioning received
views.

("I don't believe" without meeting such an
obligation seems irresponsible.)

The post from which I took my comments has
message id,

<qpOdndg6ae9MNinF...@giganews.com>


mitch

[mitch]

On 03/07/2017 12:15 PM, Jim Burns wrote:

The idea of substituting equals for equals can
be found in Euclid. So, first-order substitutivity
is actually "faithful" with respect to formalizing
mathematics. This is not derived from second-order
formulations.

As for "leaving second-order behind", the struggles
of nineteenth and early twentieth century logicians
makes that a very accurate view.

What seems to be the key motivating idea is the
development of logical calculi. Substituting
"equals for equals" seems odd in the case of
substituting "same for same". But, if you need
interpretations of the sign of equality governing
syntactic transformations, then the reflexive
axiom,

x = x

read as

"x is substitutable for x"

separates "logic" from the metaphysical concerns
that "identity" may carry. And with this, one
can prove symmetry and transitivity from the
indiscernibility of identicals,

Ap( x = y -> ( P(x) -> P(y) ) )

Personally, I would prefer to exchange the symbols
here because I would have this as

"y is substitutable for x"

But,

"x is equal to y"

sounds like

"x is substitutable for y"


There is a gap in my historical reading with respect
to Pierce, Shroeder, and Lowenheim. What I can say
is that de Morgan admitted an exception for parameterizing
the sign of equality when it is clear that other relations
may be represented without concern for intended content.
Hilbert described formalist domains as presupposing
well-construed identity relations. With Skolem and the
rise of first-order logic (Goedel's completeness theorem)
the exception for the sign of equality seems to be
lost. In addition, you have Wittgenstein's criticism
of the identity of indiscernibles to the extent that
it influenced philosophical persepectives on the matter.

All of this is separate from Frege's notion of
logicism based upon realizing arithmetic through
"extensions of concepts". It is with Frege's identity
puzzles where "from this second-order definition"
has its significance.

From the standpoint of first-order logic as the
received view, Frege's work is historical. But,
if one has reason to question the logic, then
other logics more closely related to Frege's views
may come into play. There had been no such
sense of "logics" at the beginning of the
twentieth century.

If I remember correctly, there had not even been
a notion of truth table before Post and Wittgenstein.

mitch

[Jim Burns]

On 3/8/2017 12:20 PM, mitch wrote:
> On 03/07/2017 12:15 PM, Jim Burns wrote:

> Now, recall your formula from above,
>
>>
>> Ax,Ay, x = y <->
>> ( AAp, p(x, ... ) <-> p(y, ... )
>> & AAf, f(x, ... ) = f(y, ... ) )
>>
>
> You have occurrences of the sign of equality
> on both sides of the biconditional.

I'll have more to add later, but one point I'd like
to clear up:

When I presented that definition, I said that
the f-values would be cashed out with more statements
of equivalence. Basically, I intend a fuller (but
less comprehensible) definition to have '=' only on
one side.

I haven't written out the fuller definition yet, but I have
some ideas of how I want it to look.

The model I'd like to follow is Goedel's expression of
recursive definitions in the language of arithmetic. An
essential aspect of that is finding a way to describe
_finite sequences_ of numbers. Goedel found that he was
able to use the Chinese Remainder Theorem to do that.

// f(a,b) = c is some recursively defined function
// f(a,0) = g(a)
// f(a,k) = m -> f(a,Sk) = h(a,k,m)

// for example,
// exp(a,0) = S0 = g(a)
// exp(a,Sk) = m -> exp(a,Sk) = a*m = h(a,k,m)

// foo := bar
// means
// "foo is an abbreviation of bar, and can be replaced by bar"

f(a,b) = c :=
Ex,Ey,(
funcdef(x,y,0) = g(a)
& Am,Ak,(( k < b ) ->
( funcdef(x,y,k) = m ) ->
funcdef(x,y,Sk) = h(a,k,m) )
)
& funcdef(x,y,b) = c
)

where we define
a =< b := ( En,( a + n = b ) )

a < b := ( Sa =< b )

a % b = c := ( En,( a = b*n + c & c < b ) )

funcdef(u,v,i) = j := u % S(v*Si) = j

// read
// funcdef(u,v,i) = j
// as "the function defined by u and v has value j at i"

// It is the Chinese remainder theorem that guarantees us
// there exists some u and v for which this is true, for
// any finite sequence of j-values.

So, that is the sort of thing I mean by saying there is
a recursive definition of '='. Not that we are allowing
'=' on the right side, but that there is a way to express
the concept of finite sequences of function names
(with a terminal predicate name).

(It may be that I'll have to enrich the language in
order to be able to do this. I can live with that.
I'm talking about _syntax_ not _semantics_ , I think.
And I've already gone to second order. How much
worse could it get?)

Anyway, this is my idea of what "indiscernible" means.
Surely, it has to be something like that, doesn't it?
Saying x = y doesn't become anything more than lines
on a page until we are talking about some sentence or
sentences being true or false.

What I'd like to do is characterize syntactically
which sentences x = y says are equivalent.
I _think_ Goedel did something similar.

[Ross A. Finlayson]

One might aver that syllogistic tableau (truth tables)
are available (as implicit conjunction or causality)
since about forever.

[Ross A. Finlayson]

That's kind of like "Venn and Boole".

[mitch]

On 03/07/2017 12:15 PM, Jim Burns wrote:

< snip >

>
> Maybe I'm not understanding (I wouldn't be surprised),
> but I think you (mitch) are trying to explore primitive
> _identity_ as opposed to _indiscernability_ . I don't
> want to persuade you to give up (if I do understand),
> but, in my opinion, indiscernability is the best that
> we can do _in principle_ .

You are very close here. And, I agree completely
with your statement.

For me, the motivating problem is the continuum
hypothesis.

Its independence rests with our understanding of
metatheory.

The received metatheory admits

x = x

as true through either "ontological considerations"
or "logical claims", where I am thinking about
a claim of "necessary logical form" in the latter
case.

With regard to the logical claim, it needs to
be true for every existent. But, what exists
needs to be dictated by the theory in question.
In general, set theory dictates what may exist
for a theory when the universal quantifier is
interpreted as a domain of existents. But, for
Zermelo-Fraenkel set theory over pure sets, itself,
the truth of an identity statement for what does
not exist in the theory becomes problematic.

Should the hypothetical nature of mathematical
statements be respected over the widest application
of logic, or, should the most general application
of the logic delineate what constitutes mathematical
discourse?

The received metatheory admits proper classes
because

x = x

is presented as being true in all cases. Whereas
the logical context for this is understood with
respect to the formulation of a calculus, the
ontological justification forces the hypothetical
nature of mathematical statements to be understood
solely through the intended interpretation of
singular terms as individuals. It is an artifact
of logical atomism.

The problem, then, is that the only means of
critical argument against the independence of the
continuum hypothesis is through identity statements
and their use in the metatheory.

In the SEP entry on "Nominalism in the Philosophy
of Mathematics", the discussion of deflationary
nominalism distinguishes between "ontological
commitments" and "quantifier commitments". What I am
doing does not correspond precisely with what is
described in the article, but the quote,

< begin quote >

"This means, however, that even though the semantics is
uniform throughout the sciences, mathematics and ordinary
language, deflationary nominalism requires the introduction
of the existence predicate. But, at least on the surface,
this predicate does not seem to have a counterpart in the way
language is used in these domains. It is the same semantics
throughout, but the formalization of the discourse requires an
extended language to accommodate the existence predicate. As a
result, the uniformity of the semantics comes with the cost of
the introduction of a special predicate into the language to
mark ontological commitment for formalization."

< end quote >

does express the idea of separating the indiscernibility
arising from the grammatical predicates and the "primitive
identity" with its existential quantifier. That "primitive
identity" is a proxy for the assertion that singular terms
represent individuals and justifies applying the logical
axioms to the system.

Perhaps a more telling quote related to how we agree on
indiscernibility being the best we can do is this remark:

< begin quote >

"As it turns out, on Azzouni's view, mathematical objects
are ontologically dependent on our linguistic practices
and psychological processes. And so, even though they may
be indispensable to our best theories of the world, we are
not ontologically committed to them. Hence, deflationary
nominalism is indeed a form of nominalism."

< end quote >

Almost everyone with minimal knowledge of foundations,
however, is taught about Frege's arguments against a
psychological basis for mathematics. But, they are not
taught about Frege's retraction of logicism late in
his career.

The best argument for separating the mathematical theory
and the logic in order to implement these ideas is in
a quote from Professor Holmes in the link,

http://www.personal.psu.edu/t20/fom/postings/9801/msg00128.html

Without committing himself to the position he describes,
he explains that the "if ... then ... " of a realist position
based upon hypotheticals cannot be simple material
implication. For his part, Professor Holmes would consider
second-order set theory to be a sufficient description of
mathematical truth without mathematical objects. But,
my problem only involves the metatheory by which the
continuum hypothesis is claimed to be independent of
Zermelo-Fraenkel set theory. So the emphasis lies on the
interpretation of identity statements for objects not
representable within the theory.

>
> It seems to me that what we mean by
> "b is indiscernable from c"
> is
> "whatever we say about c, we can say about b"
> which is a statement about _what we can say_ ,
> not a statement about _what is_ .
>

Correct.

But, ontological justifications for 'x = x' lie
precisely with the concerns for _what is_. I am
trying to retain the importance of this for the
logical calculus while isolating it from _what we
can say_ mathematically.

> One way of looking at our logical/mathematical foundations
> is as semantics described in set theory. That's a reasonable
> enough position, because to go lower than that would be
> too trivial. But really, isn't the ground level entrance
> to our stack of theories propositional logic, and slightly
> above that predicate logic? Once we have those, we can
> start to talk about sets.
>

What I said before about truth tables and the eliminability
of unary negation actually changed my views about what
you refer to as "the ground level" here.

At a level of combinatorial complexity far beyond where
I am at now, think about a projective plane of order 16
with 17 points on its line at infinity. The line is
fixed by an elation. One of its points are fixed by the
elation, while the other 16 points exchange with one
another as pairs.

I have begun to think of "self-identity" in terms of
such a notion of invariance based on finite geometries.
Because Hilbert pointed to arithmetical metamathematics
in his studies, finite geometries are an area that has
not even been broached.

For the truth tables in relation with one another
as a finite affine plane of order 4, the associated
projective plane has a line at infinity comprised of
5 points. As before, an elation exchanges 4 of those
points and holds one fixed. Let me name those points,

SOME --> Ex

OTHER --> Ex~

ALL --> Ax

NO --> Ax~

NOT

Within the affine subplane the truth table (names)
exchange with their negations.

This projective plane is a unit which could have
operators other than quantifiers naming those
4 points on the line at infinity. So, I do not
necessarily see a hierarchy at the very bottom of
how I understand these things. I see a transition
from the traditional square of opposition to the
modern "function concept" of truth functional logic
mediated by geometric (and unmentioned order-theoretic)
structures.

mitch

[mitch]

Should this

exp(a,Sk) = m -> exp(a,Sk) = a*m = h(a,k,m)

be

exp(a,k) = m -> exp(a,Sk) = a*m = h(a,k,m)

???

> // foo := bar
> // means
> // "foo is an abbreviation of bar, and can be replaced by bar"
>

Thanks for the reminder...

> f(a,b) = c :=
> Ex,Ey,(
> funcdef(x,y,0) = g(a)
> & Am,Ak,(( k < b ) ->
> ( funcdef(x,y,k) = m ) ->
> funcdef(x,y,Sk) = h(a,k,m) )
> )
> & funcdef(x,y,b) = c
> )
>
> where we define
> a =< b := ( En,( a + n = b ) )
>
> a < b := ( Sa =< b )
>
> a % b = c := ( En,( a = b*n + c & c < b ) )
>
> funcdef(u,v,i) = j := u % S(v*Si) = j
>
> // read
> // funcdef(u,v,i) = j
> // as "the function defined by u and v has value j at i"
>
> // It is the Chinese remainder theorem that guarantees us
> // there exists some u and v for which this is true, for
> // any finite sequence of j-values.
>

When I looked at building arithmetic from the order
relation in the sentence

AxAy( x < y <-> ( Az( y < z -> x < z ) /\ Ez( x < z /\ ~( y < z ) ) ) )

interpreted as "proper divisor" I wrote an axiom based
on Goedel's pairing function so that the system supported
the construction of sequences without reliance on
set-theoretic notions.

> So, that is the sort of thing I mean by saying there is
> a recursive definition of '='. Not that we are allowing
> '=' on the right side, but that there is a way to express
> the concept of finite sequences of function names
> (with a terminal predicate name).
>

OK.

I see it now.

I did the same thing "intuitively" by considering
the structure of the definitions. There is a
reduction to predicates (Unfortunately, I habitually
think in terms of "relations" coming from the
model-theoretic perspective. My usage expresses
that habit.)

> (It may be that I'll have to enrich the language in
> order to be able to do this. I can live with that.
> I'm talking about _syntax_ not _semantics_ , I think.
> And I've already gone to second order. How much
> worse could it get?)
>
> Anyway, this is my idea of what "indiscernible" means.
> Surely, it has to be something like that, doesn't it?

Yes. It is exactly like that.

> Saying x = y doesn't become anything more than lines
> on a page until we are talking about some sentence or
> sentences being true or false.
>

This is an interesting statement.

There is "true" and "false" in the sense of
semantics.

There is also "true" and "false" in the sense
of what is intended to be invariant across
transformations in a proof. This had been
Russell's criterion for distinguishing between
a rule of detachment and an axiom of the
logic.

Since the modern notion of derivation does
not seem to require that the first and last
formulas be closed, that is another area
in which I question whether the widest study
of formal systems is entirely relevant to how
mathematics is being represented in foundational
studies.

> What I'd like to do is characterize syntactically
> which sentences x = y says are equivalent.
> I _think_ Goedel did something similar.
>

It sounds like something that would be a
natural progression of his work.

It had been the incompleteness theorem which
motivated me to study mathematics. I can
now find reasons to discount it. But those
reasons all lie with a general criticism of
the arithmetization of mathematics. There
could be no "crisis in geometry" except among
those who confused geometry with a metaphysical
spatial theory.

Everything that comes out of Goedel's work
with arithmetic is simply stunning.

mitch

[mitch]

Boole's work had literally been algebraic. It
did not lead to truth tables directly. Rather,
it had been an attempt to make logic more
mathematical by treating conjunctions and disjunctions
as products and sums.

It is the ultimate irony. Boole is making logic
more mathematical while the continental mathematicians
begin making mathematics more logical.

Venn diagrams had been intended to provide
visual representations of syllogistic systems.
The complexity of such diagrams for more than
a few sentences is noteworthy. But, the smallest
diagram had been what brought my attention to
finite geometries.

When the three circles involved overlap, one gets
seven regions. Six of the regions are spatially
opposite to one another ( I cannot say symmetric
because they have different shapes ). Then, there
is a central region. The smallest projective
plane has seven points and seven lines.

You can see the diagrams in the link,

http://philosophy.lander.edu/logic/syll_venn.html

Because we learn Venn diagrams in the context of
modern mathematics and logic, we confuse the
modern notion with the original purpose in the
context of the logic of the time.

mitch

[Ross A. Finlayson]

It seems there's purely logical and properly logical
equality, indiscernibles are indistinguishable when
they have the same structure or that somehow, logically,
there is a reversal of complement as sameness. This is
where, in the properly logical, difference can be erased
(as of "logical equality" vis-a-vis "structural" or "bit-
wise" equality in computing's machine types), that '='
really is just a convenience in notation for otherwise
being in an equivalence class as about a relation (for
itemized matching besides broad classes).

Then what seems interesting for a logician is the logical
equality and this "reversal of complement" as is still
"purely logically" equality, i.e., as of no logical difference
whatsoever, here as usually of primary or ur- elements as
have themselves the inherent quality of so establishing a
refutation of paradox in logical systems (which lack them).

[George Greene]

On Wednesday, March 8, 2017 at 12:20:29 PM UTC-5, mitch wrote:

> That is why the significance of Skolem's criticisms of
> Zermelo become an issue.

NOTHING is "why the significance of Skolem's criticisms of Zermelo become an issue". Skolem's criticisms ARE NOT significant, and about that, there IS NO issue.

> If set theory is "just another
> theory" then it cannot be "the foundational theory".

That is utter horseshit. Every theory is different. It is entirely possible that ONE of these "just another theories" can be APPROPRIATE for foundations OF MATH, at least, even if not of anything else.
The fact that proofs have to be finite has led to A COMPELTELY separate foundational theory for proof theory, namely, primitive recursive arithemtic.
Finitist/Finitary considerations are INdispensable in THAT context BECAUSE
proofs have to be finite. THE REST OF MATH, BY CONTRAST, HAS to EMBRACE infinity and so of course is going to look different.

Your insistence on "the founcational" theory is itself ABSURD.
There are OBVIOUSLY MANY DIFFERENT POSSIBLE ways to do foundations.
I would like to point out that MERE BIT-STRINGS, the mere ASCII-encoding,
is a foundation -- whatEVER OTHER foundation ANYone else may come up with, you
can absolutely guaranteed that it will be presentable and explainable VIA THIS
medium (computers/ byte-streams) and so will therefore necessarily be reducible
TO BITS AS AN ALTERNATIVE foundation.

There are MANY, shall we say, "comprehensive neutral frameworks", where the framework is comprehensive in the sense that virtually anything cam be expressed in it, and neutral in the sense that its particular MODE or dialect of expression DOES NOT prejudice or advantage any one inquiry over any other.
There are -- again, OBVIOUSLY -- multiple different ways of defining and characterizing what we now call primtive recursive functions. The lambda calculus and Turing Machines and combinators don't superficially appear to have a lot in common, but it turns out there IS ONE thing going on there.

> The SEP entry on "Skolem's Paradox" seems fairly balanced
> on the issues. In Section 3.2,

Not really.

> "On the surface, after all, any sufficiently general
> criticism of realism

Realism is irrelevant bullshit; nothing more need be said.
It does NOT MATTER except to someone trying to finish a dissertation in philosophy whether mathematical objects are or are not "real", or if so,
what "the nature" of that reality is.
The issue is fundamentally NOT mathematical IN ANY case!!
Is the letter "a" "real"??

[George Greene]

On Wednesday, March 8, 2017 at 12:20:29 PM UTC-5, mitch wrote:

> The SEP entry on "Skolem's Paradox" seems fairly balanced
> on the issues. In Section 3.2,

Not really. The most balanced word in that treatment is "small".

>
> https://plato.stanford.edu/entries/paradox-skolem/#3.2
>
> it discusses skepticism toward Skolemite views.

We are dealing with nested levels of skepticism here.
The Skolemite view is itself skeptical both of the generally received
view, and, far more problematically, of the existence of uncountable sets.

> This
> section includes the quote,
>
> < begin quote >
>
> "On the surface, after all, any sufficiently general
> criticism of realism would apply to the Skolemite's own
> model theory as much as it does to classical set theory.
>
> < end quote >
>
> So, it is certainly plausible for someone whose sole
> question about the legitimacy of the mathematics being
> taught lies with the model theory of Zermelo-Fraenkel
> set theory ends up questioning the extent to which
> the study of formal systems is actually relevant to
> what has been taught as "foundations".

it is not legitimate that ANYbody questions THAT -- OF COURSE model
theory is relevant to foundations. Model-existence is equivalent to consistency!!

> "Suppose one required that the stipulated
> meaning of non-logical symbols was required
> as part of formalizing a mathematical proof."

This is a stupid assertion.
The axioms BY DEFINITION *DO* stipulate the meaning of all non-logical symbols occurring in them -- IN ANY axiom-set, the non-logical symbols BY DEFINITION mean EXACTLY what the axiom-set SAYS they mean. The whole axiom-set IS one extended definition of EVERY non-logical symbol occurring in it.
ALL axioms (collectively in each coherent axiom-set, even if not individually) ARE stipulations of meaning, BY DEFINITION (of "axiom").

[Julio Di Egidio]

On Thursday, March 9, 2017 at 2:57:36 AM UTC+1, George Greene wrote:
<snip>

> Realism is irrelevant bullshit; nothing more need be said.
> It does NOT MATTER except to someone trying to finish a dissertation in philosophy whether mathematical objects are or are not "real", or if so,
> what "the nature" of that reality is.
> The issue is fundamentally NOT mathematical IN ANY case!!
> Is the letter "a" "real"??

Philosophy per se is NOT irrelevant, indeed forgetting about philosophy
is another way to say the sickness of our epoch and culture. That said,
of course I agree with you: properly philosophical issues indeed are
utterly irrelevant to mathematical theories and foundations, and they
hardly matter even as for doing mathematics.

Julio

[Jim Burns]

On 3/8/2017 6:07 PM, mitch wrote:
> On 03/07/2017 12:15 PM, Jim Burns wrote:

>> Maybe I'm not understanding (I wouldn't be surprised),
>> but I think you (mitch) are trying to explore primitive
>> _identity_ as opposed to _indiscernability_ . I don't
>> want to persuade you to give up (if I do understand),
>> but, in my opinion, indiscernability is the best that
>> we can do _in principle_ .
>
> You are very close here. And, I agree completely
> with your statement.
>
> For me, the motivating problem is the continuum
> hypothesis.

We may be heading in different directions from this point
on. To me, the continuum hypothesis doesn't look
foundational at all. It may be that you and I are trying
to answer different questions with our respective
foundations.

[...]

> The received metatheory admits proper classes
> because
> x = x
> is presented as being true in all cases. Whereas
> the logical context for this is understood with
> respect to the formulation of a calculus, the
> ontological justification forces the hypothetical
> nature of mathematical statements to be understood
> solely through the intended interpretation of
> singular terms as individuals. It is an artifact
> of logical atomism.

I have concerns about logical atomism. Does logical
atomism correctly describe a Quantum Universe? I
strongly suspect that it doesn't.

I am taking logical atomism to refer to Betrand Russells'
grounding his semantics in "facts" -- which I mistook
for _statements about facts_ here in sci.logic not very
long ago. (It was Peter Olcott who introduced me to
"facts".)

I know, it seems crazy. The idea, the _certainty_ that
there is a fact of the matter for things like whether
Shroedinger's cat will be alive or dead when we later open
a box _whether or not we know which_ seems to be among the
most boring and mundane of furniture in our inner worlds.

I'm not completely sure my interpretation of various
experiments is correct, but my best guess is that (i) if
there is a fact of the matter whether the cat will be alive
or dead, it will be determined by what is in the box,
(ii) I believe this is a restatement of local causality, and
(iii) I'm pretty sure local causality (which John Bell
proved to contradict quantum mechanics in some circumstances)
_fails_ , when it goes head-to-head against quantum mechanics.

To put it in logical-atomistic terms, there are no logical
atoms (facts) until the wave function collapses -- or so I
strongly suspect.

This concern I have about the nature of "facts" is a good
background for my own foundation-like inquiries. We humans
are a middle-sized species, somewhere between atoms and
galaxies, and our size plays a role in what we consider
"normal" behavior of our surroundings. When we explore outside
our comfort zone, I'm not sure what some of the things we say
mean, or if they are true or false, or if it is not a mistake
to ask if they are true or false.

Something I still feel confident about, though, is that
_if I say_ Ax, ~(Sx = 0), then _I have said_ Ax, ~(Sx = 0)
I would like mathematics and logic to be grounded in
speech acts (syntax) instead of facts (semantics).

I am still confident about the overall nature of our speech
acts, anyway, and I expect to remain confident (I, along with
our many-times descendants) because we are middle-sized, and
our speech acts reflect the "normal" middle-sized behavior of
our middle-sized immediate surroundings.

What our speech acts _describe_ is a different matter.
We've already used them to describe atoms and galaxies,
and I don't expect it to stop there.

[...]

[Ross A. Finlayson]

It's one thing to have a philosophy that a foundation is a
platform, it's another to have "the" foundation as a sole
foundation, that philosophy and mathematics as bridged by
logic (for reason and critical reason's sake) must evenly
reconcile.

Some have mathematics as a branch of logic and others as
vice versa, these inversions of priority reflect their use
or application of sorts, then for about where they naturally
lay as indispensably one without the other. That's all
largely as the properly logical, philosophy basically gives
is our word for the primary objects of theory that as an
abstract reasoning, logic "is".

Some have foundation as platonic or objective, beyond being
a stable platform for usual fundamental results of various
usual systems of arithmetic, combinatorics, and analysis as
are so fruitful, the very consideration of the extra or
beyond (or super) courtesy Goedel hint not only that a
restful foundation remains to be found but that indeed
applications may so result as further justifying a true
foundation and sole foundation and self-fulfilling besides
a platform for (some) systemic results in the applied.

[Julio Di Egidio]

On Thursday, March 9, 2017 at 3:40:47 AM UTC+1, Ross A. Finlayson wrote:
> On Wednesday, March 8, 2017 at 6:30:40 PM UTC-8, Julio Di Egidio wrote:
> > On Thursday, March 9, 2017 at 2:57:36 AM UTC+1, George Greene wrote:
> > <snip>
> > > Realism is irrelevant bullshit; nothing more need be said.
> > > It does NOT MATTER except to someone trying to finish a dissertation in philosophy whether mathematical objects are or are not "real", or if so,
> > > what "the nature" of that reality is.
> > > The issue is fundamentally NOT mathematical IN ANY case!!
> > > Is the letter "a" "real"??
> >
> > Philosophy per se is NOT irrelevant, indeed forgetting about philosophy
> > is another way to say the sickness of our epoch and culture. That said,
> > of course I agree with you: properly philosophical issues indeed are
> > utterly irrelevant to mathematical theories and foundations, and they
> > hardly matter even as for doing mathematics.
>

> It's one thing to have a philosophy that a foundation is a
> platform, it's another to have "the" foundation as a sole
> foundation, that philosophy and mathematics as bridged by
> logic (for reason and critical reason's sake) must evenly
> reconcile.

Bullshit, you just don't know what you are talking about.

> Some have mathematics as a branch of logic

Some have the world is flat.

Julio

[Ross A. Finlayson]

There's a lot built into "quantum causality" in terms of
the auto-interaction of systems of particles as waves
that to preserve causality may see super-tachyonic models
of extra-classical waves or a non-classical wave model,
meaning that physics might "really" have that what we
model as the classical wave in solution is just an image.

That you look to be establishing a science of communication
(vis-a-vis its deterministic inputs and outputs) see a
utility for, ... utility logics that often can have the
difference erased as the same statements in first order
logic (the classical variety).

I don't really see any reason why something that's logically
available couldn't be expressed, if not in its entirety, at
least in its sum.

[Ross A. Finlayson]

This is the same discussion as "Ultimate Theory /
Theory of Everything".

Now, here as the thread is about order theory and
CH and so on, about that _alternative foundations
are parts of an integrative whole_ and _somehow
the model supports the extra_ then _theory bridges
these_ then that's a reasonable justification in
not so many words.

[William Elliot]

CH is insignificant to GCH.
GCH is the true way for as Occam admonishes,
"don't multiply entities beyond necessity."

What need is there for uncountable numbers smaller
than the continuum? Can you give an explicit example?
An uncountable subset of the reals with fewer numbers
than the real line, for example?

Oh yes, such fantasies are used to entertain the minds
of idle mathematicians ad infinitum. Compare with:

Vishnu sleeping on the eternal ocean of nonexistence
dreaming of countless Bramha worlds.

Is the intersection of theology and the transfinite not empty?

[mitch]

I will make some clarifications to what I have said
and to what you have said when I have more time. I
have some questions.

For the moment, though, it is precisely the semantics
surrounding the continuum hypothesis to which I am
objecting.

One of my early motivations had been to develop axioms
which would permit denotation of a universal set so
that the universal quantifier in set theory would be
meaningful. As it stands, it seems that such a universe
must be a set by being self-membered. I tried the usual
notion of the reflexive closure for the subset relation
and it leads to a contradiction just like naive set
theory.

What one would take for the universal class would
be given by

Ax( x = V() <-> Ay~( x = y <-> ( y in x -> ~( y in y ) ) ) )

This seems to not lead to contradiction.

The notion of "proper classes" not in the theory
determining truths in a theory from which "proper
classes" are specifically excluded is nonsensical.
I have a fundamental objection to this.

It arises because the naive notion used to formulate
Russell's paradox may simply be incorrect and
because the treatment of identity statements with
the form

x = x

as always true. The latter allows one to speak
of objects not in the theory as if they have
existential import with respect to the theory.

But, as I stated in what you snipped, it seems
that it is the subtle relationship between the
theory and the logic that must be adjusted
because logic has something to say about identity
statements.

mitch

[FredJeffries]

On Wednesday, March 8, 2017 at 3:07:07 PM UTC-8, mitch wrote:
>

> For me, the motivating problem is the continuum
> hypothesis.
>
> Its independence rests with our understanding of
> metatheory.

I do not pretend to understand what you are talking about, but I am curious: you seem concerned about the independence of the continuum hypothesis. Do you have a similar concern about the independence of the parallel postulate?

[Ross A. Finlayson]

One of the reasons for model theory is to talk about
incompleteness, and inside and outside the model as
reflect what are otherwise plainly axiomatic (and
non-axiomatic, but structurally evident as shewn into
existence by incompleteness) derivations as of the
class of all the derivations of statement of theorems
of the theory (theories) of the model (models).

This applies even to neatly basic theories of arithmetic
and as of extensions even of finite groups and so on
that in induction over the indices model arithmetic
and become fulfilling of Goedel's completeness and
incompleteness, "Goedel's Russell-ization" (or to
keep some of the weight off of Russell, "Goedel's
extra-ordinary theory").

Then, eventually some structure that is actually
Goedel's extra-ordinary is also the same thing as
its model, about where model theory is re-united
as logical theory, because it doesn't simply exist
as a manner of speaking about consequences of the
incompleteness of Goedel.

So: Goedelize, then finish it.

Good luck with that.

[Ross A. Finlayson]

(Grappling with the extra-ordinary of comprehensive fundamental
theory has that eventually the conscientious formalist does
acknowledge what one's talking about.)

Similar to letting, relaxing, or flexing CH, letting Post.5 or ||
isn't so much "anti-" or "non-", as: "extra-" or "super-" (in the
sense of the relations, not the property). The "parallel lines"
don't meet anywhere: except "at infinity" (or the bounds), in
these "non-Euclidean" (elliptic, hyperbolic) geometries. These
geometries vary in how other properties (as postulated) change
to so reflect the maintenance of otherwise the relations (of
shapes and paths in geometry). Here it's the emergent properties
of the derived structures (within the models) that are so affected.

Now, these geometries might define manifolds besides spaces, with
otherwise a usual perspective that Euclidean geometry is a manifold
of objects in space quite generally (as of the origin as also the
orthnormal vector basis) here that these models of cardinal arithmetic
define hierarchies and ranges, or as above about the differences among
succession and progression. About an analog of an origin in these
non-Euclidean spaces, the utility of them (as in the applied in models
of physics) is to maintain the results of transport within the manifold
as encompassing all the necessary book-keeping as of transport within
the space (eg the Minkowskian and space-time, in the applied models,
and even if the Minkowskian is the book-keeping of effects as would
occur that again becomes the super-classical not the non-classical,
trading convenience in notation for clarity in effect.)

[mitch]

On 03/08/2017 08:32 PM, Jim Burns wrote:

< snip >

>
>

> Something I still feel confident about, though, is that
> _if I say_ Ax, ~(Sx = 0), then _I have said_ Ax, ~(Sx = 0)
> I would like mathematics and logic to be grounded in
> speech acts (syntax) instead of facts (semantics).
>

You may correct me on this. I shall give you a little
time to investigate it for yourself rather than trying
to provide any links.

My understanding of the expression "speech act" is that
it falls under the notion of "pragmatics".

Although pragmatics did not originate with Carnap, he is
the one that made others aware of it. The basic idea
is that syntax is independent from the language user
while pragmatics takes the language user into account.

When I make comments about "mathematics-as-religion" it
is because of the portrayal of mathematics solely in
terms of a "syntax/semantics" dichotomy. As a person
with a degree in mathematics, I find claims that the words
I use are meaningless to be little more than insults.
Talking about "mathematical universes" (Tegmark) or
"believing axioms" (Maddy) or discussing "abstract objects"
as existents outside of space and time has the effect,
in my opinion, of declaring my understanding of mathematics
as being equivalent to a belief in a deity.

By contrast, I am more than happy to discuss such matters
in the context of the triad consisting of pragmatics, syntax,
and semantics.

Mr. Percival once made the observation that Russell did
not provide a semantic theory. This is true. But, Russell
did have a theory of knowledge in which the interpretation
of the demonstratives "this" and "that" involved ostensive
language acts. The formalization for demonstratives with
a semantic theory did not appear until Kaplan's work.

But, there is a community of analytical philosophers who
will not admit pragmatics into any discussion for the
foundations of mathematics. Very often, they cite Frege's
arguments against "psychologism". They are citing a man
who retracted his logicism at the end of his career and
then suggested that all mathematics is based upon geometry.

Setting Frege's opinion aside for the moment, if you find
that "speech acts" do fall under "pragmatics", then perhaps
you will entertain the idea that we share opinions closer
in kind than what seems to be the case at this moment.

mitch

[mitch]

On 03/08/2017 08:32 PM, Jim Burns wrote:

> On 3/8/2017 6:07 PM, mitch wrote:
>> On 03/07/2017 12:15 PM, Jim Burns wrote:
>
>>> Maybe I'm not understanding (I wouldn't be surprised),
>>> but I think you (mitch) are trying to explore primitive
>>> _identity_ as opposed to _indiscernability_ . I don't
>>> want to persuade you to give up (if I do understand),
>>> but, in my opinion, indiscernability is the best that
>>> we can do _in principle_ .
>>
>> You are very close here. And, I agree completely
>> with your statement.
>>
>> For me, the motivating problem is the continuum
>> hypothesis.
>
> We may be heading in different directions from this point
> on. To me, the continuum hypothesis doesn't look
> foundational at all. It may be that you and I are trying
> to answer different questions with our respective
> foundations.
>

I would like to share a quote from Kleene's "Introduction
to Metamathematics". Before reading it, consider the
questions,

"What is mathematics?"

"What is the foundation of mathematics?"

contrasted with the question,

"What can be certain?"

And, please keep in mind that the string of "crises"
that arose in the nineteenth century had arisen largely
because of people's beliefs about mathematics.

Here are the four paragraphs from Kleene:

< begin quote >

"Since Leibniz (1666) conceived his idea of a universal
characteristic, formal logic also has been receiving a
symbolic treatment, with the aid of mathematical techniques,
under DeMorgan (1847, 1864), Boole (1847, 1854),
Pierce (1867, 1880), Shroeder (1877, 1890-1905) and others.

"These concurrent developments have finally led to
formalizations of portions of mathematics, in the strict
sense, by Frege (1893, 1903), Peano (1894-1908), and
Whitehead and Russell (1910-1913). (The method of making
a theory explicit which we have been describing is often
called the _logistic_ method.)

"To Hilbert is due now, first, the emphasis that strict
formalization of a theory involves the total abstraction
from the meaning, the result being called a _formal system_
or _formalization_ (or sometimes a _formal theory_ or _formal
mathematics_ ); and, second, his method of making the formal
system as a whole the object of a mathematical study called
_metamathematics_ or _proof theory_.

Metamathematics includes the description or definition of
formal systems as well as the investigation of properties
of formal systems. In dealing with a particular formal
system, we may call the system the _object theory_ and
the metamathematics relating to it its _metatheory_."

< end quote >


Now, unless I am misreading this passage, the distinction
between an "object language" and a "metatheory" is a
fundamental presupposition of "metamathematics" that is
not "mathematics". It is, in fact, so fundamental that
it is recognized by stipulation.

By contrast, "mathematics" is concerned with what is
happening with the "axioms", "theorems", and "proofs"
_within_ the object language.

So, when I come here trying to talk about axiom systems
arrived at by considering logical relationships between
the antecedents and consequents in the object language,
I am -- to the best that I can tell -- talking about
"mathematics", foundational analysis within "mathematics",
and not "metamathematics".

I could say more here based on a handful of other quotes
from Kleene. But that would simply complicate matters.

What I would like to point out, is that the inductive
order relation I use,

AxAy( x < y <-> ( Az( y < z -> x < z ) /\ Ez( x < z /\ ~( y < z ) ) ) )

may be interpreted in a manner that leads to arithmetic
directly (proper divisor). In the other direction, it
grounds a theory of classes that had been motivated by
topology, which is also known as "rubber sheet geometry"
when described informally. It is not a notion of "class"
in the sense of a logicists paraphrases. Rather, it is
a notion of class arising solely by considering the system
of "pure sets" under Zermelo-Fraenkel set theory and the
idea that a set is simply a class that is the element of
a class. My point here is that the membership relation --
in its "topological guise" -- is fundamentally an incidence
relation.

So, if you wish to dispense with logicism by virtue of
the kinds of statements found in Kleene's discussion of
the various "-isms", my approach is "restoring" the
traditional notion of "mathematics" with respect to
arithmetic and geometry.

And, in that traditional structure, logic is not
mathematics.

mitch

[Ross A. Finlayson]

(Just a comment about "mathematical universe hypotheses",
is that a mathematical platonist's view can be seen instead
of a physical scientist's view, to satisfy that mathematics
is as or more fundamental than physics, so you can have a
"mathematical universe hypothesis" and keep it, too. Then,
as that might reflect on platonism, there are strong grounds
available to reason that fundamental and primary mathematical
objects are platonist without the necessity of stretching to
"faith", instead that the platonist belief is based on "reason".
Then, that's even not incompatible with "faith"-ers or the
"show me" types, in terms of that "G-d's own theory" would be
the "perfect science" and for the platonist those are all one
and the same as a "mathematical theory of everything".)

[Ross A. Finlayson]

Re: "metamathematics", that relates to this notion that:
a complete theory doesn't need a model, that it is its
own, here about mathematics in mathematics (in logic,
in the philosophy of reasoning, for a usual rationale).

This is with ideas following Goedel's "Completeness AND
Incompleteness" that both the theory's model contains
itself and the theory also does, here about the bridge
(and the building of it) between a unity and a whole.

[mitch]

On 03/09/2017 04:50 AM, mitch wrote:

The formula below needs a correction.

>
> What one would take for the universal class would
> be given by
>
> Ax( x = V() <-> Ay~( x = y <-> ( y in x -> ~( y in y ) ) ) )
>
> This seems to not lead to contradiction.
>

Ax( x = V() <-> Ay~( x = y <-> ( y in x /\ ( y in x -> ~( y in y ) ) ) ) )

When working with a lot of complex formalizations,
one begins recognizing certain "idioms". Here
the idiom would be

A /\ ( A -> B )

because its negation would be

~A \/ ( A /\ ~B )

So, assume 'x = y' in the formula above. Then,
if the universe is self-membered, one has

y in y /\ ~~( y in y )

y in y /\ y in y

The possibility that

~( y in y )

is supported. But, to be the "set universe" under the provision
that a set is a class which is the element of a class, it can
only fall under the quantifier if it is self-membered.

mitch

[mitch]

On 03/09/2017 03:37 AM, William Elliot wrote:

> CH is insignificant to GCH.

The continuum hypothesis is true under the
axiom of determinacy without reference to
the generalized continuum hypothesis.

Arguably, a mathematician might justify taking
the continuum hypothesis to be true on the
basis of results in transfinite dimension
theory. There is no transfinite dimension
greater than or equal to the first uncountable
infinity.

Note, however, that the invariance of topological
dimension relies upon a continuity assumption.

With respect to topology and first-order logic,
Flum and Ziegler developed a notion of logic
whose models coincide with those of first-order
logic on discrete and trivial topologies.

Because of this coincidence, formalizations
in mathematics whose underlying notion of an
individual is based on a convergent filter
is always interpretable as a first-order
theory.

Set theory over pure sets is different.

Here is a "classical" universe of discourse,


philosophers

|-----------------------------------|
| |
| |
| |
| Plato |
| * |
| |
| |
| |
|-----------------------------------|




In a theory of pure sets, each set provides
for a separation of the universe discourse,

classes

|-----------------------------------|
| |
| |
| |
| A |
| * A |
| |------| |
| | | |
| |------| |
| |
|-----------------------------------|

The "individual" A denotes the "collection
of individuals" A. And, this is within the
scope of the theory.

Every set is a class. Hence, the universe is
labeled "classes". It is presumed that a
set is a class which is an element of a class.

As a class, the empty set as an "individual"
denotes all of the classes outside of the
universe,

classes

|-----------------------------------|
| |
| |
| |
| null |
| * |
| |
| |
| |
| |
|-----------------------------------|

Those classes, of course, are non-existent
because of what is meant by a universe of
discourse. Hence, the empty set has no
members and no representation as a
"collection of individuals" that acts to
separate the universe.

As a class, the universal class as an
"individual" denotes the "collection of
individuals" corresponding to all of
the classes,

classes

|-----------------------------------|
| |
| |
| |
| U |
| * |
| |
| |
| |
| |
|-----------------------------------|

Because it is "all", this "collection
of individuals" does not act to separate
the universe.

And, admitting it as a self-membered
class, it is a set. Hence, it may fall
under a universal quantifier interpreted
quantitatively as a parameter over sets.

The formalization problem is to more
closely reflect the topological form. I
have no inclination to treat the universal
class as a "Quine atom". But, other than
that one wants a true membership predicate
to reflect a descending chain as if it
were part of a convergent filter.

mitch

[mitch]

Because of the whole nonsense about "formalist on Sunday",
philosophers such as Quine have imbued the deductive calculus
with "ontology" and "ontological commitment". Undoubtedly,
I will attract some lecture about "bad philosophy" when my
sole objective is to formulate much clearer lines between
mathematics and philosophy.

If you read the section on deflationary nominalism,

https://plato.stanford.edu/entries/nominalism-mathematics/

you will find that this account makes a clear distinction
between "ontological commitment" and "quantifier commitment".

I have no problem with first-order logic being a criterion
for "ontological commitment". But, the formalizations should
be such that "mathematics" is hypothetical so that there can
be no question of vagueness over "quantifier commitment" and
"ontological commitment".

You will find that the authors want to make your argument.

I seek something stronger.

mitch

[mitch]

No.

Whether or not a pair of definitions are
equivalent in a theory is different from
making claims about "truths" based on elements
not in the theory and, further, stipulated to
not be in the theory.

In Euclidean geometry, "equidistant" and
"non-intersecting" correspond. That correspondence
is what is broken.

But, here is a cute thought.

Consider the iteration of "units" for some constructive
notion of numeral (Hilbert's metamathematics, Markov's
constructive arithmetic, WM's monotonic enumerations).

| | | ...

We say they are "intuitively" the same because they
have "the same shape".

What geometry is characterized by "rigid motion"?

Why don't the arguments against "mathematical
intuition" apply to modern views as they had been
applied in the nineteenth century?

And, at what point did our physicists determine
the actual geometry of the universe so that we
can know which two symbols in distinct spatial
locations actually are "the same shape"?

Such is the nature of "rhetorical truth" obtained
through "publish or perish".

mitch

[George Greene]

On Saturday, March 11, 2017 at 5:22:56 PM UTC-5, mitch wrote:
> Every set is a class. Hence, the universe is
> labeled "classes".

Are any of these classes proper?
Are any of them too big to be sets?

The universal class IS NOT a set.
Good grief. It is the archetypical NON-set.
By "universal class" you WOULD HAVE to mean, in this
context, the class of ALL SETS, NOT the class of all classes!

[William Elliot]

On Sat, 11 Mar 2017, mitch wrote:

> On 03/09/2017 03:37 AM, William Elliot wrote:
>
> > CH is insignificant to GCH.
>
> The continuum hypothesis is true under the
> axiom of determinacy without reference to
> the generalized continuum hypothesis.

No thanks, AD is anti-choice.

> Arguably, a mathematician might justify taking
> the continuum hypothesis to be true on the
> basis of results in transfinite dimension
> theory. There is no transfinite dimension
> greater than or equal to the first uncountable
> infinity.

Use Occams Razor for that clear thinking feeling.

> Note, however, that the invariance of topological
> dimension relies upon a continuity assumption.
>
> With respect to topology and first-order logic,
> Flum and Ziegler developed a notion of logic
> whose models coincide with those of first-order
> logic on discrete and trivial topologies.

Do, as a concession to my poor wits, Lord Darlington, just explain
to me what you really mean.
I think I had better not, Duchess. Nowadays to be intelligible is
to be found out. -- Oscar Wilde, Lady Windermere's Fan

[mitch]

On 03/09/2017 02:43 PM, FredJeffries wrote:

This is a good question to which I gave a bad
reply.

I will reproduce a quote from Aristotle below. Where
he speaks of "known without qualification" he is referring
to how we use universal quantifiers. When he speaks of
"known better by us" he is speaking of how we understand
the world through perceptions. This may be considered in
relation to existential quantifiers in the sense of a
chair in the room being a witness to "There is a chair
in the room".

Aristotle will also be speaking of "essence". This has
been considered problematic because of its relationship
with his metaphysics. You may, however, consider an ordered
sequence of formulas in which some of the formulas are
definitions for the same thing. Then, the first such
formula becomes the "essential definition" in that context.
Absent the metaphysics, "essence" may be understood as
saying that a collection of definitions is a pointed
set (or a collection of terms in an equivalence class
is a pointed set).

Consequently, the metaphysical import of "essence" will
be irrelevant for what I am trying to explain. Its relevance
lies with how it corresponds to the use of definitions.

What Aristotle is describing in the excerpt below is a
"logical aesthetic". It may not be exactly the same as that
among modern logicians. But, since the statement involves
the discussion of geometric figures, those parts of it have
relevance to how convergent topological filters relate to
logical individuals in modern mathematics. But, the modern
"logical aesthetic" proclaims topological notions to be
inadmissible as a "second-order" construct.

At one point in the excerpt, Aristotle writes,

< begin partial quote >

"We must realize, however, that someone who offers
this sort of definition cannot possibly reveal the
essence of the thing being defined, unless the same
thing turns out to be both better known to us and
better known without qualification."

< end partial quote >

What I am talking about is that a slightly different
arrangement of axioms -- made possible only by the
claim that a theory of pure sets suffices for the
practice of mathematics -- will admit this kind of
coincidence.

Then the question of whether or not the continuum
hypothesis is independent remains to be decided. In
all likelihood, my use of inductive axioms will exclude
the forcing methods of Cohen.

mitch

here is the excerpt:


< begin quote >

"Whether or not someone has defined and stated
the essence is to be examined on the following
grounds.

"First, we should see whether he has constructed
the definition out of things that are prior and
better known. For a formula is supplied to give
knowledge, and we gain knowledge not from just
any old thing, but from things that are prior and
better known, as is true in demonstrations -- for
that is the character of all teaching and learning.
Hence it is apparent that whoever fails to define
through these things has not given a definition
at all.

"[...]

"The objection that the formula has not been stated
through better known things can be understood in
either of two ways: either that it is composed of
things less well known without qualification, or
that it is composed of things less well known to
us -- for either case may arise. The prior is
better known without qualification than the
posterior. The point, for instance, is better known
than the line, and the line than the plane, and
the plane than the solid, just as the unit is
better known than the number (since the unit is
prior to any number and is the principle of
number); the same is true of the letter and the
syllable. In the case of what is better known
to us, by contrast, the opposite is sometimes
true; for the solid is more readily available to
perception than the other things, and the plane
more than the line, and the line more than the
point. For most people come to know these more
readily perceptible things first, since any sort
of intellect can learn about them, whereas it
takes a superior and exact intellect to learn about
the things that are naturally prior.

"Without qualification, then, it is better to seek
knowledge of the posterior things through the prior
things, since that is a more scientific procedure.
Still, in dealing with people who are incapable of
acquiring knowledge through these prior things, it
is presumably necessary to construct an account
through the things known to them. Definitions of
this sort include those of the point, the line,
and the plane. For all these reveal the prior
through the posterior -- it is said that a point
is the limit of a line, a line of a surface, and
a surface of a solid.

"We must realize, however, that someone who offers
this sort of definition cannot possibly reveal the
essence of the thing being defined, unless the same
thing turns out to be both better known to us and
better known without qualification. For a correct
definition must be given through the genus and
differentia, and these are better known without
qualification and prior to the species; for the
destruction of the genus and the differentia involves
the destruction of the species, so that they are
prior to it. They are also better known. For it is
necessary that if the species is known, the genus
and differentia are known (for example, someone who
knows man also knows both animal and terrestrial),
but it is not necessary that if the genus or the
differentia is known, the species is also known;
and so the species is less well known.

"Moreover, those who claim that these definitions
based upon what is known to each person are really
definitions will end up saying that there are many
definitions of the same thing. For in fact different
things are better known to different people, not the
same things to everyone; and so a different definition
will have to be provided for each person, if
definitions ought to be constructed from things
known to each person."

Topics 141a24

Aristotle: Selections
Terrence Irwin and Gail Fine
Hackett Publishing, Indianapolis/Cambridge, 1995

< end quote >

[mitch]

On 03/09/2017 02:43 PM, FredJeffries wrote:

> On Wednesday, March 8, 2017 at 3:07:07 PM UTC-8, mitch wrote:
>>
>> For me, the motivating problem is the continuum
>> hypothesis.
>>
>> Its independence rests with our understanding of
>> metatheory.
>
> I do not pretend to understand what you are talking about,

I hope you will recall a thread in sci.math some time ago
in which the expression "number theory" had been repeatedly
used with respect to Peano arithmetic. You chose to make a
post pointing out that you had had some classes in "number
theory" and that little of the material, if any, came from
Peano arithmetic. To the contrary, emphasis in number theory
is placed upon divisibility rather than succession.

With this in mind, consider what is done in typical mathematics
classes in a mathematics department.

If a professor proposes a definition,

"A commutative group is a group such that ... "

it will be followed by an example showing that the definition
is not vacuous -- that the definition can be substantiated
with an example.

And, if a professor says something like

"The identity element of a group is unique",

it will be followed by a proof of uniqueness.

So, definitions are substantiated and claims of uniqueness
are warranted.


Now, the following sequent,


|- Ex( Q(x) ), |- AxAy( ( Q(x) /\ Q(y) ) -> x = y )
-------------------------------------------------------
<| [ (iz)( Q(z) ) ]


is what motivated Abraham Robinson to title his paper,
"On constrained denotation".

On the bottom of the sequent is the syntax for definite
descriptions as he uses them. Specifically,

(iz)( Q(z) )

corresponds to the description and

<|

is an operator stating that the description is interpretable
as an individual.

For brevity, Robinson is omitting the reference to some
collection of extralogical axioms K. So, the bottom should
be

K <| [ (iz)( Q(z) ) ]

On the top of the sequent one has

|- Ex( Q(x) )

which should be

K |- Ex( Q(x) )

This is the claim that Q(x) will be substantiated under
interpretation.

On the top of the sequent one also has

|- AxAy( ( Q(x) /\ Q(y) ) -> x = y )

which should be

K |- AxAy( ( Q(x) /\ Q(y) ) -> x = y )

This is the claim that Q(x) describes a unique individual
under interpretation.

Where is this mathematical practice faithfully represented
in first-order logic?

What I believe captures this is an explicit definition such
as,

Ax( x = V() <-> Ay~( y = x <-> ( y in x /\ ( y in x -> ~( y in y ) ) ) ) )

an axiom asserting its definiendum such as

ExAy~( y = x <-> ( y in x /\ ( y in x -> ~( y in y ) ) ) )

with a semantic warrant for the logic

AxAy( Ez( x = z /\ z = y ) -> x = y )

supported by an axiom in the theory,

AxAy( x = y <-> Ez( x = z /\ z = y ) )

So, reversing the connections, the axiom,

ExAy~( y = x <-> ( y in x /\ ( y in x -> ~( y in y ) ) ) )

asserts the truth of the definiendum for the definition,

Ax( x = V() <-> Ay~( y = x <-> ( y in x /\ ( y in x -> ~( y in y ) ) ) ) )

In turn, that means that

k = V()

holds for some witness k. By the axiom,

AxAy( x = y <-> Ez( x = z /\ z = y ) )

one has

Ez( k = z /\ z = V() )

so that

k = V()

is an admissible identity statement for the logical calculus.

Now, of course, I should check that my definiendum may be satisfied
by no more than one witness before asserting the definition. And,
an axiom asserting existence is not needed if an existent can be
proven to exist.

Perhaps, I should have chosen a definition for the null class
instead of the universal class. I have just been working with this
definition recently.

The difference between this and first-order logic is that whatever
is explicitly definable is implicitly definable in first-order
logic. Objects simply exist because the quantifier rules are
independent of the rules for identity statements in the calculus.

mitch

[George Greene]

On Saturday, March 11, 2017 at 4:08:09 PM UTC-5, mitch wrote:

> Now, unless I am misreading this passage,

OF COURSE you are misreading it. Good grief.
WHY do you torture yourself like this? Philosophy is not necessary
at all to math. I say that as person with a philosophy degree.
Th philosophical questions are interesting in THEIR OWN right and
are helpful for organizing YOUR OWN thought. But they simply have no
bearing on any mathematical question whatosever. 1+1 will still equal 2
(or 0, mod 2) REGARDLESS of what "kind of thing" 1 is or isn't, or 0 is or isn't, or whether they (or 2) are "real". You lack all relevant PHILOSOPHICAL
intuition about what MATTERS!!!

> the distinction
> between an "object language" and a "metatheory" is a
> fundamental presupposition of "metamathematics"

It is NOT a pre-supposition, YOU IDIOT! It is A PRACTICE!!
Once the object theory exists, once you contemplate it as an entity,
then IT CAN BE STUDIED, and you can have a theory of that. Obviously
that is not the same thing as the original theory UNLESS the original
theory was SO comprehensive that it can be a "theory of everything", INCLUDING itself.

> that is
> not "mathematics".

IT *IS*SO*TOO* mathematics, *YOU*IDIOT*!!!!!
IT IS the study OF A MATHEMATICAL object! The object theory, thanks to the fact that theories nowaDAYS are SO HIGHLY formalized, IS ITSELF A MATHEMATICAL object!! THEREFORE, ANY study of it, INCLUDING "metamathematical" study, IS ALSO mathematical!!

> It is, in fact, so fundamental that
> it is recognized by stipulation.

It IS NOT "recognized by stipulation", YOU IDIOT.
IT IS *OBSERVED* as a practical FACT. It is JUST NOTICED that
people theorize ABOUT THEORIES, and thereby ACT ACCORDING to an object theory
/ meta-theory distinction. There IS NO NEED to "stipulate" anything and in fact, EVERYone remains free to stipulate THE PRECISE OPPOSITE of what you are talking about, namely, to say "I'm going to analyze first-order set theory in purely first-order set-theoretical terms", IF THEY WANT to. NOTHING IS STOPPING them, LEAST OF ALL some NON-existent "stipulation" that YOU DREAMED UP!!
Everybody CREATES the meta-theory / object-theory distinction SIMPLY BY DECIDING TO THEORIZE about the object-theory.

[FredJeffries]

On Wednesday, March 8, 2017 at 6:32:15 PM UTC-8, Jim Burns wrote:
>

> This concern I have about the nature of "facts" is a good
> background for my own foundation-like inquiries. We humans
> are a middle-sized species, somewhere between atoms and
> galaxies, and our size plays a role in what we consider
> "normal" behavior of our surroundings. When we explore outside
> our comfort zone, I'm not sure what some of the things we say
> mean, or if they are true or false, or if it is not a mistake
> to ask if they are true or false.

Not only our size, but our time-scale, our temperature range, pressures, the range of electromagnetic radiation to which we are sensitive, the possible patterns of the elements and chemicals with which we are made, ..., the fact that we use (linear) vocal communication, the fact that we are relatively free to move in two dimensions, rather restricted in a third, and pretty much imprisoned in the time dimension (except for memory), ..., the chemical, electromagnetic, and other laws which control the workings of our nervous system, the fact that we have a central nervous system, the fact that we (and our intelligence and language-ability) evolved in a communal situation, that fact that we are symmetric bipeds with opposable thumbs, ...

All of these influence what we regard as "facts" and how we deal with and manipulate those facts. Would beings with a different set of symmetries and three hands have come up with our true/false dichotomy or would they have a three-valued logic?

[FredJeffries]

On Thursday, March 9, 2017 at 2:50:28 AM UTC-8, mitch wrote:
>

> One of my early motivations had been to develop axioms
> which would permit denotation of a universal set so
> that the universal quantifier in set theory would be
> meaningful.

With respect, why do you WANT a universal set? Other than your stated tour-de-force of making the universal quantifier in set theory "meaningful"? That just pushes back to why should the universal quantifier be meaningful?

Doesn't the concept of an unbounded universal quantifier smack of hubris? Isn't the idea of wee humans having a complete theory-of-everything just silly?

[FredJeffries]

On Sunday, March 12, 2017 at 5:45:23 PM UTC-7, mitch wrote:
> On 03/09/2017 02:43 PM, FredJeffries wrote:
>
> I hope you will recall a thread in sci.math some time ago
> in which the expression "number theory" had been repeatedly
> used with respect to Peano arithmetic. You chose to make a
> post pointing out that you had had some classes in "number
> theory" and that little of the material, if any, came from
> Peano arithmetic. To the contrary, emphasis in number theory
> is placed upon divisibility rather than succession.

Indeed. Number theory had thousands of years of glorious history before Peano and Dedekind came up with the successor concept. Would anyone be so silly to say that Gauss was not a great number theorist because he didn't reduce his proofs back to the Peano axioms?

> With this in mind, consider what is done in typical mathematics
> classes in a mathematics department.
>
> If a professor proposes a definition,
>
> "A commutative group is a group such that ... "
>
> it will be followed by an example showing that the definition
> is not vacuous -- that the definition can be substantiated
> with an example.

Well, SOME professors may do it that way. But the first day of my first abstract algebra class the professor drew a square and discussed its symmetries. THEN he gave us the definition of a group.

Only my opinion, but it seems more natural to give several different examples of some abstract object (group, category, topological space, ...) and show that these seemingly different objects share an interesting common pattern.

It's like understanding that the cardinality five is a pattern common to that herd of five elephants and that bouquet of five daisies but is NOT common to that herd of five elephants and this herd of six elephants, even though, superficially, a herd of five elephants looks a lot more like a herd of six elephant than it foes to a bouquet of five daisies.

Spotting those non-superficial patterns: THAT is mathematics. IF one of those complex patterns can be summarized by a simple system of axioms, all well and good. But it's hardly necessary-- as far as I know, no one has yet come up with an axiomatic definition of "fractal".

But that is all probably irrelevant to the point you are trying to make...

[Ross A. Finlayson]

You mention hubris and it's fair, but,
you have a theory of things, right?

We can detail the logical (plainly logical
and any properly logical) properties of ...
theories and for all of them. Some such
simple principles of
causality and
non-contradiction
(eg as conservation then symmetry
and their reflections
diversity then variety) as then
constancy,
consistency,
completeness, and
concreteness
(constructively) begin to detail all
necessary properties of any theory of
everything, that due the uniqueness of
all its structural content is sole and
"the" theory of everything, that each
addresses in any consideration of
"the" theory of everything, and about
its singular "universe" of all things,
i.e. about itself.


Of the hubris to posit the existence and
nature of such a thing (eg, natural
philosophy) there's as much or more
(worse) hubris as suggesting the
violability of causation or that
the supreme (as omniscience or
omnipotence) wouldn't have a
perfect theory of everything.

Also the ubiquitous success of
mathematics (and physics) rather
demands that some noble intentional
ignorance for humility's sake is not
then respectful of whatever real laws
of nature there are.

Then, just like Hilbert, where the Hilbert
Programme's goal was a rigorous formal
abstract and symbolic foundation for
all of mathematics, with that being
the ultimate goal of the formalism
(and not just a formalism) then we
find Goedel, who accomplished two
primary goals in relation to his
theory, on theories.

Goedel showed completeness, of the regular, ordinary
theory, and also incompleteness. Understanding that
there is an ir-regular (not-necessarily-well-founded)
extra-ordinary theory, then, is a cognitive advance
just as from the bounded to unbounded and finite to
infinite, this regular to universal.

Goedel's is a modern take, with completeness of regular
theory (here set theory) for finite combinatorics (and
then ramified and stratified for regular comprehension
schema). That's where then the (technical) philosophical
canon since the Renaissance and Enlightenment periods
sits correctly right on top of the structures of Goedel's
theory on theories, which becomes a non-naive post-modern
retro-classical framework for theory as from first principles
as final cause of reason then to rationale, for rationality
(and even from the anthropocentric, objectively).


Theory without a universe in it becomes as barren (ultimately)
as numbers without a successor or collection. Still, denial
of the paradoxes of universal quantification is not their
resolution (and the resolution as rejection instead of
refusal must be so for the conscientious constant formalist).

Then for my own sake I arrived at the dually-self-infraconsistent
primary null and universe, with that the opposite of all the
statements and content of the theory is the same theory, so
resistant to meddling and derivative of its own properties
(and lack thereof) its structure, theory for everything (logical)
as theory of everything. This I call the "Null Axiom Theory"
or "A-Theory", not that it has no objects, but that they are
all that they are and must be (and that it is not hubris to
find them as they are, as it is to deny to refuse what they are).

A bibliography of this sort of development finds most of the
heavyweight philosophers and thinkers over time, for the technical
philosophy then logic quite canonically (and as references within
the resulting _structure_).

[FredJeffries]

On Saturday, March 11, 2017 at 2:45:36 PM UTC-8, mitch wrote:
> On 03/09/2017 02:43 PM, FredJeffries wrote:
> > On Wednesday, March 8, 2017 at 3:07:07 PM UTC-8, mitch wrote:
> >>
> >> For me, the motivating problem is the continuum
> >> hypothesis.
> >>
> >> Its independence rests with our understanding of
> >> metatheory.
> >
> > I do not pretend to understand what you are talking about, but I am curious: you seem concerned about the independence of the continuum hypothesis. Do you have a similar concern about the independence of the parallel postulate?
> >
>
> No.
>
> Whether or not a pair of definitions are
> equivalent in a theory is different from
> making claims about "truths" based on elements
> not in the theory and, further, stipulated to
> not be in the theory.
>
> In Euclidean geometry, "equidistant" and
> "non-intersecting" correspond. That correspondence
> is what is broken.

Likewise, in set theory with the (generalized) continuum hypothesis "power set" and "set of equivalent ordinals" correspond. THAT correspondence is what is broken.

[Julio Di Egidio]

That is very reasonable, very common, very easy to accept, utter bullshit.
Yes, "there are as many sensibilities and talents as there are people, but
there is one and only one rationality. The skeptics and the liars deny
that", and the rest just doesn't know any better. Note: same goes for the
aliens, that is: there *truths of rationality* which are indeed *universal*.

Julio

[FredJeffries]

On Sunday, March 12, 2017 at 5:45:23 PM UTC-7, mitch wrote:
>

> With this in mind, consider what is done in typical mathematics
> classes in a mathematics department.
>
> If a professor proposes a definition,
>
> "A commutative group is a group such that ... "
>
> it will be followed by an example showing that the definition
> is not vacuous -- that the definition can be substantiated
> with an example.
>
> And, if a professor says something like
>
> "The identity element of a group is unique",
>
> it will be followed by a proof of uniqueness.
>
> So, definitions are substantiated and claims of uniqueness
> are warranted.

Since I don't understand what you say below, I'll just prattle on. Interested readers may find the snippage at
https://groups.google.com/forum/#!original/sci.logic/3OQk9wzuTZ4/W3cf4RwoBwAJ

But, this "uniqueness" is not a global uniqueness. A group's identity element is unique WITHIN THAT GROUP. But different groups (may) have different identities.

Universal uniqueness belongs in metaphysics or theology or ontology, but not in mathematics. Mathematics involves finding common patterns in what were previously seen to be distinguished situations.

A toddler has not learned to count when she points out her blocks and says "one", "two", "three", .... She has learned to count when she ALSO points to chairs and says "one", "two", "three", ..., and when she points to her toys and says "one", "two", "three", ..., and when she points to her friends and says "one", "two", "three", ..., and when Cecily and Jack and Gwendolyn and Algy also point to some collections of objects and say "one", "two", "three", ....

Mathematicians have never needed to know "what a number is", although they haven't always realized it. It was after Dedekind, Frege, Peano, et al, came up with their "Was zind und was zollen die Zahlen" that mathematicians realized that it doesn't matter. No one knows WHAT a number IS and THAT'S A GOOD THING.

It only matters how numbers work. I think it was David Ullrich who a few months ago pointed out the modernness of Eudoxus's concept of incommensurables in that he tells us how to compare and manipulate them without actually saying what they are.

Peano's axioms are pretty worthless when studying number theory. They do not "define" THE NATURAL NUMBERS. But, they do define a natural number object which can be seen in other situations like Cantor's ordinal indexes for derived sets, and , most importantly, in recursive function theory which is one of the foundation of modern computation.

Category theory captures this with the notion of universal properties.

So, radical slogan: There are no individuals in mathematics

[Ross A. Finlayson]

I think that's an interesting deliberative process and
encourage you to continue.

(Then, see to it that how you make sense there combines
with all the other ways of making sense then of what
gives that they all make sense together.)

There are all kinds of platforms that need to be satisfied
by some sole foundation / true foundation, or in other
words all of them together.

You might find these lead to a strong platonism or a
strong (abstract) symbolism, then later that platonism
is a symbolism (and how it is).

[Julio Di Egidio]

On Friday, March 17, 2017 at 11:10:08 PM UTC+1, Ross A. Finlayson wrote:
> On Friday, March 17, 2017 at 12:17:28 PM UTC-7, FredJeffries wrote:

> > So, radical slogan: There are no individuals in mathematics

Which is just more bullshit, many thanks: numbers is the other side of the
coin of individuation.

> I think that's an interesting deliberative process and
> encourage you to continue.

What are you encouraging, the uneducated guessing??

Julio

[Ross A. Finlayson]

It's a long way to the top.

Might as well know how to find ways to get there.

(One should....)

[Julio Di Egidio]

On Friday, March 17, 2017 at 11:45:44 PM UTC+1, Ross A. Finlayson wrote:
> On Friday, March 17, 2017 at 3:37:03 PM UTC-7, Julio Di Egidio wrote:
> > On Friday, March 17, 2017 at 11:10:08 PM UTC+1, Ross A. Finlayson wrote:
> > > On Friday, March 17, 2017 at 12:17:28 PM UTC-7, FredJeffries wrote:
> >
> > > > So, radical slogan: There are no individuals in mathematics
> >
> > Which is just more bullshit, many thanks: numbers is the other side of the
> > coin of individuation.
> >
> > > I think that's an interesting deliberative process and
> > > encourage you to continue.
> >
> > What are you encouraging, the uneducated guessing??
>

> It's a long way to the top.

And a quick way to the bottom.

> Might as well know how to find ways to get there.
>
> (One should....)

One should realise that just as mathematics cannot be improvised, the same
goes for logic or philosophy or any other discipline.

Julio

[Ross A. Finlayson]

"Order theory" in foundations (or
very fundamentally) is a milieu
for establishing conditions and prospects
for derivability and completeness.

It's a milieu (or working background)
and example of a milieu, about structures
(as con-structions or the substrate) then
about the content (that it's the structure).

For then the usual question about whether
mathematics is invented or discovered, I
think it's discovered, but everyone has to
invent for themselves (eg, via emulation)
how to justify their understanding or find
the truth in it.

This is a continuing and ongoing process
with a result and goal of many being to
understand what "would be" the foundation,
among all these discoveries and inventions,
for what it is.

So, where something like set theory achieves
a "local maximum" of sorts, but there are
entirely different formalisms with eventually
the same content, maybe ("equi-interpretable")
or extra or less, they have different local
extremes in terms of global or total extremes.

Investing in only one formalism, or putting all
the eggs in the basket, has that eventually it
should be a component and in some "one true
formalism" or sole foundation / true foundation,
with acknowledging that you're going to need a
bigger basket, or just right, about where it's a
fixture in a foundation.

[George Greene]

On Wednesday, March 8, 2017 at 1:07:56 PM UTC-5, mitch wrote:
> The idea of substituting equals for equals can
> be found in Euclid. So, first-order substitutivity
> is actually "faithful" with respect to formalizing
> mathematics. This is not derived from second-order
> formulations.

OF COURSE IT IS, YOU IDIOT.

ANYthing that is a GENERALIZATION OVER ALL of first-order anything
IS INHERENTLY SECOND-order BY DEFINITION. The fact that you can
substitute equals for equals WITHIN ANY AND EVERY first-order
"thing" IS INHERENTLY AND DEFINITIONALLY A SECOND-order "thing".

More to the point, the fact that the relevant connective is a BIconditional --
Things are equal IF AND only if they CAN be substituted for each other IN ALL first-order "things" (contexts) WITHOUT CHANGING anything important (like truth-value) makes the notion of first-order equality itself INHERENTLY 2nd-order.

The foundational 0th-order notion is sort of equality "ad oculos" -- against the EYE -- just FROM LOOKING at it -- that occurs between (e.g.) an occurrence of the letter "a" in one part of a string and the "same" letter "a" in a different part. Coherence of the whole communication paradigm requires those "two tokens" of the "same" symbol to be recognizable as tokenS PLURAL of ONE SINGULAR symbol. But that sort of "recognition of atomic sameness" IS NOT what is happening with first-order equality and substitution.

ANYWHERE IN ANY first-order treatment OF ANYthing where you see an axiom-SCHEMA, where you see some big greek letter standing in for a formula, THAT IS INHERENTLY second-order. The first-order schema that you are looking at IS A DUMBED-DOWN APPROXIMATION (down to first-order) of the SECOND-order reality that is ACTUALLY INTENDED. This dumbing-down has some intriguing consequences so it has spawned a huge mathematical literature but you need to understand that the class of people who care about the class of models of first-order PA is MUCH SMALLER THAN the class of people who care about the natural numbers and THEIR properties.

[Ross A. Finlayson]

In the zero-eth order it does look like there's just one
value and it's the sole variable and the sole constant
and otherwise is this primordial ur-state of affairs
as Kant's "neumenon" and the "monad" and so on.

Then in a way higher orders are the consequences of
quantification, for a fundamental theory where that's
again through all items and that's again just first order.

That might seem flippant, that it's so simple that fundamental
theory is first order, and that the "higher order" is just a
convenience for notation and expression, that it is.

Something like Louwenheim/Skolem then just becomes another
example of an existence proof of a first order form for
anything, vis-a-vis things like "univalency" which are
claims (rather assertions or stipulations) of the ordinariness
of this that is instead part of an extra-ordinary universe,
arrived at deductively instead of via assertion.

[mitch]

On 03/16/2017 03:36 PM, FredJeffries wrote:
> On Thursday, March 9, 2017 at 2:50:28 AM UTC-8, mitch wrote:
>>
>> One of my early motivations had been to develop axioms
>> which would permit denotation of a universal set so
>> that the universal quantifier in set theory would be
>> meaningful.
>
> With respect, why do you WANT a universal set? Other than your stated tour-de-force of making the universal quantifier in set theory "meaningful"? That just pushes back to why should the universal quantifier be meaningful?

Because I am interested in a meaningful resolution of
the continuum hypothesis. I do not know what results
from the kind of changes that are involved.

More significantly, what I have learned along the way
gives me even more motivation.

Both Cantor and Frege had received inspiration from
Leibniz' work. The quotes at the top of this thread
show that the relevant relationship between Leibniz
and Aristotle had been an order-theoretic account.
With respect to Cantor's work, this had been expressed
topologically in his nested closed set theorem.

The wikipedia link,

https://en.wikipedia.org/wiki/Specialization_(pre)order#Definition_and_motivation

contains the statement,

< begin quote >

These restatements help to explain why one speaks of
a "specialization": y is more general than x, since it
is contained in more open sets. This is particularly
intuitive if one views closed sets as properties that
a point x may or may not have. The more closed sets
contain a point, the more properties the point has, and
the more special it is. The usage is consistent with the
classical logical notions of genus and species; and also
with the traditional use of generic points in algebraic
geometry, in which closed points are the most specific,
while a generic point of a space is one contained in
every nonempty open subset.

< end quote >


The structure of the set universe is that of a closure
algebra. It has this form because of the "genus and
species" account of logic. What the quoted text above
refers to as a generic point is what corresponds to a
denotation for the set universe. And, if you have such
a denotation, you may have an axiom of intersection
dual to the axiom of union. The principal reason one
cannot have that now is because intersection over the
empty set has no target. With a universe it
does.

The identity of indiscernibles is actually related to
the form of equivalence lattices. The bottom of such
lattices consists of a set of singletons.

By contrast, the axiom of choice is related to
Boolean lattices. This is recognized by how orthologics
related to simplexes express themselves as Boolean
lattices.

So, one simply describes a container with respect to
the "genus and species" accounts of Aristotle and
Leibniz. This will require associating a membership
relation with descending chains. An axiom like

AxAy( x in y -> Ez( x in z /\ ( x in z -> ( z ppart y \/ Aw( z ppart w
-> y ppart w ) ) ) ) )

would be part of achieving this. With respect to
this "genus and species" account, one introduces a
term for the set universe. Topologically, this is
done in terms of the particular point topology. If
you follow the links on generic points from the
Wikipedia page above, you should be able to get to
the particular point topology.

With this as a "container", one then builds normal
sets in the form of a cumulative hierarchy. But,
instead of "paraphrasing" the expression "is a
set", one will have idiomatic antecedents such
as

Av( ExEw( v part w /\ w ppart x ) -> EwEx( w sub x /\ Ay( y in w <-> Ez(
z in v /\ y in z ) ) ) )

The antecedent

ExEw( v part w /\ w ppart z )

is a betweenness condition that excludes the universe.

The condition

ExEw( w sub x /\ ...

is a betweenness condition stipulating how the set in
question must have an extensional relationship with a
superset.

In contrast with Frege, Cantor's idea had been motivated
by geometric ideas. And, when Lawvere began his work
on a category for sets, others in foundations pointed out
how his work had actually been closer to Cantor's ideas
with respect to the notion of invariance.

My interest may have begun with having a universal
set whose admission might change the axioms enough
to resolve an independent question. But, what I have
learned is that "traditional foundations" is little
more than a single-minded pursuit arising from the
arithmetization of mathematics.

I personally have no reason to accept the expungement
of geometry from mathematics just because of a logical
aesthetic promoted by a handful of analytic philosophers.

Their views would hold much more weight with me if
mathematicians arrived at their axioms by taping the
lectures they give in order to "paraphrase" their own
words into "formalizations".

Do you know any mathematicians who work that way?

mitch

[mitch]

On 03/16/2017 03:36 PM, FredJeffries wrote:

There are a few things I would like to say about
hubris, except that you are using it in a different
context.

I do not know if the universal quantifier and notions
of a complete-theory-of-everything are the same sort
of thing.

If you were to study set theory from Jech, at least,
you will find many statements that involve an ordinal
bounded above by another ordinal. This is just a
betweenness condition. Adding a denotation for the
universe would simply involve understanding the set
universe with respect to betweenness conditions
involving the set universe.

Now, I tried to formulate a system with the usual
notion of a universe as the reflexive closure of
the subset relation. It led to contradiction. It
could be my axioms. I believe, to the contrary,
that what is normally viewed as the set universe
is contradictory.

So, now I look at the set universe as a fixed point
characterized by self-membership. Such a universe
seems to not invite contradiction. Moreover, it is
compatible with anti-foundation set theories in
which well-founded sets are a subsystem.

My only sense of what I work on is that it will
constrain the model theory of set theory. I do
not see it in terms of any theory of everything.
Moreover, because the sentences by which I do
this cannot be used for urelements, they are only
applicable to how a theory of pure sets suffices
for the practice and study of mathematics.

With regard to a theory of everything, I am in
agreement with you. But, I have no sense of how
others understand mathematics as a conduit to
truth about reality. Even if that were the case,
it could only be realized through our cognitive
abilities. So, once brain science establishes
the forms associated with our interactions with
the world, you will have the same solipsistic
circularity that philosophers dread. And, as I
pointed out last year, brain science is presently
reaching such a situation.

mitch

[George Greene]

On Friday, March 17, 2017 at 11:36:45 PM UTC-4, Ross A. Finlayson wrote:
> That might seem flippant, that it's so simple that fundamental
> theory is first order, and that the "higher order" is just a
> convenience for notation and expression, that it is.

No, it isn't. Second-order really is different.
For one thing, first-order has a halfway tractable consequence relation (recursively enumerable) and second-order DOESN'T.
For another, diagonalization -- there really are MORE 2nd-order (as opposed to just more complicated, although that is true as well) things than first-order ones.

[George Greene]

On Wednesday, March 8, 2017 at 6:07:07 PM UTC-5, mitch wrote:

> For me, the motivating problem is the continuum
> hypothesis.

No it isn't.

>
> Its independence rests with our understanding of metatheory.

No, it doesn't. Regardless of anybody's metatheory, there exist models
of ZFC where the continuum hypothesis is true AND MODELS of ZFC where the
continuum hypothesis is false. If you actually knew or cared ANYthing about
meta-theory then you would have to be attacking the meta-theorectical CONSTRUCTION of one of these models. If the meta-theory that allows BOTH of them to be constructed is legitimate then the independence of the continuum hypothesis simply completely ceases to be noteworthy, or to be entangled with meta-theory in any way.

Unprovability-sentences in general are independent of the axioms that went into the proof-predicate, but but we NEED those axioms to be consistent (if we are using them), so we are actually always more interested in the models where the unprovability-sentences are TRUE than in the ones where they are false (despite the fact that the ones where they are false ALSO EXIST).

[mitch]

On 03/16/2017 03:36 PM, FredJeffries wrote:

There is something else I should say
about the universal quantifier.

Early on, I maintained that the
interpretation of quantifiers lies with
the rules of the deductive calculus. I
had been surprised when I recently
discovered that Martin-Lof wrote a paper
with that conclusion. It is being used
by the HOTT community in arguments with
traditional foundations.

But, of course, there is a traditional
view arising from traditional philosophy,
bad or good.

In a somewhat civil discussion with
Mr. DiEgidio last year, there had been some
confusion over uses of the expression,
"inductive". I had been using it in the
context of certain mathematical texts, while
Mr. DiEgidio had been using it in a more
philosophical context. He advised me to look
at the last chapter of Strawson's book on
logic. I did.

There is no justification other than belief
for taking a universal quantifier to be definite.
This is as clear from Aristotle as it is with
Strawson's exceptional analysis leading into a
discussion of probabilities governing the
formation of universals. I concede to Mr. DiEgidio's
objections on the basis of his usage for "inductive".

Nevertheless, I see no reason why concerns over
"the world" in actuality apply to the notion of
a theory of pure sets being sufficient for mathematics.
One may dispute that a theory of pure sets suffices.
That is what I have learned since responding to
Mr. Greene's flames by studying "how we got to
now" through texts on philosophy and logic. But,
to the extent that one is focused only on a theory
of pure sets, the entire matter of what to believe
about universal quantifiers seems silly. It
speaks to Frege's objection: show me a forest
without trees.

Ultimately, this is why I finally found myself
committed to offering a different logic. Mathematics
is better portrayed as a hypothetical with a
non-truth-functional "If y exists..." than it is
equating mathematical language with common language
and asking what one may believe about word meanings.

mitch

[mitch]

On 03/16/2017 04:12 PM, Ross A. Finlayson wrote:
> On Thursday, March 16, 2017 at 1:36:29 PM UTC-7, FredJeffries wrote:
>> On Thursday, March 9, 2017 at 2:50:28 AM UTC-8, mitch wrote:
>>>
>>> One of my early motivations had been to develop axioms
>>> which would permit denotation of a universal set so
>>> that the universal quantifier in set theory would be
>>> meaningful.
>>
>> With respect, why do you WANT a universal set? Other than your stated tour-de-force of making the universal quantifier in set theory "meaningful"? That just pushes back to why should the universal quantifier be meaningful?
>>
>> Doesn't the concept of an unbounded universal quantifier smack of hubris? Isn't the idea of wee humans having a complete theory-of-everything just silly?
>

< snip >

>
> Then, just like Hilbert, where the Hilbert
> Programme's goal was a rigorous formal
> abstract and symbolic foundation for
> all of mathematics, with that being
> the ultimate goal of the formalism
> (and not just a formalism) then we
> find Goedel, who accomplished two
> primary goals in relation to his
> theory, on theories.
>

< snip >

On my reading, Hilbert's statements about
why mathematics should have a formalist
attitude arise from the problem of applicability.
Hilbert is concerned that any contradictions
that arise in applications of mathematics not be
attributable to mathematics. Consequently, the
formalist attitude describes hypothetical objects in
relation, and, any purported objects (objects in the
sense of applications) that satisfy those relations
may enjoy the benefit of the mathematics associated
with that formalist system.

It is in the transition to metamathematics where
issues arise. Goedel has a grasp of formal systems
as syntactic systems like no one before him. His
completeness theorem is one means of understanding
non-contradictoriness. But, it does not advance
the problem of completed infinities which led
Hilbert to metamathematics. First-order logic and
its model theory still require that a term
interpreted as a completed infinity correspond with
a completed infinity.

There is a reason I posted a proof that the language
terms of a consistent theory satisfy the axioms of
a proximity space several years ago. Absent the
ability to materially demonstrate a completed infinity,
the best one can do is to formulate theories that
exemplify proximity spaces. First and foremost,
Hilbert's issue had been that the systems not generate
contradictions (which is not the same as believing
that they do not generate contradictions). To the
extent that set theory and logical language relate
to one another in a topological sense, that topological
sense may be used to describe a set universe based upon
the structure of a proximity space.

Now that I have passed through the "mereology" phase
of trying to understand how my axioms relate to
standard set theory, I have Csaszar's theory of
syntopogenous orders. Proximity spaces correspond to
biperfect syntopogenous orders. And, a set theory
formulated on that basis is closer to a consistent theory
than one which is not. There is no claim here about
consistency in the sense of first-order logic. By
"closer to a consistent theory" I mean "has a structure
provably associated with a consistent theory". And, one
can hope that this suffices with respect to
non-contradictoriness.

mitch

[mitch]

That is why I realized I needed to
write something else!

Good for you catching me being
lazy and stupid.

mitch

[Ross A. Finlayson]

It rather seems you're doubting belief. Some have
that's not mathematical and it's not logical in
their philosophy where such things aren't matters
of belief. (This is for achieving "freedom from
desire".)

Restricting quantifiers is either restricting
quantifiers or it isn't. So, HTT as "the strength
of ZFC plus two inaccessible cardinals" expands to
restrict, as it were, but those non-set cardinals
do reflect being Cohen's dual models, here the
second as the proper class again, just like the
universe as would be self-referential as noted
above.

The goal is that because admitting that breaks
things, to figure out how instead there is
"symmetry flex" so it's the way of things.

Extremes or opposites in the classical are
often reflected in the models of the extra
and out and on through the structures of the
foundation, echoed as regimes of comprehension.
Here "induction" and "deduction" are courses as
among these, also "inherent" or "strong" properties
as variously bridge (or vault) or transfer over
the limits or boundaries of regimes of comprehension.

That's technical, indeed.

[mitch]

You will have to forgive certain "outdated" uses of
language here (described by others as "bad" philosophy),
but what you are saying looks a lot like ...


< begin quote >

"Philosophical knowledge is the knowledge gained
by reason from concepts; mathematical knowledge
is the knowledge gained by the construction of
concepts. To construct a concept means to exhibit
a priori the intuition which corresponds to a
concept. For the construction of a concept we
therefore need a non-empirical intuition. The
latter must, as intuition, be a single object, and
yet none the less, as the construction of a concept
(a universal representation), it must in its
representation express universal validity for all
possible intuitions that fall under the same concept.
Thus I construct a triangle by representing the
object which corresponds to this concept either by
imagination alone, in pure intuition, or in
accordance therewith also on paper, in empirical
intuition -- in both cases completely a priori,
without having borrowed the pattern from any experience.
The single figure which we draw is empirical, and
yet it serves to express the concept, without
impairing its universality. For in this empirical
intuition we consider only the act whereby we construct
the concept, and abstract from the many determinations
(for instance, the magnitude of the size and of the
angles), which are quite indifferent, as not altering
the concept 'triangle'."

Immanuel Kant
Critique of Pure Reason
A714, B742

< end quote >


< begin quote >

"... But although in such cases they have a common
object, the mode in which reason handles that
object is wholly different in philosophy and in
mathematics. Philosophy confines itself to universal
concepts; mathematics can achieve nothing by concepts
alone but hastens at once to intuition, in which it
considers the concept in concreto, though not
empirically, but only in an intuition which it
presents a priori, that is, which it has
constructed, and in which whatever follows from
the universal conditions of the construction must
be universally valid of the object of the concept
thus constructed."

Immanuel Kant
Critique of Pure Reason
A716, B744

< end quote >


When you characterize me as a "Kantian" it is
precisely because of a view of mathematics that
you just shared. Across my readings, it is Kant's
statements which most closely reflect my experience
in mathematics as presented by the mathematics
department at the University of Chicago. You, of
course, may see something else in these quotes. But,
if you see any reasonable analogy with what you just
wrote, then I will challenge you to find an opinion
closer than what Kant has written. I will gladly
study it and embrace it if I agree with you.

To be "Kantian" is not to reject logic as with some
interpretations of Brouwer.

< begin quote >

"Our nature is so constituted that our intuition
can never be other than sensible; that is, it contains
only the mode in which we are affected by objects. The
faculty, on the other hand, which enables us to think
the object of sensible intuition is the understanding.
To neither of these powers may a preference be given
over the other. Without sensibility, no object would
be given to us, without understanding, no object would
be thought. Thoughts without content are empty, intuitions
without concepts are blind. It is, therefore, just as
necessary to make our concepts sensible, that is, to add
the object to them in intuition, as to make our intuitions
intelligible, that is, to bring them under concepts.
These two powers or capacities cannot exchange their
functions. The understanding can intuit nothing, the
sense can think nothing. Only through their union
can knowledge arise. But, that is no reason for confounding
the contribution of either with that of the other. We
therefore distinguish the science of rules of sensibility
in general, that is, aesthetic, from the science of the
rules of the understanding in general, that is, logic."

Immanuel Kant
Critique of Pure Reason
A51, B75

< end quote >


On the other hand, seeing a relationship between topology
and logic through the identity of indiscernibles and
Cantor's theorem on closed nested sets compels me to
reject Skolemite mathematics and Goedellian metatheory
for a theory of pure sets.

mitch

[Ross A. Finlayson]

There are two senses of "regular" to consider,
regular in the sense of topology and
regular in the sense of well-foundedness
are not the same, indeed the first is the
dispersive uniformly while the second is
the reductive linearly.

In a regular topology you never know where you are,
in a regular progression you always know where you've been.

There are only sets in a "pure" set theory,
constants like 0 and omega are not (sets).

That you would reject Skolem and Goedel's extra
_after_ their acknowledgement is _restriction of
comprehension_ (with that what they "were", and
are, is courtesy comprehension and it's usual
expansion). You've established a stipulation
and it's not without a cost.

Quantification (here as ordering) builds and is
structure. This is back to the notions of
succession or collection as progression, then
for gathering or ranging as dispersion (and
all quite regularly).

[mitch]

On 03/17/2017 02:17 PM, FredJeffries wrote:
> On Sunday, March 12, 2017 at 5:45:23 PM UTC-7, mitch wrote:
>>
>> With this in mind, consider what is done in typical mathematics
>> classes in a mathematics department.
>>
>> If a professor proposes a definition,
>>
>> "A commutative group is a group such that ... "
>>
>> it will be followed by an example showing that the definition
>> is not vacuous -- that the definition can be substantiated
>> with an example.
>>
>> And, if a professor says something like
>>
>> "The identity element of a group is unique",
>>
>> it will be followed by a proof of uniqueness.
>>
>> So, definitions are substantiated and claims of uniqueness
>> are warranted.
>
> Since I don't understand what you say below, I'll just prattle on. Interested readers may find the snippage at
> https://groups.google.com/forum/#!original/sci.logic/3OQk9wzuTZ4/W3cf4RwoBwAJ
>
> But, this "uniqueness" is not a global uniqueness. A group's identity element is unique WITHIN THAT GROUP. But different groups (may) have different identities.

And, this is what is involved in Robinson's account.

A term introduced by a definite description is asserted
to be unique for that theory.

Metaphysical arguments that a definite description
cannot define an individual are ignored in favor
of stipulating that the system is characterized by
having a single individual (if uniqueness is confirmed
or axiomatized) with the properties of the description.

>
> Universal uniqueness belongs in metaphysics or theology or ontology, but not in mathematics. Mathematics involves finding common patterns in what were previously seen to be distinguished situations.
>

The "contradiction" yielding the empty set

null set = { x | x =/= x }

is based upon ontology.

> A toddler has not learned to count when she points out her blocks and says "one", "two", "three", .... She has learned to count when she ALSO points to chairs and says "one", "two", "three", ..., and when she points to her toys and says "one", "two", "three", ..., and when she points to her friends and says "one", "two", "three", ..., and when Cecily and Jack and Gwendolyn and Algy also point to some collections of objects and say "one", "two", "three", ....
>

See my response to Mr. Finlayson about how I
read Hilbert's formalism.

> Mathematicians have never needed to know "what a number is", although they haven't always realized it. It was after Dedekind, Frege, Peano, et al, came up with their "Was zind und was zollen die Zahlen" that mathematicians realized that it doesn't matter. No one knows WHAT a number IS and THAT'S A GOOD THING.
>

When you read Euclid, you have the definition,

< begin quote >

"A unit is that by virtue of which each of the things
that exist is called one."

< end quote >

People who have historically objected to this definition
sought other definitions for 'unit'. If you notice, it
uses a demonstrative ("that") and nothing which is now
called "mathematical logic" even addresses demonstratives.
However, demonstratives do have a logic and with a
semantics. Modern analytical philosophy will never admit
this to its studies because it falls under "pragmatics"
and they seek a mathematics which excludes the role of
language users.

I do not recall if Dedekind defined a unit. I do not
think so. He simply looked at a mapping from a set into
itself and assumed that a set is composed of individuals.

Cantor claimed that an ordinal sequence could be viewed
as a completed infinity. His revelation about units is
that any completed infinity could be taken as a new unit
for a new sequence. Hence, each completed infinity is
actually a different type. But, he also provided a polynomial
form through which the different types relate to one
another. This is in parallel with how Vieta transformed
geometric forms associated with dimensions into separated
terms in a polynomial. When you say it does not matter, one
thing that matters to some is that only Cantor's view leads
to the clear distinction between ordinal numbers and cardinal
numbers.

Frege defined a unit using logic by taking the extension
of self-contradictory descriptions. This extension is
empty since no object is delineated by a self contradicting
description. What is important -- and relates to how provability
based on the definiendum of a definite description serves
as an epistemic warrant -- is that the empty extension is
provably unique. Because of this provable uniqueness,
Frege could claim that the class of descriptions satisfied
by a single individual could serve as the logicist definition
of the number one.

Frege's method is precisely the one I described with
respect to substantiation and uniqueness. Robinson
shows the method to be applicable to Russell's theory
of definite descriptions.

Here is the paper where I learned about demonstratives,

https://www.phil-fak.uni-duesseldorf.de/fileadmin/Redaktion/Institute/Allgemeine_Sprachwissenschaft/Dokumente/Bilder/11_Kaplan__1978_.pdf

If demonstratives provide for a "relocatable" notion of
a unit as the basis for counting, then it is compatible
with your claim that one does not need to know "what a
number is".

You will find that Kaplan describes a different notion
of validity from the modal logic that had been standard
at the time. And, there is significant discussion of
definite descriptions at the end of the paper.

> It only matters how numbers work. I think it was David Ullrich who a few months ago pointed out the modernness of Eudoxus's concept of incommensurables in that he tells us how to compare and manipulate them without actually saying what they are.
>
> Peano's axioms are pretty worthless when studying number theory. They do not "define" THE NATURAL NUMBERS. But, they do define a natural number object which can be seen in other situations like Cantor's ordinal indexes for derived sets, and , most importantly, in recursive function theory which is one of the foundation of modern computation.
>

Yes.

< snip >

>
> So, radical slogan: There are no individuals in mathematics
>

When you counter a mathematical claim with a counterexample,
is such a counterexample definite? Have you described a
plurality of counterexamples or a singularly specific
counterexample?

mitch

[mitch]

That is the basic idea of what I wrote
elsewhere.

In so far as geometric notions ground "numerical
identity", geometric notions ground "numerical
diversity". So, the convergent filters of a
topology are the order-theoretic analogs to
interpreting an "edge" between two vertices
in a simple graph as a "diversity relation".

Well-foundedness gives you the upward constructive
account with objects from the universe of
discourse having relationships of prior and
posterior with respect to membership chains
as well as subset chains.

>
> In a regular topology you never know where you are,
> in a regular progression you always know where you've been.
>
> There are only sets in a "pure" set theory,
> constants like 0 and omega are not (sets).
>

That is where definability comes in. But, there are
objections to the identity of indiscernibles with
regard to such definitions. One ought not be able
to define an existent. That is why I had to look at
a logic with respect to which quantifier rules and
identity statements are not independent.

> That you would reject Skolem and Goedel's extra
> _after_ their acknowledgement is _restriction of
> comprehension_ (with that what they "were", and
> are, is courtesy comprehension and it's usual
> expansion). You've established a stipulation
> and it's not without a cost.
>

Correct.

Among other things, the model theory is constructive
if Robinson's views about a system where constants
are introduced through definite descriptions is
correct.

> Quantification (here as ordering) builds and is
> structure. This is back to the notions of
> succession or collection as progression, then
> for gathering or ranging as dispersion (and
> all quite regularly).
>
>

mitch

[Ross A. Finlayson]

The object that remains in the theory when there
aren't any more constants introduced attains the
properties of these constants (that the constants
wouldn't otherwise exist in the language of the
elements, or that they would).

Here I'm trying to convince you that the null axiom
theory has a primary element that is dually void
and universal, the component is its context, and
so on.

I'd plan to employ Kant to assist, but it's not just
"a" way to make a triangle, but all the ways, that
so is: its form. The line is defined by what it is,
and is defined by what it isn't, constructively either
way, and, both ways. The more fundamental the object,
the more often it appears, and the more mathematical
is is.

That is where courtesy Goedel (as about theories) and
Russell and Burali-Forti there's the non-well-founded
(anti-foundational, ir-regular, "extra"-"ordinary")
after the well-founded "ord"-inary, it's retro-classical
in the finding the classical means again while maintaining
all the modern machinery.

There's still though then, besides "completeness" to
consider, the "completeness of completeness" or
"repleteness" so that a deeper foundation (toward
a sole or "true" foundation, as compatible with a
mathematical universe and being scientific, yet all
utterly spare and neat) isn't just another "donjon of
detail", how it's the "tower of rain".

That's rather ambitious.


These days then it's about truth as the first conserved
quantity, rather one-sided and lacking detail in the
regular assortment of the dually-self-infraconsistent
primary ur-element of the null axiom theory. Leibniz
might've called it monadology, but I have all of modern
mathematics' result to employ.

I was deeply enough set that "infinite sets are equivalent"
to go through the establishment for all these concerns,
to the point not just where I think it might not be any
different, but that that's as different as it can be,
and no different. It doesn't matter whether I'm mistaken
that the primary element is either void or universal,
because that's right, that then indeed the closure
demands that's both.


Then the key is the tenuous establishment of the assortment
of machinery in all the regular, that given a chance establishes
the tension (here a gradient) to maintain the projection, via
the integrity of the regular and its own self-consistent
definition. Maybe that's too hopeful, but at least the
perceived structure is so justified.

There isn't really the non-logical then in the theory,
all of humanity's knowledge is really just a scratch of
a number, but the entirety can be so modelled in so many
conveyed terms. (This is that "strong platonism".) The
theory really is and has to be _all_ of everything, for
then a usual assignment of the Ding-an-Sich / noumenon /
monad / continuum, ... there may be alternatives here ...,
regular strong arithmetic theories, ..., marks on a page.

They're marks with meaning.

[mitch]

On 03/18/2017 03:52 PM, Ross A. Finlayson wrote:

< snip >

>
> Here I'm trying to convince you that the null axiom
> theory has a primary element that is dually void
> and universal, the component is its context, and
> so on.
>

I get that Ross.

The way I understand logical constants are through
a set of axioms. Each axiom is of the form,

A( B, C ) = D

if one replaces each element of that formula with
its de Morgan conjugate, the resulting formula,

a( b, c ) = d

is also an axiom.

When Frege defined his zero, it had been based upon
the identity of non-existents now understood in the
semantics of negative free logic.

Since one can define a null class as the least
element in an order, I turn around Frege's account
with respect to the non-existents in Zermelo-Fraenkel
set theory to describe a universal class within
which a null class may be order-theoretically
defined.

My metamathematics is based entirely upon dualities
associated with geometric contexts. The hard part
is identifying how to portray a symmetry as the
asymmetry needed to develop the mathematical system.

The toy theories at the top of this post are presented
as being symmetrical with one another in form. But,
they are asymmetrical because of interpretations
dictated by an interest in truth and extensional
mathematics.

I will prepare the subset of my sentences and the
needed proofs to include in this thread in the near
future.

In principle, the formulas

AxAy( x ppart y <-> ( Az( y ppart z -> x ppart z ) /\ Ez( x ppart z /\
~( y ppart z ) ) ) )

AxAy( x in y <-> ( Az( y ppart z -> x in z ) /\ Ez( x in z /\ ~( y ppart

z ) ) ) )

are syntactically parallel and may be interpreted
as expressing the same thing. Only further constraints
on the relations will associate the order relation with
the intensionality of "second-order" and the membership
relation with the extensionality of first-order
individuals.

Mr. DiEgidio has claimed that symmetry is uninteresting. But,
finding (or, attempting to find) justifications for how
symmetry transforms into asymmetry useful for describing
mathematics is part of what I am doing.

In the case of the duality associated with the logical
connectives, this begins with the biconditional. Its
possible truth tables can be arranged to correspond with
the incidence matrix of a tetrahedron. Had that arrangement
corresponded with the exclusive disjunction, then I would
think about a system where exclusive disjunction ought to
be taken as a primitive. I do not really care for what
the justification is, as long as it does not arise from
asking "what does this symbol mean"?

mitch

[Ross A. Finlayson]

This symmetry about the inverse (with the
inverse as rather fundamental) is one of these
"inherent" properties here with that there's an
inverse about the center, or a constant, besides
inverse about the extremes, or the gradient.

(Here the associated vocabulary is basically
as direct as I have here, that I would expect
to be enduring and immutable, constancy.)

Then the inverses of the constants are about
the participation of the objects as the elements
of the algebas of all the structures they are in
(with inversion and reciprocity and lack thereof).
There is a true memoryless symmetry there.
The inverse of the gradient from the extremes is
similar to inverting the tree of the types or
"inverting the diamond" as I described it before,
this is basically flipping all the 1's and 0's,
and the result is the same, where the key result
of the inverse of the constant is that
the result is different.

context:
conservation and symmetry (regular, contra the extra-ordinary)
constant:
diversity and variety (ordinary, contra the ir-regular)

The idea is that these are blindly interchangeable,
that emergent (analytic) are their properties.

constant <-> context (extremes)

Then, it's just one primary object suiting all
the purposes. The object in the universe is
simply its image, and strongly no different.

Then, these strong properties are being in all
these regimes (or here regular areas or regions),
where the regularity holds, and the property holds.

This property of inversion or something like continuity
(of various sorts...) can be identified this way as
concomitant what were otherwise the properties of the
properly logical axiomatically-defined objects: which
clearly form a much more compartmentalized or self-
contained (via definition) declaration of terms, than
"all the logical terms".

(That's rather "self-contained via definition" as restriction,
for the "self-contained via inclusion" as expansion, of
comprehension.)

Then as expected (as it were) the very property of definition
falls out and is trivial or vacuous because it's extreme or
total with this axiom-free definition-free logical system
(for axiomatic definition).

This then goes on with that some such resulting system as
so ubiquitous would also have to be "scientific" about the
reading of these things and understanding besides concepts
then to follow like the "metal" and "concrete" numbers.

The applied and all the utility is in the properly logical,
this is about philosophical support of the purely logical,
for various absolute or universal statements to have a
proper (and, pure, as it were) support or foundation.

Then it's a useful reference for abstract formalism,
then that also it helps establish the concept that
negation varies in: the opposite, the anti-, the non-,
and in Janus' introspection: being the same. It's
a way (and all the other question words) to flex
instead of fail.


Then the point I'd hope to lift out for the applied is
that it gives room for redefinition of numbers underneath
the standard (i.e. as fundamental) for the retro-fitting
of modern algebra's models with these more replete models
of continuity of the continuum of the real numbers (a line).
It's necessarily extra-ordinary for it to be ordinary (which
is completely relevant for a given regime or model of these
elements of the object). This is for a geometry of points
and spaces instead of points and lines, Euclidean in the
sense that there are the same results, but with different
objects and here plainly mental (abstract) beside physical
tools available. Then these poly- and pan-dimensional points
as elements of the geometry so compose variously then for
the effects in their systems (or algebras) as of numbers
that in the applied there is a reasonable framework for
the estimation of effect to so automatically equip the
physical theories with these properties so resulting from
theory about the numbers.

So, there's a point.

[George Greene]

On Saturday, March 18, 2017 at 12:17:38 PM UTC-4, mitch wrote:
> Consequently,

It does not matter what the following was a "conseuence" of.
AFTER the paradigm has been adopted, the appropriate adverb becomes
"Definitionally"...

> the formalist attitude

Which, again, TO A FORMALIST, AFTER the paradigm has been adopted, becomes
"the mathematical attitude"

> describes hypothetical objects in relation,

Exactly. If you are going to bother with the model/semantic
side of the theory (which you NEED NOT, AT ALL -- the completeness theorem
is a proof that first-order consequence, IF you commit the original sin of defining it in terms of semantics and all-model agreement, can DESPITE that definition STILL be reduced to something PURELY SYNTACTICAL -- then the "usual" method requires the model to consist of relations. An interpretation of the theory in the model associates every syntactic element of the theory/signature except the 0-ary functors (constants) with a relation, and "all the work" is done by the arrows doing the relating: the *particular* objects that *get* related, or that comprise the DOMAINS of the relations, ARE NEVER important.
People who (wrongly) try to philosophize about this flaunt THEIR OWN ignorance
of THE DIFFERENCE BETWEEN "don't-know" and "don't-care" non-determinisms.

> and, any purported objects (objects in the
> sense of applications) that satisfy those relations
> may enjoy the benefit of the mathematics associated
> with that formalist system.

You're still one step too committed to the objects: ANY OBJECTS PERIOD may enjoy the benefits. If there exist relations that can model the theory, then if the relations you are using don't HAPPEN to have these (ANY) objects (of YOUR ARBITRARY) choice in their domains, then you can just DEFINE SOME NEW relations that DO have those objects as their domain, and isomorphically model the theory with THOSE relations. There IS a model of Peano Arithmetic in which 0 is [interpreted as] your big toe and s(your big toe) is 1. There IS a relation that relates your big toe to 1.

> It is in the transition to metamathematics where issues arise.

Well, obviously, a lot of metamathematics and philosophy of math were both already performed, just to commit us to the paradigm above. Nevertheless, it remains the received paradigm, as far as mathematicians are concerned. If philosophers want to behave otherwise then they are going to have a hard time getting ANYbody else TO CARE.

[George Greene]

On Saturday, March 18, 2017 at 12:17:38 PM UTC-4, mitch wrote:

> It is in the transition to metamathematics where
> issues arise. Goedel has a grasp of formal systems
> as syntactic systems like no one before him. His
> completeness theorem is one means of understanding
> non-contradictoriness. But, it does not advance
> the problem of completed infinities which led
> Hilbert to metamathematics.

Hold UP. FIRST, YOU have to prove that THERE EXISTS A "problem with completed infinities". The modern position is that THERE IS NO problem with completed infinities.

> First-order logic and its model theory still require that a term
> interpreted as a completed infinity correspond with
> a completed infinity.

NO, THEY DON'T.
The modern paradigm of model theory does NOT require that ANY particular TERM correspond TO ANY particular thing. It is THE MAPPINGS that might be infinite. If addition is a function then it has an infinite domain so + has to be interpreted as some function-in-the-model that also has an infinite domain. But a FUNCTOR is NOT a TERM (unless it's a constant). 1+1 is a term. + is not a term. PA in fact HAS NO terms that are completed infinities, although the fact that simple infinite sets have finitary descriptions means that you can godel-encode or turing-encode or chinese-remainder-encode infinite sequences via FINITE terms IF YOU SO CHOOSE. This does NOT TECHNICALLY expand the model's domain to include actually infinite objects (infinite sets of finite numbers).
Oddly, however, 1st-order PA and Godel's investigations highlight the OPPOSITE problem, that the theory is not powerful enough to EXCLUDE actually infinite objects, DESPITE the fact that there ARE NO infinite Terms naming them.

[khongdo...@gmail.com]

On Saturday, 18 March 2017 18:50:54 UTC-6, George Greene wrote:
> On Saturday, March 18, 2017 at 12:17:38 PM UTC-4, mitch wrote:
>
> > It is in the transition to metamathematics where
> > issues arise. Goedel has a grasp of formal systems
> > as syntactic systems like no one before him. His
> > completeness theorem is one means of understanding
> > non-contradictoriness. But, it does not advance
> > the problem of completed infinities which led
> > Hilbert to metamathematics.
>
> Hold UP. FIRST, YOU have to prove that THERE EXISTS A "problem with completed infinities". The modern position is that THERE IS NO problem with completed infinities.
>
> > First-order logic and its model theory still require that a term
> > interpreted as a completed infinity correspond with
> > a completed infinity.
>
> NO, THEY DON'T.
> The modern paradigm of model theory does NOT require that ANY particular TERM
> correspond TO ANY particular thing.

Amen. Some people do forget that FOL language symbol should be distinct in role
from the object it symbolizes even if existentially both are the same. For instance,
one can take the term SSS0 itself to be an object but the language term SSS0 isn't
logically bound to symbolize itself: it could be taken to symbolize the term SSSSS0,
for instance.

> It is THE MAPPINGS that might be infinite. If addition is a function then it has an infinite domain so + has to be interpreted as some function-in-the-model that also has an infinite domain. But a FUNCTOR is NOT a TERM (unless it's a constant). 1+1 is a term. + is not a term. PA in fact HAS NO terms that are completed infinities, although the fact that simple infinite sets have finitary descriptions means that you can godel-encode or turing-encode or chinese-remainder-encode infinite sequences via FINITE terms IF YOU SO CHOOSE. This does NOT TECHNICALLY expand the model's domain to include actually infinite objects (infinite sets of finite numbers).

> Oddly, however, 1st-order PA and Godel's investigations highlight the OPPOSITE problem, that the theory is not powerful enough to EXCLUDE actually infinite objects, DESPITE the fact that there ARE NO infinite Terms naming them.

Amen, again. This also points out to a general weakness of the Induction Principle
as an absolute mathematical truth guidance: the range of Induction isn't long enough;
it's restricted to only what's symbolized-able by language symbols.

[Peter Percival]

khongdo...@gmail.com wrote:
> On Saturday, 18 March 2017 18:50:54 UTC-6, George Greene wrote:

>> NO, THEY DON'T. The modern paradigm of model theory does NOT
>> require that ANY particular TERM correspond TO ANY particular
>> thing.
>
> Amen. Some people do forget that FOL language symbol should be

> distinct in role from the object it symbolizes [...]

So there are no such things as term models?



--
Do, as a concession to my poor wits, Lord Darlington, just explain
to me what you really mean.
I think I had better not, Duchess. Nowadays to be intelligible is
to be found out. -- Oscar Wilde, Lady Windermere's Fan

[mitch]

As expected, the never ending subthread begins...

[mitch]

Mr. Greene, being a hateful bastard, understandably
ignored the expression "interpreted" in order to
spew his vitriol.

But, I am surprise that *you* failed to recognize that
I actually referred to an "interpreted term" because
you are so technically precise about everything.

mitch

[mitch]

Whoops!

I thought I was reading Nam's post...

Obviously, *you* being *I* did not fail
to recognize the expression "interpreted".

Silly me.

mitch

[khongdo...@gmail.com]

(Fwiw, you were too "sensitive": I didn't have you i mind specifically when
responding to Mr. Greene's post).

[mitch]

Thank you for the clarification.

mitch

[FredJeffries]

On Saturday, March 18, 2017 at 4:51:32 AM UTC-7, mitch wrote:
> On 03/16/2017 03:36 PM, FredJeffries wrote:
> > On Thursday, March 9, 2017 at 2:50:28 AM UTC-8, mitch wrote:
> >>
> >> One of my early motivations had been to develop axioms
> >> which would permit denotation of a universal set so
> >> that the universal quantifier in set theory would be
> >> meaningful.
> >
> > With respect, why do you WANT a universal set? Other than your stated tour-de-force of making the universal quantifier in set theory "meaningful"? That just pushes back to why should the universal quantifier be meaningful?
>
> Because I am interested in a meaningful resolution of
> the continuum hypothesis.

Which continuum hypothesis?

The ZFC background fairy-tale DOES give a resolution of its continuum hypothesis: it's undecidable. It is also undecidable within the framework of "The Three Bears"

The reason that's its undecidable in ZFC is not because there's no universal set. It's because WE DON'T KNOW WHAT A POWER SET IS. At least, we cannot specify it within the framework of ZFC. When we think we have one corner fastened down we discover that the other three corners are flapping up there in the wind.

[FredJeffries]

On Saturday, March 18, 2017 at 11:32:03 AM UTC-7, mitch wrote:

> The "contradiction" yielding the empty set
>
> null set = { x | x =/= x }
>
> is based upon ontology.

But { x | x =/= x } is not a valid specification of a set, using unbounded comprehension.

Rather, for each set A, {x in A | x =/= x} is a subset of A. And, by extensionality, for any two sets A and B, the empty subset of A is equal to the empty subset of B. So, within any set universe, there is a unique empty set.

And there is a plethora of set universes...

[FredJeffries]

On Saturday, March 18, 2017 at 11:32:03 AM UTC-7, mitch wrote:

> > So, radical slogan: There are no individuals in mathematics
> >
>
> When you counter a mathematical claim with a counterexample,
> is such a counterexample definite?

Of course not. There is (probably) no such thing as a mathematical claim with a single counterexample.

Such would be a dead end. Counterexamples are useful because they illuminate previously unseen aspects and bring a new, living area of mathematics into existence.

> Have you described a
> plurality of counterexamples or a singularly specific
> counterexample?

One has uncovered a previously unseen pattern.

The diagonal of a unit square is "incommunsurable". Singular event. Big whoop. Just throw the clown overboard and no one will notice.

But that one "singular" discovery leads to a whole infinite pattern of incommunsurables.