15 May 2022 |

BabySnake | because its axioms lead to the principle of explosion | 21:12:07 |

DiscoDoug | You’d want to be able to show you satisfy the axiom with something like bijection and not simply say “they’re equal” | 21:12:28 |

DiscoDoug | Garkelein showed why this axiom is necessary. | 21:13:02 |

BabySnake | if you add a theorem which is provably not true given the other axioms as an axiom your new axioms are not consistent | 21:13:02 |

BabySnake | the assertion that all E which satisfy the first 4 axioms are all isomorphic is provably untrue | 21:13:37 |

BabySnake | so if we assert it /is/ true, then we have a statement which is both true and false | 21:13:50 |

BabySnake | which is the principle of explosion | 21:13:55 |

BabySnake | which makes the theory inconsistent | 21:13:59 |

DiscoDoug | Proving that you can’t invent something is clearly harder | 21:14:06 |

BabySnake | all models of N being isomorphic is a consequence of the second order inductive axioms | 21:14:29 |

DiscoDoug | I’m not sure why I’m not getting my point across but I’m running out of ways to say the same thing. | 21:14:56 |

DiscoDoug | It isn’t a consequence. | 21:15:05 |

DiscoDoug | That’s why there even is a fifth axiom. | 21:15:24 |

DiscoDoug | You don’t toss in an axiom for giggles. | 21:15:42 |

BabySnake | but its not an axiom | 21:15:49 |

BabySnake | I dont know where he got it from but thats not an axiom | 21:15:56 |

DiscoDoug | I can only wish you good luck at this point. | 21:16:22 |

BabySnake | Its a theorem of PA when you have the inductive axioms | 21:16:28 |

BabySnake | Garklein where did you get that original image from? | 21:16:34 |

BabySnake | Unless were implicitly defining E to be from some predicate P, then its the inductive axiom | 21:17:35 |

BabySnake | but thats what I said the other day is maybe its a weird way of writing the inductive axioms | 21:17:47 |

DiscoDoug | I’m out of ways to make this point. Sorry. | 21:18:07 |

DiscoDoug | From the wiki on Peano axioms: “The intuitive notion that each natural number can be obtained by applying successor sufficiently often to zero requires an additional axiom, which is sometimes called the axiom of induction.” | 22:38:04 |

16 May 2022 |

| nikyq#8590 changed their display name from nikyq to nikyq#8590. | 06:18:34 |

| @idahotokens:matrix.org joined the room. | 11:17:21 |

| dzaima banned @idahotokens:matrix.org. | 15:03:41 |

kamila | Download image.png | 18:06:17 |

kamila | i love spotting tiny gems like these in source code | 18:06:24 |

Brian E#0926 | lol | 18:13:12 |

Garklein#9297 | it's from oskar31415's youtube channel banner | 18:59:06 |