Re: Current Issues in the Philosophy of Practice of Mathematics & Informatics

Re: Current Issues in the Philosophy of Practice of Mathematics & Informatics

[Fred E.J. Linton]

A week or more ago Patrik Eklund <peklund@cs.umu.se> wrote of
  
> ... a "lativity" in logic ... .

Not wishing to broadcast my illiteracy in the matter, I searched high
and low for the meaning of the quoted term, to no avail: neither Google, 
nor Wikipedia, nor the other contemporary search mechanisms I tried,
offered any insight whatsoever into that term.

So I ask you now, in public, where my shame can be greatest: what 
do you mean by "lativity"? Anagram for "vitality"?

(Yes, I have seen -- but been mystified by -- Eklund's use of that term 
in an older Categories posting, of Feb 05 2014, 09:55, with Subject:

: categories: Re: Martin-Lof type theory gentle introduction please ... .)

Many thanks. Cheers, -- Fred	  	



[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Current Issues in the Philosophy of Practice of Mathematics & Informatics

[Patrik Eklund]

On 2015-08-09 05:10, Fred E.J. Linton wrote:
> Not wishing to broadcast my illiteracy in the matter ...
> So I ask you now, in public, where my shame can be greatest: what do
> you mean by "lativity"?

Thank you, Fred, for your questions. We were actually nervously waiting
for somebody to ask that question, so we will remember you always for
having done that.

In logic we typically have signatures, terms, sentences, structured sets
of sentences, entailment, models, satisfactions, axioms, theories and
proof calculi. We cannot e.g. define entailment before we have a notion
of sentences, and we should not define sentences before we have a notion
of terms. The latter is a bit more controversial. In first-order logic I
would see P(x), where P is a "predicate symbol", as a term, and not as a
sentence, whereas putting a quantifier in front of it, Ex.P(x), makes it
no longer a term. This is why I have difficulties e.g. to accept that
the two 'not's in expressions like "not Ex.P(x)" and "Ex.not P(x)" would
be the same. I am starting to think they are only informal as symbols, a
bit similar as Church said lambda is and informal symbol, so actually
not part of the formal syntax. Am I wrong or am I wrong?

In logic we indeed need a signature (sorts and operators) in order to
construct the categorical object of terms. Construction is important. We
need terms to categorically construct sentences, which appear because of
a sentence functor not being extendable to a monad. Otherwise sentences
are terms, aren't they, because then we could substitute sentences
within sentences, and that does not comply with our traditional view of
sentences.

Traditional first-order pretty much doesn't care, and neither did
Aristotle about these things. Aristotle's and first-order logic are
therefore very "illative" and also very unsorted, I would like to add.

You are not broadcasting illiteracy at all, and your shame couldn't even
be small because no shame whatsoever is justified to exist, at least not
on your side. There may, however, be some of it now or eventually on my
side, but let us see what happens if/when/how this dialogue develops. It
may indeed turn out that at least some members of this catlist will see
me just as a devoted soldier "seeking the bubble reputation, even in the
canon's mouth".

When we were searching for a name describing what we try to explain, we
wanted to be careful not to use a "reserved word" that is more easily
misunderstood than not well understood. In the latter case, we thought
we can always try to explain, as I am about to do now. In the former
case it would be a differentiation, which is more tricky.

So here goes.

'Lative' is related to motion, and more specifically, motion 'to' and
'from', so when terms appear in sentences, terms 'move into' sentence,
and 'appear within' sentences. At the same time, sentences 'move away
from' terms, and separates terms from sentences. In comparison,
'ablative' is motion 'away', and nominative is static. The lative
locative case (casus) indeed represents "motion", whereas e.g. a
vocative case is identification with address.

We want to underline the need not to have "mixed bags", so that we can
ensure that a term does not appear in the bag of sentences, or a
structured set of sentences would appear in the bad of entailment. I
shouldn't compare with waste sorting, because then somebody might say
"Patrik Eklund said Kurt G??del didn't care about waste sorting".
Obviously, I do respect the work of G??del, even if at the same time I do
find his approach "illative". From categorical point of view, G??del also
complies only with the underlying category of sets, but as we have shown
(e.g. in
http://www.sciencedirect.com/science/article/pii/S0165011413000997), we
may have other underlying categories for the the term monad. The term
constructor and the use of category theory as the metalanguage for logic
is here important. Logic developed "hand-in-hand" with set theory and as
being a metalanguage for category theory should then not be confused
with the lativity of logic we explain using categorical notions.

Let me also again underline that nomenclatures and classifications in
health care is one of our motivation areas of examples and applications.
Nomenclatures exist also elsewhere, but he ones appearing in health we
find very motivating.

At this point of our "research program" we believe we have a fair
understanding of the lativity as related to signatures, terms and
sentences, and we hope we have a fair intuition about how we now proceed
to investigate the lativity of that with respect e.g. to to entailment
and models.

Thanks again, and indeed, possible shame in whatever form or magnitude
is all mine.

Best,

Patrik



[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Current Issues in the Philosophy of Practice of Mathematics & Informatics

[Thomas Streicher]

> In logic we typically have signatures, terms, sentences, structured sets
> of sentences, entailment, models, satisfactions, axioms, theories and
> proof calculi. We cannot e.g. define entailment before we have a notion
> of sentences, and we should not define sentences before we have a notion
> of terms. The latter is a bit more controversial. In first-order logic I
> would see P(x), where P is a "predicate symbol", as a term, and not as a
> sentence, whereas putting a quantifier in front of it, Ex.P(x), makes it
> no longer a term. This is why I have difficulties e.g. to accept that
> the two 'not's in expressions like "not Ex.P(x)" and "Ex.not P(x)" would
> be the same. I am starting to think they are only informal as symbols, a
> bit similar as Church said lambda is and informal symbol, so actually
> not part of the formal syntax. Am I wrong or am I wrong?

I don't understand why atomic formulas are terms but not formulas.
Always thought the Lawvere's hyperdoctrines made all this very clear:
terms are in the base and formulas are in the fibres.
In case there is a generic family of propositions  A:Prop |- True(A)
we can turn predicates into terms of type Prop. That's the shift to HOL.

The 2 different negations are just negations in two different fibres.

Thomas


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Current Issues in the Philosophy of Practice of Mathematics & Informatics

[Steve Vickers]

Dear Patrik,

I think I understand what you mean by lativity - in the logical account
you proceed from one kind of structure to another, defining the latter
in terms of the former.

By the way, your discussion of terms and sentences seems to be missing
the notion of formula as distinct from terms. (I think at one point you
mentioned the Goguen-Burstall institutions, which have a similar
omission.) Usually one thinks of terms as referring to the things you
are talking about, and formulae as what you are saying about them: so
the predicate P(x) is a formula with x a term. Quantification still
yields formulae, but a formula with no free variables is also a
sentence. (What would you call Ex.P(x,y) in your language?) As I
understand it, this is lative in that you proceed from terms to formulae
to sentences.

To check my understanding, here's another system that I believe you
would call lative: sequent calculus where a sequent is entailment of
formulae in a context (of free variables available). You proceed from
formulae to sequents, and the sequent is the analogue of the sentence in
this logic. Then there is a sharp, lative distinction between the
quantified formula Ax.P(x), with no free variables, and the sequent
   T |-_{x} P(x)
with context {x}.

Here's an example I guess you would call illative: dependent type
theory. The types are in many ways analogous to formulae, but types
depend on terms and terms depend on types. (Also you have judgements
similar to sequents.) Most of us are happy with that; it just means that
terms and types are defined together, inductively in a well-founded way.

Is dependent type theory illative? If so, what difference does that make
to you?

Here's another contrast. Algebraic theories are lative, in that you
proceed from terms to equations (the formulae). Essentially algebraic
theories are illative in that the existence of terms may depend on
equations holding. For example the composite of two morphisms in a
category exists only if the codomain of one equals the domain of the
other. When you are constructing free algebras, the lativity of the
algebraic case means you can do it in three steps: first construct the
terms, then generate a congruence, then factor out the congruence. The
illativity for the essentially algebraic case seems to spoil this, in
that factoring out the congruence may create more equalities and hence
bring more terms into existence. (Though actually you can do it in the
same three steps if you first create all "potential" terms, then
generate a partial congruence, where self-congruence is existence, then
factor that out.)

Regards,

Steve.

On 09/08/2015 10:52, Patrik Eklund wrote:
> On 2015-08-09 05:10, Fred E.J. Linton wrote:
>> Not wishing to broadcast my illiteracy in the matter ...
>> So I ask you now, in public, where my shame can be greatest: what do
>> you mean by "lativity"?
>
> Thank you, Fred, for your questions. We were actually nervously waiting
> for somebody to ask that question, so we will remember you always for
> having done that.
>
...

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Current Issues in the Philosophy of Practice of Mathematics & Informatics

[Robert Dawson]

Patrik Eklund wrote:'

... at least some members of this catlist will see me just as a devoted
soldier "seeking the bubble reputation, even in the _canon's_ mouth".

I'm trying to figure out if this is a misspelling or a pun so clever
that I can't quite figure it out.

Robert Dawson


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Current Issues in the Philosophy of Practice of Mathematics & Informatics

[Ralph Matthes]

[why on the categories mailing list? some of the courses are strongly
based on category theory, and it seems that quite some subscribers to
this list are interested in connections between mathematics and philosophy]


Dear colleagues,

The thematic trimester CIPPMI "Current Issues in the Philosophy of
Practice of Mathematics & Informatics" will be held from 4th April to
1st July 2016 at the Centre International de Math??matiques et
d'Informatique de Toulouse (CIMI).

This thematic trimester is organised by an interdisciplinary team of
researchers in Mathematics, Philosophy, and Computer Science from the
Institut de Math??matiques de Toulouse (IMT) & the Institut de
Recherche en Informatique de Toulouse (IRIT).

It will feature course sessions, workshops, and a thematic school on
themes at the interface of Philosophy, Mathematics and Computer Science.

You will find all relevant information on the website of the thematic
trimester that will be regularly updated:
http://www.cimi.univ-toulouse.fr/cippmi/en

A mailing list allows you to receive the different announcements from
CIPPMI: https://sympa.math.ups-tlse.fr/wws/info/cippmi

You can register at
http://www.cimi.univ-toulouse.fr/cippmi/fr/inscriptionregistration

A funding for accommodation is available in priority for junior
researchers and for some senior researchers without funding from their
laboratory. For further information, please consult the page:
http://www.cimi.univ-toulouse.fr/cippmi/fr/boursesgrants

With apologies for cross-posting, best regards, the CIPPMI scientific
organisation committee.

---

Ralph Matthes

IRIT (CNRS & Univ. Toulouse)
http://www.irit.fr/~Ralph.Matthes/


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Current Issues in the Philosophy of Practice of Mathematics & Informatics

[Graham White]

And (continuing "why on the categories mailing list?") it seems
to some people (such as me) that what category theory actually is, is
a formal description of the practice of mathematics, rather than a
foundation for mathematics. It may do the latter as well (though I don't
really believe so), but an account of the practice of mathematics
would be far more philosophically interesting than a foundation. It
would, for example, allow a dialogue between the philosophy of
mathematics and the rest of philosophy, which has, for 30 or 40 years
now, been much less foundational than it used to be. And it may even
make category theory an important tool in philosophy generally.

Graham

On 24/07/15 05:12, Ralph Matthes wrote:
> [why on the categories mailing list? some of the courses are strongly
> based on category theory, and it seems that quite some subscribers to
> this list are interested in connections between mathematics and philosophy]
>
>
> Dear colleagues,
>
> The thematic trimester CIPPMI "Current Issues in the Philosophy of
> Practice of Mathematics & Informatics" will be held from 4th April to
> 1st July 2016 at the Centre International de Math??matiques et
> d'Informatique de Toulouse (CIMI).
>
> This thematic trimester is organised by an interdisciplinary team of
> researchers in Mathematics, Philosophy, and Computer Science from the
> Institut de Math??matiques de Toulouse (IMT) & the Institut de
> Recherche en Informatique de Toulouse (IRIT).
>
> It will feature course sessions, workshops, and a thematic school on
> themes at the interface of Philosophy, Mathematics and Computer Science.
>
> You will find all relevant information on the website of the thematic
> trimester that will be regularly updated:
> http://www.cimi.univ-toulouse.fr/cippmi/en
>
> A mailing list allows you to receive the different announcements from
> CIPPMI: https://sympa.math.ups-tlse.fr/wws/info/cippmi
>
> You can register at
> http://www.cimi.univ-toulouse.fr/cippmi/fr/inscriptionregistration
>
> A funding for accommodation is available in priority for junior
> researchers and for some senior researchers without funding from their
> laboratory. For further information, please consult the page:
> http://www.cimi.univ-toulouse.fr/cippmi/fr/boursesgrants
>
> With apologies for cross-posting, best regards, the CIPPMI scientific
> organisation committee.
>
> ---
>
> Ralph Matthes
>
> IRIT (CNRS & Univ. Toulouse)
> http://www.irit.fr/~Ralph.Matthes/
>

-- 
Graham White
Electronic Engineering and Computer Science
Queen Mary, University of London
http://www.eecs.qmul.ac.uk/~graham/


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Current Issues in the Philosophy of Practice of Mathematics & Informatics

[Patrik Eklund]

Philosophy of mathematics is still philosophy and has nothing to do with
mathematics, since philosophy does not adhere to any mathematical
principles.

Philosophy of logic is the same, since philosophy does not adhere to any
logical principles.

However, the logic of mathematics and the mathematics of logic is more
interesting in particular as a major part of informatics can learn from
logic.

It is somehow interesting that the philosophy of set theory is never on
any agenda, even if set theory, logic and mathematics is very much
intertwined. Early 20th century work and development in G??ttingen,
Vienna and Warsaw, and other places, of course, is often said to be very
well known, but surprisingly few actually still read work from that era.

Why, for instance, is it so clear that G??del's Incompleteness Theorem is
a "theorem" and not a "paradox"? After all, it is nothing but a bit more
subtle version of the Liar paradox. I paradox means Fix it!, whereas a
theorem means Don't touch!.

In logic, why do we make a giant leap from Aristotle (who was a
philosopher, not a logician) to Boole/Peano/Frege, ignoring whatever
happened logically in between? In math we don't do that.

Category theory can play a role in all this, in particular in more
strict definitions of the notion of logic. Type theory is good example,
where type constructors are still allowed to dangle around any formalism
adopted, and then something magic comes in from the outside and provides
a "solution". HoTT and its predecessors are doing that all the time.

The phrase "Philosophy of Practice of Mathematics & Informatics", I
guess, is as good as any variation  of it. WE could also debate about
the "Mathematical Practice of the Informatics of Philosophy", or the
"Informatics if Mathematics of Philosophy & Practice", or even the
"Mathematical Practice of Informatics without any interference
whatsoever of Philosophy".

Best,

Patrik

www.glioc.com



On 2015-07-25 16:57, Graham White wrote:
> And (continuing "why on the categories mailing list?") it seems
> to some people (such as me) that what category theory actually is, is
> a formal description of the practice of mathematics, rather than a
> foundation for mathematics. It may do the latter as well (though I
> don't
> really believe so), but an account of the practice of mathematics
> would be far more philosophically interesting than a foundation. It
> would, for example, allow a dialogue between the philosophy of
> mathematics and the rest of philosophy, which has, for 30 or 40 years
> now, been much less foundational than it used to be. And it may even
> make category theory an important tool in philosophy generally.
>
> Graham
>
> On 24/07/15 05:12, Ralph Matthes wrote:
>> [why on the categories mailing list? some of the courses are strongly
>> based on category theory, and it seems that quite some subscribers to
>> this list are interested in connections between mathematics and
>> philosophy]
>>
>>
>> Dear colleagues,
>>
>> The thematic trimester CIPPMI "Current Issues in the Philosophy of
>> Practice of Mathematics & Informatics" will be held from 4th April to
>> 1st July 2016 at the Centre International de Math??matiques et
>> d'Informatique de Toulouse (CIMI).
>>
>> This thematic trimester is organised by an interdisciplinary team of
>> researchers in Mathematics, Philosophy, and Computer Science from the
>> Institut de Math??matiques de Toulouse (IMT) & the Institut de
>> Recherche en Informatique de Toulouse (IRIT).
>>
>> It will feature course sessions, workshops, and a thematic school on
>> themes at the interface of Philosophy, Mathematics and Computer
>> Science.
>>
>> You will find all relevant information on the website of the thematic
>> trimester that will be regularly updated:
>> http://www.cimi.univ-toulouse.fr/cippmi/en
>>
>> A mailing list allows you to receive the different announcements from
>> CIPPMI: https://sympa.math.ups-tlse.fr/wws/info/cippmi
>>
>> You can register at
>> http://www.cimi.univ-toulouse.fr/cippmi/fr/inscriptionregistration
>>
>> A funding for accommodation is available in priority for junior
>> researchers and for some senior researchers without funding from their
>> laboratory. For further information, please consult the page:
>> http://www.cimi.univ-toulouse.fr/cippmi/fr/boursesgrants
>>
>> With apologies for cross-posting, best regards, the CIPPMI scientific
>> organisation committee.
>>
>> ---
>>
>> Ralph Matthes
>>
>> IRIT (CNRS & Univ. Toulouse)
>> http://www.irit.fr/~Ralph.Matthes/
>>

-- 
Prof. Patrik Eklund
Ume?? University
Department of Computing Science
SE-90187 Ume??
Sweden

-------------------------

mobile +46 70 586 4414
website www8.cs.umu.se/~peklund


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Current Issues in the Philosophy of Practice of Mathematics & Informatics

[Martin Escardo]

I am not sure why these questions are being asked in this list:

On 26/07/15 16:33, Patrik Eklund wrote:
> Why, for instance, is it so clear that G??del's Incompleteness Theorem is
> a "theorem" and not a "paradox"?

I am not sure what you mean by a paradox. But let me take this as a
possible interpretation: A paradox is a statement P such that both P
and not P are theorems (or, equivalently, such that P holds iff not P
holds).

As far as current mathematical knowledge goes, Goedel's Incompleteness
Theorem is just a theorem, with significant further work needed to
elevate it to the status of a paradox.

> After all, it is nothing but a bit more subtle version of the Liar
> paradox. I paradox means Fix it!, whereas a theorem means Don't
> touch!.

For comparison, in naive set theory, the set of all sets that don't
belong to themselves does lead to a paradox, corresponding to the Liar
Paradox: this set belongs to itself if and only it doesn't. Naive set
theory is inconsistent (and hence deserves its name).

In ZFC, however, the same argument *proves* that there is no set of
all sets, and no set of sets that don't belong to themselves.

It is important here that ZFC can actually formulate the question of
whether there is a set of all sets. And the answer is no.

Of course, in principle, the possibility is open that ZFC, too, has a
some paradox. This involves exhibiting a statement P and two proofs,
following strict rules of mathematical rigour, one of the statement P
and another of the statement not P. Nobody has so far managed to
exhibit such three things.

This is so hard that probably deserves a Fields Medal (followed by
immediate eviction from the mathematical community).

M.



[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Current Issues in the Philosophy of Practice of Mathematics & Informatics

[Patrik Eklund]

Hi Martin,

Thanks for your response. My catlist posting was using rather general
formulations but there are underlying detail that can be found in our
papers.

Let me add just a few historical remarks.

One main idea of our work is that their is a "lativity" in logic that is
not respected. It's not comparable to the "lativity" in set theory where
you can create classes out of sets, but you cannot throw classes back
into the basket of sets, whatever that would be. The same thing happens
in logic. We must start with the signature, based on which we construct
terms, and terms are used inside sentences. Once we have the "bag of
sentences" we may proceed "latively" to construct other things. When we
eventually come to proof rules, the bag of sentences was closed a long
time ago. Yet, G??del uses "provability" to create new sentences, and
simply opens up that bag of sentences, and throws in these new ones. It
has always been accepted, but this in fact breaches the lativity
principle, which indeed is not respected in logic.

The lativity principle cannot be formulated in set theory alone, and set
theory is also very much untyped, we have to say. It basically also
boils down to separating object languages from their metalanguages.
First-order logic as developed from a fons-et-origo becomes acceptable
over decades while being developed hand-in-hand, so as to say, with set
theory.

Type constructors in type theory are good examples that basically appear
in no language whatsoever. They are simply brought in from the outside,
almost like a holy spirit.

But then we have category theory, and in our approach we use it as an
object language where that hand-in-hand appears as a metalanguage. And
then I turn category theory into a new metalanguage in order to deal
with lativity of logic.

There is a bit of lativity in Goguen-Burstall's and Meseguer's general
models, but unfortunately types do not explicitly occur since the Sign
category is considered as abstract until it is made precise for
particular logics. And when it's made "precise" e.g. for first-order, it
simply adopts e.g. the traditional explanation of terms, so they are not
formally constructed within that categorical metalanguage. This is of
course then the also reason why the Cat theory enters when dealing with
semantics. It's also too general.

Yes, we cannot create the set of all sets, similarly as we shouldn't
even try out creating the type of all types. Nevertheless, Martin-L??f
took the liberty of doing that, and was opportunistic enough to publish
it. Things went wrong but it was not called a paradox. Constructions
were "improved" over decades, but the HoTT community still uses
universality, so that paradox just appears as the emperors new clothes.

Sch??nfinkel, Curry and Church saw all these problems, and Hilbert saw
it, too, of course, since all of these three were discussing these quite
frequently over many years in G??ttingen. Hilbert never wrote anything
about it, but probably because he couldn't solve it (or wasn't
interested in medals), and he was becoming too old at that time anyway.
Sch??nfinkel and Church write more explicitly that something remains to
be understood, but Curry less so. Curry just went on even if the
foundations were shaky. Kleene never did that, and he was in any case
cleaning up other things. von Neumann probably saw what was going on,
but he kept himself always out of that mess. So when that mess now has
rooted itself like the Mentha Piperita, opportunists travel around, and
the bank voles follow them.

> I am not sure why these questions are being asked in this list:

In our work now it's indeed about understanding that lativity, and these
questions turn up when we use categories as a metalanguage for logic. We
thereby also say that types are not fundamental, but rather given
because of an object in a category.

We also see how we need to debate category theory itself. Take monoidal
categories. They are not really categories, are they? They do contain a
category, but they are not categories. They are not algebraic structures
either, are they? Freeness issues become tricky, and it becomes doubtful
if universal algebra can overcoat lativity of logic. Universal algebra
kind of strangles logic to become what it is generally accepted to be.

Cheers,

Patrik



-- 
Prof. Patrik Eklund
Ume?? University
Department of Computing Science
SE-90187 Ume??
Sweden

-------------------------

mobile +46 70 586 4414
website www8.cs.umu.se/~peklund


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Current Issues in the Philosophy of Practice of Mathematics & Informatics

[Martin Escardo]

Some claims quoted below need to be rectified, given that this is a
public forum:

On 29/07/15 06:54, Patrik Eklund wrote:
>> Yes, we cannot create the set of all sets, similarly as we shouldn't
> even try out creating the type of all types. Nevertheless, Martin-L??f
> took the liberty of doing that, and was opportunistic enough to publish
> it. Things went wrong but it was not called a paradox.

It is called Girard's Paradox, and the construction resembles
Burali-Forti's Paradox, rather than Russell's paradox.

The idea was to have a type U of all types, including U itself,
written U:U. This may seem naive given Russell's Paradox was known.

However, there is more to U:U than Russell's paradox, because "U:U" is
not a proposition (it is a so-called judgment), and hence it cannot be
true or false, or taken as a hypothesis in a mathematical
statement. In particular, using U:U, you cannot form the type of all
types that don't belong to themselves, because there is no "belong"
relation in type theory, and for instance writing something such as
"not(X:X)" is not even grammatically correct.

To derive a contradiction using U:U (in a type theory extended with
this judgement) is much harder than to derive a contradiction from the
hypothetical existence of a set of all sets (in set theory).

> Constructions were "improved" over decades, but the HoTT community
> still uses universality, so that paradox just appears as the
> emperors new clothes.

The improvement adopted both in MLTT in the 1980's, and in MLTT+HoTT
axioms now, was already available, and is the same as the one Russell
proposed a century ago to avoid his paradox, and adopted in Principia
Mathematica, namely to instead have a hierarchical stratification
U_0 : U_1 : U_2 : U_3 : ... by "size", where U_0 is the type of all
small types, which lives in the type U_1 of large types, which lives
in the type U_2 of even larger types, etc.

The idea is at least 107 years old.

M.





[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Current Issues in the Philosophy of Practice of Mathematics & Informatics

[Thomas Streicher]

> Yet, G??del uses "provability" to create new sentences, and
> simply opens up that bag of sentences, and throws in these new ones. It
> has always been accepted, but this in fact breaches the lativity
> principle, which indeed is not respected in logic.

The point is that the provability predicate doesn't require new syntax
but can be formulated already with a modicum of arithmetic (that's what
has become known as "Goedelization").

It would be a different issue with a "truth" predicate which cannot be
expressed in the language (known as Tarski's theorem).

Thomas


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Current Issues in the Philosophy of Practice of Mathematics & Informatics

[Robert Dawson]

On 7/26/2015 12:33 PM, Patrik Eklund wrote:
> Philosophy of mathematics is still philosophy and has nothing to do with
> mathematics, since philosophy does not adhere to any mathematical
> principles.
>
> Philosophy of logic is the same, since philosophy does not adhere to any
> logical principles.
>

By an argument such as this, it would appear that you could say that
bacteriology has nothing to do with bacteria, because you cannot grow
bacteriology on a Petri dish or sequence its DNA -and obviously this
would be absurd.

I think the source of the confusion here is that mathematics is
reflexive in a way that bacteriology isn't:  mathematics/logic _does_
feed back into itself and become a tool for doing more
mathematics/logic.  It's thus tempting to think that anything outside
this loop is not part of mathematics/logic.

However, the loop is not closed, and cannot be.  There are questions
which are legitimate parts of mathematics/logic that cannot be answered
internally.  I'm not talking about Goedel incompleteness here (though
one might), but about why we do what we do.  If we want to say what
constitutes mathematics worth doing - to say why Fermat's Last Theorem
or the Riemann Hypothesis are more important that the (3n+1) problem or
finding palindromic sequences in the decimal expansion of pi - we cannot
do this by calculation and proof.  This is an example of a place where
philosophy of mathematics can have a genuine connection.

-Robert Dawson




[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Current Issues in the Philosophy of Practice of Mathematics & Informatics

[Vaughan Pratt]

While agreeing wholeheartedly with Robert, I would like to point a
finger at what I think of as the "monolithic mathematics mob", MMM.
These are the people who treat mathematics as a single theory.  Carl
Hewitt, with whom I shared an admin at MIT for a decade, has a proof of
the consistency of mathematics based on that premise at

https://docs.google.com/file/d/0B79uetkQ_hCKbkFpbFJQVFhvdU0/edit?usp=sharing

along with a little more that so far I've been unable to pin down.  But
I rather suspect that pretty much everyone who finds G??del's second
incompleteness theorem paradoxical shares Hewitt's view of mathematics
as a single theory.

I find the following difficulties with the MMM view.

1.  You can't have a theory without a language.  What is the language of
mathematics?  Judging by appearances it would seem to be a living thing
that grows in different directions following the many varied and
evolving interests of mathematicians, pure, applied, Arcturan, or whatever.

This leads to:

Principle 1.  There will never come a time when mathematicians have
settled on the language of mathematics.

2.  In the unlikely event that Principle 1 is violated, namely by
collecting every mathematical symbol that will ever be needed in
mathematics into a single language possessed of a single consistent
theory T, there is no reason to expect any such thing to be recursively
enumerable.  With the requisite assumptions this is G??del's first rather
than his second incompleteness theorem.

But this raises the imponderable question of whether mathematics is what
mathematicians know, or what they could ever know (by enumeration of
theorems), or the aforementioned theory T, which they can never know at
any future time t even as all the consequences-in-principle of whatever
finite axiomatization of T they have agreed on by time t.

Which leads to:

Principle 2.  There will never come a time when mathematicians have
settled on what constitutes mathematics.

G??del's first incompleteness theorem suffices for Principle 2.
Principle 1 is even more elementary.  Much as I appreciate G??del's
second incompleteness theorem, it seems to me that his first is all
that's needed to answer those who find the second paradoxical.

Vaughan Pratt

On 7/29/2015 6:56 AM, Robert Dawson wrote:
...
> However, the loop is not closed, and cannot be.  There are questions
> which are legitimate parts of mathematics/logic that cannot be answered
> internally.  I'm not talking about Goedel incompleteness here (though
> one might), but about why we do what we do.  If we want to say what
> constitutes mathematics worth doing - to say why Fermat's Last Theorem
> or the Riemann Hypothesis are more important that the (3n+1) problem or
> finding palindromic sequences in the decimal expansion of pi - we cannot
> do this by calculation and proof.  This is an example of a place where
> philosophy of mathematics can have a genuine connection.
>
> -Robert Dawson


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Current Issues in the Philosophy of Practice of Mathematics & Informatics

[Patrik Eklund]

On Hewitt's Inconsistency Robustness, and given that my original posting
was related to category theory as a metalanguage for logic in the sense
of explaining extensions of the Goguen-Burstall and Meseguer approaches,
phrases like "mathematics is inconsistent" and "proof does not
intuitively increase our confidence in the consistency of mathematics"
(appear in Hewitt's paper) really make no sense at all.

Martin Escardo in his first reply to my posting says "I am not sure why
these questions are being asked in this list". My simple reply is
because my posting was suggesting to debate the use of category theory
as a the underlying language for logic. Basically none of the replies to
my posting has so far anything to do with category theory.

Hewitt says "A mathematical theory is an extension of mathematics whose
proofs are computationally enumerable." which basically means he says
logic is an extension of mathematics. Logic is part of mathematics as a
discipline, so logic cannot be the external canon for mathematics as
little as philosophy can be the external canon for science. Nothing is
global or canonic as far as mathematics is concerned. Many have tried to
do so, but their is no consensus in that direction. Hewitt's note
confirms that quite clearly.

"Philosophy and mathematics can have a genuine connection", but that
doesn't lead to anything useful. It just adds to fragmentation of the
understanding of foundations. With category theory underlying type
theory we believe we can manage type constructors more formally without
restarting foundations a la HoTT.

In Hewitt's note I am surprised not to see anything written about the
'iota' and 'o' types when speaking about Church. These are key types in
the categorical description of the "lativity" of logic I mentioned
earlier, and universal algebra comes short to deal with them. That
lativity is important also otherwise. Proof mechanisms come after (not
before or during) the bags of terms and sentences have been closed and
sealed. So statements and enumerations involving proofs are not
sentences in that sealed bag. This is the principle of lativity not
respected by traditional logic where the metalanguage is absent. With
categories in the meta for logic, we have term monads because we need
substitutions to compose, but we only have sentence functors. A
sentences functor being a monad simply means those sentences are terms.
We have also said that an unquantified proposition P is not a sentence.
It's a term. Quantifying it makes it a sentence, but then we have
problems with the negation. The "not" before a P (as a term) is really
different from a "not" before a quantifier, isn't it? Traditionally not,
but when we start to construct terms and sentences otherwise than using
natural language, we see it more clearly.

All this is overlooked in traditional logic, and having category theory
as a metalanguage for constructing terms and sentences, respectively as
monads and functors, gives us something new to think about. This is our
credo.

Languages are more or less formal. Languages are more or less
mathematically defined. Whatever the situation, if an object language
allows less formal outsiders to be invoked side by side with its
underlying metalanguage, ugly gets even worse.

Best,

Patrik



[For admin and other information see: http://www.mta.ca/~cat-dist/ ]