[FOM] Potential infinite model of STT
matthias
matthias.eberl at mail.de
Wed Mar 6 01:12:57 EST 2019
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>
More information about the FOM
mailing list