Timeline for Can this weakish system of arithmetic express multiplication for second-sort numbers?
Current License: CC BY-SA 4.0
14 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Dec 29, 2023 at 16:35 | answer | added | abo | timeline score: 1 | |
| Jun 3, 2021 at 7:44 | history | edited | David Roberts♦ | CC BY-SA 4.0 |
Added link, slight cleaning of markdown
|
| Jun 3, 2021 at 7:39 | comment | added | David Roberts♦ | @abo good to see you again! | |
| Jun 3, 2021 at 7:24 | history | edited | abo | CC BY-SA 4.0 |
added 12 characters in body
|
| Jun 2, 2021 at 22:37 | comment | added | abo | @James Hanson. I've tried to answer your question by adding an Appendix. | |
| Jun 2, 2021 at 22:35 | history | edited | abo | CC BY-SA 4.0 |
Tried to answer James Hanson's question in comments.
|
| Jun 2, 2021 at 19:59 | comment | added | James E Hanson | @abo Under the assumption of $\text{top}$, multiplication isn't going to be a total function. Are asking if the graph of multiplication as a partial function is definable? | |
| Jun 2, 2021 at 19:06 | history | edited | user44143 | CC BY-SA 4.0 |
reformatted
|
| Jun 2, 2021 at 16:10 | history | edited | abo | CC BY-SA 4.0 |
added 468 characters in body
|
| Jun 2, 2021 at 15:46 | comment | added | user44143 | Thanks, that clarifies the first question, and with that I can answer the second question well enough. It's probably worth mentioning the difference between finite and infinite cases in the post. | |
| Jun 2, 2021 at 15:30 | comment | added | abo | @Matt F. For your second question, one can obviously compose functions. If F(t) is a term, and G is a function, then G(F(t)) is a term. Perhaps I am misunderstanding your question? | |
| Jun 2, 2021 at 15:26 | comment | added | abo | @Matt F. For your first question. There are two cases: there exists a maximum (top), or there doesn't (inf). In the case of top, the axiom scheme for unique choice is a theorem for any $\phi$, provable by induction using the wff ($\forall x≤n \exists ! y \phi(x,y)) \rightarrow (\exists F \forall x≤n \phi(x,F(x)))$. In the case of inf, it's not a theorem. OTOH, in the case of inf, there clearly is a formula which represents multiplication for second-sort numbers even when functions are limited to unary functions, so I'm not sure of the relevance of the question. | |
| Jun 2, 2021 at 14:42 | comment | added | user44143 | Or is there an axiom scheme for unique choice, i.e. $(\forall x\, \exists! y\, \phi(x,y))\to (\exists F\,\forall x\, \phi(x,F(x)))$? Or is there at least a binary operation for composition of functions? | |
| Jun 2, 2021 at 8:05 | history | asked | abo | CC BY-SA 4.0 |