On 6/9/17, 03:14, "Mario Castelán Castro" <marioxcc...@yandex.com> wrote:
Sorry; I should have been more clear.
Consider this hypothetical situation: I have a proposition “P:σ->bool”.
(P is a metavariable ranging over HOL terms with no free variables, σ is
a HOL type which may contain free type variables). In addition, I have
proved that the predicate-set P is non-empty (“∃ x. P x”).
The question is: Under the above conditions, is it always possible to
find a HOL type “τ” and a HOL term “f:σ” which is a bijection (i.e.
“!y:τ. ?!x::P. f x = y” is provable) between the predicate-set P and the
type τ?
According to my understanding, §2.4.5 “Extension by type definition” of
LOGIC describes a mechanism to introduce by definition one such type τ.
My question can be informally interpreted as the question of whether
such a type can always be constructed without the need for using the
definition mechanism.
This depends a little on what you mean by “find a type”. In the initial state
of HOL, there are two types (bool and ind), and one operator -> (function
space). The core axiomatization allows us to conclude that bool has two
elements, and that ind has at least aleph_0 many elements. Applying the
function operator generates a type that is strictly bigger than the
exponent/domain type. With these tools, it is clear that one cannot construct a
type with cardinality one.
Yet, the predicate ?y. !x. x = y captures the idea of a type having just one
element. So, if I’m interpreting your question correctly, the answer is no.
Michael
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
