Timeline for What happens when we print the digits of a real number?
Current License: CC BY-SA 2.5
3 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 28, 2010 at 19:54 | comment | added | Carl Mummert | "Any constructive theorem must remain true if you replace subterms with extensionally equal terms" - this is not true, strictly speaking. It assumes that the constructive system contains, or can prove, extensionality axioms for the type of objects in question. There are constructive theories that have only very weak extensionality properties and cannot prove, in general, that two extensionally equal objects must satisfy the same formulas. | |
| Jul 28, 2010 at 9:19 | comment | added | Neel Krishnaswami | Any constructive theorem must remain true if you replace subterms with extensionally equal terms, but the print-an-approximation operation cannot honor this. So I want to know if there is some way to extend constructive logic with some way of using this operation without wrecking the logic (ie, by breaking the equality relation). | |
| Jul 28, 2010 at 8:03 | history | answered | Per Vognsen | CC BY-SA 2.5 |