*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 -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/everything-list/2dce4cec-2b66-4bee-ac9b-a38cc96c3b44%40googlegroups.com.
