Finitistic Higher Order Logic

[Philip Thrift]

Finitistic Higher Order Logic

Matthias Eberl

[slides] http://www.math.lmu.de/~petrakis/Eberl.pdf

A finititstic understanding of mathematics

Forerunner: Jan Mycielski (Locally finite theories, JSL ’86)

https://www.jstor.org/stable/2273942

Main idea:

Infinite sets are not actual infinite, but indefinitely extensible —

This applies also to the syntax. No notion of computability.

from http://www.math.lmu.de/~petrakis/ABM17.php :

We follow a finitistic approach initially presented by Jan Mycielski for first order logic (locally finite theories, JSL '86). Different to Mycielski's approach we use a model theory based on the idea that all infinite sets are replaced by indefinitely extensible sets --- formally these are families of sets. The interpretation then uses a kind of reflection principle whereby the universal quantifier ranges over sufficiently large finite sets, not over infinite sets. This works fine for first order logic in which the objects are finite and only infinite sets of objects are approximated by finite sets. In order to extend this idea to higher order logic in form of simple type theory (STT) we additionally have to consider infinite objects (functions), which are approximated themselves. In order to formulate a finitistic version thereof we approximate function spaces of higher types by finite sets of finite approximations of these functions. These finite function spaces are related by partial surjections (on higher types defined as logical relations) and we introduce a new notion of a limit for them. The limit structure is then equipped with a family of partial equivalence relations (PERs), approximating equality. There is a one-to-one correspondence between the families of finite sets of finite approximations and the infinite limit structures. Different to domain theory we use total functions in order to have the usual classical truth values and use STT as a higher order logic.

@philipthrift

[Bruno Marchal]

With Mechanism, this type of approach, as well as Scott one, works well for the first person logic, but cannot work for the big 3p description, where partial functions are mandatory. If we limit ourself on total functions, we get security, and nice foundations, but we loss universality, (or creativity (in Emil Post sense)), and, I would say we loss liberty. In fact, universality is liberty, at least in a first approximation. 

If the Soviet did make the discovery of Gödel and Turing, they would have sent the universal machine (aka computer) to the Goulag immediately.

Bruno

@philipthrift

--
You received this message because you are subscribed to the Google Groups "Everything List" group.
To unsubscribe from this group and stop receiving emails from it, send an email to everything-li...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/everything-list/2dce4cec-2b66-4bee-ac9b-a38cc96c3b44%40googlegroups.com.