After realising how specific exists_such_that's semantics are, a more fundamental approach to implement high order logic is to construct sets from conditional expressions.
_x_ where _x_ > 0 is any positive value
{ _x_ where _x_ > 0 } is the set of all positive values
| { _x_ where _x_ > 0 } | is the cardinality of the set of all positive values
(| { _x_ where _x_ > 0 } |) > 0 is true if there exists a positive value. (_x_ exists_such_that) _x_ > 0 should reduce to this.
How can we generalise this for any kind of condition?
let ((_x_ exists_such_that) _y_) -> (| { _x_ where _y_ } |) > 0
So exists_such_that need not be a concrete concept in the future as it could be implemented with Zia after implementing set comprehension and cardinality
After realising how specific
exists_such_that's semantics are, a more fundamental approach to implement high order logic is to construct sets from conditional expressions._x_ where _x_ > 0is any positive value{ _x_ where _x_ > 0 }is the set of all positive values| { _x_ where _x_ > 0 } |is the cardinality of the set of all positive values(| { _x_ where _x_ > 0 } |) > 0is true if there exists a positive value.(_x_ exists_such_that) _x_ > 0should reduce to this.How can we generalise this for any kind of condition?
let ((_x_ exists_such_that) _y_) -> (| { _x_ where _y_ } |) > 0So
exists_such_thatneed not be a concrete concept in the future as it could be implemented with Zia after implementing set comprehension and cardinality