Enumerations from Z+ or N? #107

Closed
opened this Issue Oct 14, 2016 · 11 comments

Projects
None yet
2 participants
Member

rzach commented Oct 14, 2016

 The section on enumerations https://github.com/OpenLogicProject/OpenLogic/blob/master/content/sets-functions-relations/size-of-sets/enumerability.tex is inconsistent between enumerations being functions from N or from Z+; it should be unified. It is also inconsistent between an enumeration being partial or total. This section should prove the equivalence of the informal and the formal definition (it does so now just for the formal definition using a partial function). The zig-zag method of enumeration probably needs its own section.
Member

rzach commented Oct 25, 2016

 @nicolewyatt agrees, we should switch this to Z^+.
Member

rzach commented Oct 26, 2016

 There is a more significant problem in that the formal definition of enumeration now uses a surjective function, but no such function exists if X is empty. The explanation assumes that f may be partial, but that conflicts with the official definition of function.
Contributor

nicolewyatt commented Oct 26, 2016

 I'm don't think I'm following this. If X is empty, then any function from Z+ to X is trivially onto X, no?
Contributor

nicolewyatt commented Oct 26, 2016 • edited Edited 1 time nicolewyatt edited Oct 26, 2016 (most recent)

 Oh, I see, the problem is with making enumerations always total functions. But surely that is just a good reason to stick with allowing partial functions to count. Is the issue with the current definition that mathematicians take function to default to total function?
Member

rzach commented Oct 26, 2016 • edited Edited 1 time rzach edited Oct 26, 2016 (most recent)

 Yes, but we previously decided to make functions total (and call mappings that are partial but functional "partial functions")! In any case there is now a mismatch between the functions chapter (everything is total) and the size of sets chapter (functions may be partial).
Contributor

nicolewyatt commented Oct 26, 2016

 Did we? I have trouble keeping track to be honest. Option 1: revise the definition to say any partial onto function or total onto function counts. (If function means total function, is the total there redundant?) Add argument to the effect that where X is non-empty there is always an onto function. Option 2: Give a two part definition of enumerability -- X is enumerable if either it is empty or ...
Contributor

nicolewyatt commented Oct 26, 2016

 Option 2 is easier but perhaps less elegant.

rzach added a commit that referenced this issue Nov 13, 2016

``` fixing issue #107, replacing \Nat with \Int^+ when discussing enumara… ```
`…tions and formulating everything with total functions`
``` 370cb02 ```
Member

rzach commented Nov 13, 2016

 Ok I've fixed this in commit 370cb02 -- where I've also tried to completely avoid formulating the diagonal arguments as indirect proofs (ie made them intuitionistically ok).
Contributor

nicolewyatt commented Nov 13, 2016

 Line 36/49 still has natural numbers rather than positive integers. At line 82 how about "The last argument shows .." rather than "The last proof shows..", since part of the motivation is that the argument in question does not meet the standards of mathematical proof, no? I have no views about the reformulated arguments, because intuitionists are crazy! ;)
Member

rzach commented Nov 13, 2016

 They may be, but all I did was change the proof from the (confusing to students) "assume there is an enumeration of Pow(N) ....contradiction" to "lets show that every list of subsets of N must leave at least one set out".
Contributor

nicolewyatt commented Nov 13, 2016

 You are no doubt right that is pedagogically better. I am pretty sure that is what I say to students in class in any case.

rzach added a commit that referenced this issue Dec 18, 2016

``` fixing issue #107, replacing \Nat with \Int^+ when discussing enumara… ```
`…tions and formulating everything with total functions`
``` 5aa3649 ```