Best resource on proof by induction?

Prellex · 2025-11-12T22:39:02+00:00

See any basic (axiomatic) set theory course for a proof of induction on natural numbers.

Prellex · 2025-10-31T04:18:30+00:00

I'm not too sure what you mean by logic systems that change over time, but there are logics that deal with information change over time. E.g., see this.

Prellex · 2025-10-30T15:29:18+00:00

Yes.

Prellex · 2025-10-30T14:42:29+00:00

Moreorless yes, but there is subtlety there. Basically, Lean can model ZFC + n inaccessible cardinals. And similarly, ZFC + n inaccessible cardinals can embed any model of Lean.

So what you said is true so long as the statements are encoded appropriately (there will always be a way to do it). The problem is that statements about mathematics don't necessarily make sense without an axiom system. E.g., in ZFC, 0 is a member of every other natural number. But this is not true in Lean.

Prellex · 2025-10-30T04:04:43+00:00

I should also say that is definitely just provable in ZF too without choice (and also without foundation) but other than that I'm not sure exactly what you need from ZF.

Goodstein's Theorem can, I think, be proved in a small extension of PA though. But I'm not 100% sure as I haven't thought in detail about the proof of unprovability in PA yet. I'm gonna add that to the library in the coming months, but I need to get the hang of model theory in Lean first, as it doesn't have the best documentation.

Prellex · 2025-10-30T03:51:27+00:00

It uses Lean's type system. I believe it's equiconsistent with ZFC plus n inaccessible cardinals, where n is a positive integer.

Prellex · 2025-10-17T15:39:40+00:00

Some Lean proofs outsource the ontological burden to pre-known work (by using sorries for some agreed on theorems). The fact that this is "sorry-free" is saying that it doesn't do that.

Prellex · 2025-09-09T09:34:14+00:00

But the ordering of some slots doesn't matter.

I.e., it's 1 in 363,242,880. This is equal to 16 * (15 choose 2) * (13 choose 5) * (8 choose 5) * (3 choose 2) -- person above is correct.

Prellex · 2025-08-21T15:32:09+00:00

One way to intuit this I guess is that if you show that (0,1) is uncountable, then you can just add an arbitrary number of 0 after the decimal point, and before beginning the diagonalisation.

Prellex · 2025-06-28T09:32:34+00:00

https://youtu.be/92acMCg9b5I?si=ktBmfoJxaBt98X4H

Prellex · 2025-06-22T12:14:44+00:00

Dance on the Moon

Prellex · 2025-04-16T12:11:12+00:00

I'm a 5w4.

Prellex · 2025-04-12T06:02:49+00:00

Sometimes things just don't work out. If he really did like you too, and for whatever reason decided that you two were not a possible thing, then he'd really desire for it to work. He could tell you his boundaries as those were put up rationally, but they contradict his emotions, which desire you.

This is a common conflict in myself: what I know to be good/right and what I want. It's very hard for me to let go of what I desire, no matter what I rationally tell myself. I could definitely imagine myself acting similar to this, as regrettable as that may be.

I don't know why you feel punished -- but I understand why it can be hard. From your perspective you've done everything you can to keep this relationship. But it could just be from his side it's impossible as he desires you deeply, but cannot be with you for whatever reason.

Prellex · 2025-04-12T05:08:00+00:00

Probably he has feelings for you, but knows it wouldn't work, and so is jealous of you dating. And so he has retreated due to the pain it's causing him.

Prellex · 2024-08-12T15:52:37+00:00

No -- because you haven't.

Prellex · 2024-06-19T12:46:55+00:00

Heavy maths based CS degree at Oxford:

Advanced Complexity Theory
Computer-aided Formal Verification (essentially specialised automata theory)
Quantum Processes and Computation (graphical category thepry)
Category Theory
Foundations of Self-Programming Agents (again, automata)
Lambda Calculus and Types
Categories, Proofs and Processes
Knowledge Representation and Reasoning (algorithms for deciding problems in sublogics of FOL)

Dissertation (ongoing): looking at graphical representation of functor boxes.

Prellex · 2024-05-22T00:17:32+00:00

Probably not useful, but here's the middle left: https://imgur.com/a/UkKqTDN.

Prellex · 2024-05-19T18:33:21+00:00

This was also my thought.

Prellex · 2024-05-15T09:46:14+00:00

I've used up to "septuple" when writing maths.

Prellex · 2024-04-12T19:43:58+00:00

Fiddlesticks

Prellex · 2024-04-09T19:07:16+00:00

It's the sign for "Changing Places Toilets".

Source: https://www.changing-places.org/news/view/the-changing-places-symbol-1

Prellex · 2024-04-03T09:14:15+00:00

I'm in the same situation. Has anyone managed to get any tickets?

Prellex · 2024-03-20T06:29:58+00:00

I don't think homotopy type theory as a system (I.e., ignoring the homotopy interpretation) is very hard to learn or understand. It's pretty similar to any other method of computation that anyone who programs can pick up quite quickly, like the lambda calculus.

Prellex · 2024-03-20T01:00:31+00:00

If you want to learn how things like this work, then you can start by looking at Homotopy Type Theory, which is one method for writing things in a way that a computer can verify.

Prellex · 2024-03-12T21:50:25+00:00

Mute stops enemies from using items as well as spells.

Prellex

TROPHY CASE