[FOM] Potential infinite model of STT

[matthias]

I have two questions concerning this issue.

1) is there a potential infinite model of simple type theory with total 
functions (to be used as a classical HOL)?

The following are not models, since their constructions make sense only 
if there is an actual infinite set:
- The total objects in a domain. This is due to the fact that a domain 
is based on the notion of 'directed completeness' (e.g. as the ideal 
completion of its compacts or as a bilimit). Finite directed sets always 
have a supremum.
- The hyperfinite type structure (by Norman, Palmgren and 
Stoltenberg-Hansen). Its construction is based on a factorization 
through a Frechet product, i.e., sequences that differ on finitely many 
arguments are identified.

A possible model is one in the style of a direct or inverse limit. But 
since logical relations (which are the means to extend properties to 
higher types) are not transitive one has to use a limit construction 
that is based on relations R instead of functions and the following 
property:
     aRb and aRc implies bRc
instead of transitivity.

2) Is this or a similar limit construction already known?

Kind regards,
Matthias
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20190306/bf0503e4/attachment.html>