Lambda the Ultimate

...although types do not necessarily give real SOL, since they are usually interpreted using Henkin (i.e., first-order) semantics.

FOL (Henkin) semantics works at least as well for Z_2 as the usual class of first-order models do in the case of PA (Z_1).

In fact, the distinctive point about first-order model theoory is that it doesn't bar monsters, allowing interesting theories such as PA+inconsistent(PA) that are relatively hard to give natural axiomatisations for in the language of Z_2.

Computer Science foundations need to bar the monsters of first-order logic, i.e. infinite integers and infinitesimal reals are highly undesirable in practical models of computation.

Ok, that's reached the line for me. Please. Stop. Trolling. Carl. The other threads should be more than enough to explore your alternative theory.

Maybe it's time for a certain greasemonkey script? ;-)

Funny you should mention that, just last week I was thinking of creating a chrome extension that would automatically add "?comments_per_page=400" to any LtU tracker link posted by Hewitt. Those threads tend to get long!

"?comments_per_page=600".

Ben,

It is an important technical point in computational models for the foundations of Computer Science that infinite integers and infinitesimal reals need to be barred.

Philosophers like Charles Stewart can argue that infinite integers and infinitesimal reals are interesting curiosities deserving attention.
Although computer systems need to deal with theories that allow such curiosities, that doesn't mean they should be part of the foundations.

Welcome to the conversation!
Do you have any substantive points to make about this controversy?

Regards,
Carl

You aren't making technical points when you employ language like "monsters" and "highly undesirable", you're employing pejorative language and you're not backing it up; you seem to be hoping for emotional reactions with this. Maybe let this thread stay focused on the linked content this time?

Ben,

Monster is a technical term after Lakatos.

Are you advocating that models of computation in foundations of CS incorporate infinite integers and infinitesimal reals?

Regards,
Carl

I have previously used (well, actually written) a system that represents numbers in a tree structure - roughly as you'd get them from parsing expressions. So if you asked it to compute triple the square root of two, the root of the tree would be a multiplication object, the upper branch would be the integer, and the lower branch a square root object which would itself have one child node denoting an integer.

It turns out that you can do quite general algebra with numbers represented this way, reducing terms and simplifying as the opportunities present themselves without loss of precision, and put off calculations that involve a possibility of rounding errors in hopes of algebraically eliminating them from results given later computation.

Not that that usually happens. Instead you get evaluation of the whole tree (monad) at the point where you have to plug the results into a limited-width representation or present an output in simple form.

Or you get evaluation of the whole tree from time to time when an emergency-level garbage collection is happening. Which is unpredictable to the programs, darnit, but at least the system does you the favor of marking the result as "non-exact" in that case. Which for other reasons (ie, irreducible without imprecise operations) it's likely to be anyway.

Such tricksy methods aside, though, that doesn't really get you the representation of the infinitesimal "real" numbers. It only gets you the representation of that ultimately tiny subset of the real numbers which can be expressed as a combination of operations on numbers that we can precisely (ie, in limited width) express.

And in number theory terms, it turns out that that set bears exactly the same relationship to the reals that rational numbers do. IE, if you have a "curve" where every such number has a y value of 1 and every other real number as a y value of 0, then like the analogous curve for rationals, it is discontinuous at every point - and like the rationals, the area under it is zero, because the infinities involved are of different orders.

Anyway, the bottom line is that one cannot represent arbitrarily-chosen members of any truly infinite set given a representation that can be stored in non-infinite memory.

But one can store a large and useful subset of those members, especially if one adapts the representation used to specifically match the results of the operations by which one arrives at the set of numbers one hopes to represent.

IOW, What I did there was not so much "representing any real number" as "picking a representation that maximizes coverage of the set of such numbers I can represent using the set of operations I use on numbers which can be expressed in source code that fits in finite space."

An I interesting thought is that if you instead calculated with rational ranges (that is nearest rational above and below the real) then the curve would be continuous and the area under it approximately correct.

Further if you assume that the irrational number must lie between the max representable rational below, and the next representable rational above, then you need only store a single rational to represent the range with the answer being in the range greater than or equal to that value itself and less than that value plus 1/max_int (and correcting for negative numbers).

Dear All,

I just would like to point out some monsters lurking in
higher order logic, that are most likely different from the
monsters that Hewitt is attacking, but that are even sometimes
useful monsters.

Monster 1:
==========
In Higher Order logic the end-user might change the meaning
of logical connectives. Usually, for example in FOL, one assumes
that by a theory we cannot change the meaning of the logical
connectives, when we define a theory we give meaning to the
predicates of this theory and the connectives are fixed.

This is not the case anymore for some Higher Order logics
for example. A discussion about this meaning shift in more
general is for example found in this book review:

Book Review, Shapiro, Varieties of Logic by
Geerdink and Dutilh Novaes, 2015
http://www.tandfonline.com/eprint/AiEZhKKXzBgRSexa9rQD/full#.VcdZbBIteO2

But we might also look on the bright side of this monster 1.
Without this monster 1 we would not have so called "logical
frameworks" that are for example underneath Isabelle/HOL, etc..
that allow to realize different logics inside the same framework.

And last but not least we are not helpless in respect of
monster 1, we could use Padoas method, for example via Craigs
interpolation, and even show for an appropriate layering in a
logic framework that the modelled logic has still fixed
logical connectives. Did somebody do this already?

Monster 2:
==========
This is an other monster I recently stepped into. It basically says
that substitution is not unbiquitious. Potentially showing some
limitations for logic frameworks based on dependent types or the
like, that impose a certain unbiquity of beta conversion.

An exposition that discusses some forms of this phaenomena is
for example the following book, which has a review here:

Book Review, Fitting, Types Tableaus and Gödels God
http://www.jstor.org/stable/20016758?seq=1#page_scan_tab_contents

I am not yet sure how this monster can be barred. But it seems
that developers of logic frameworks are aware of this monster,
at least it is sometimes heard that this and that logic framework
cannot be used for this and that modal logic.

But monster 2 might also lurk in more modest goals, such as
doing something with nominal terms and little cut-elimination
in a theorem prover. And when it can be overcome in such contexts
there can be a great benefit.

Bottom Line
===========
Most likely there is a second order logic around, that
avoids monster 1 and 2, and is quite practical. Maybe it is
even that powerful that we can redo a lot of interesting
practical mathematical stuff also formally. I am thinking of
the completion the following list:

Freek Wiedijk, Formalizing 100 Theorems
http://www.cs.ru.nl/~freek/100/

But who tells us that this second order logic is not
subject to monster 1 and monster 2? Shouldn't we better
try riding these monsters by ourselfs?

Bye

Types can help with the monsters:

* Categoricity Types can provide categoricity, i.e., a unique (up to isomorphism) model of axioms, e.g., for ℕ

* No "self-reference" Types mean that there are no "self-referential" sentences in Mathematics, e.g., "I am not provable." is not a sentence of Mathematics.

* Substitution always works for Actors of the same type.

All theorems on Wiedijk's list can easily be formalized using types except that the formalization of the incompleteness theorem for ℕ is incorrect; another monsters!.

Hi,

The list has not yet been completely proven
by a single system. The current completion state
is 91%.

The list has also not yet been completely
proven if we allow different systems for
different items in the list.

For example the following item has not been
entered yet, although a mathematical proof
now exists:

33. Fermat's Last Theorem
http://en.wikipedia.org/wiki/Fermat%27s_Last_Theorem#Wiles.27s_general_proof

Most items are 1-2 weeks work so I guess if one
starts from scratch with a new system, one needs
at least 2 years to get somewhere.

Maybe crowd sourcing would help, but proof systems
are not wide spread, the crowd would be still small.

Bye

P.S.: Hewitt do you mean 6. Gödel's Incompleteness Theorem,
where is the error?

The incompleteness theorem for ℕ:

There exists a proposition which is true in the model ℕ,
  but which is not provable using the Peano/Dedekind categorical axiomatization for ℕ.

The above theorem was first correctly proved by Church/Turing.

The article I originally linked to advocates an approach where we keep first-order theories for their tractability and we keep second-order theories for their use in fixing intended semantics: each approach comes with a set of tools that has their use.

First-order theories introduce highly undesirable infinite integers & infinitesimal reals into computational models.

Furthermore, typed theories can be more tractable than first-order logic.

From Kahneman (2011, p. 288):

Richer and more realistic assumptions do not suffice to make a theory successful. Scientists use theories as a bag of working tools, and they will not take on the burden of a heavier bag unless the new tools are very useful. Prospect theory was accepted by many scholars not because it is “true” but because the concepts that it added to utility theory, notably the reference point and loss aversion, were worth the trouble; they yielded new predictions that turned out to be true. We were lucky.

The bar is set very high for a new theory to displace FOL.



Reference

Kahneman, 2011. Thinking, Fast and Slow. Farrar, Straus and Giroux.