Ken Dickey wrote:
On Tuesday 21 October 2008 08:32:12 Abdulaziz Ghuloum wrote:
On Oct 21, 2008, at 11:04 AM, Ken Dickey wrote:
No. Actually, I'd like a holds-for-all which returns #f as the
base case.
You can push it down, but you can't escape making these
exceptions.
The law of the excluded third has a number of possible outcomes:
#t #f not-applicable undecided unknown outcome
undecided is sometimes divided into undecidable, here are a list of conditions
which would make the preposition decidable, ..
That's a good reason to use exceptions in the math system
where different choices of axiom really matter.
That's not a good reason to hair up relations and sequences
since no changes to axioms, only definitions, are in play.
I am not saying that there is no check for existence of elements. I am saying
that there is no relation holding between elements when there are no
elements.
There is an element: the "possibly empty relation".
< is a binary relation of two numbers, let's say.
<... is a singleton relation (a property or predicate or subclass) of
sequences.
(<) ; ill formed expression
(< 1) ; ill formed expression
(< 1 2) => #t
(< 1 2 3) ; ill formed expression
(<...) => #t ; the empty sequence is well-ordered
(<... 1) => #t ; a singleton sequence is well-ordered
(<... 1 2) => #t ; that two element sequence is well-ordered
(<... 1 3 2) => #f ; that three element sequence is not well-ordered
etc.
-t
Cheers,
-KenD
"In theory, theory and practice are the same, but in practice they differ."
Engineer's axiom
_______________________________________________
r6rs-discuss mailing list
[email protected]
http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
_______________________________________________
r6rs-discuss mailing list
[email protected]
http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
