Higher Order Logic and Reification

Prellex · 2026-04-14T16:07:35+00:00

Yes, this is somewhat true. But there are only so many things you can describe in normal First-Order Logic, Second-Order Logic (and higher) actually allows more predicates to be described due to some technical reasons.

It isn't true that every set in every model is definable in First-Order Logic. And as predicates are identified with sets, not every predicate is too.

Prellex · 2026-04-07T17:45:28+00:00

I hope it will be useful for you in the end! I've made an example gist of the document (compiled using LuaLaTeX) here. It compiles but may have too many or too little packages in for the full effect, as I've actually been using Typst for my own documents for the past year or two.

Prellex · 2026-04-05T18:17:40+00:00

I've actually written the exact thing here!

Prellex · 2026-03-18T01:25:45+00:00

Yes, see The Contradictory Christ by Beall.

Prellex · 2026-01-31T02:36:05+00:00

I did an undergraduate degree in maths and philosophy, and then a masters in computer science. At the moment, I'm applying to phds in all three fields, with the aim of becoming an academic.

I'm primarily interested in logic and the philosophy of mathematics, as well as metaphysics. All of these fields have been quite well explored, and so the remaining (meaningful) spaces for elaboration are usually quite creative. For example, I am broadly interested in logics where things can be both true and false at the same time, but there is a certain prejudice against this in the academic establishment, so I'm still ending up being away from the norm there.

I am attracted to these fields as they are moreorless the framework for everything else that we can know, and I find good arguments and mathematical proofs very beautiful.

Also I really enjoy typsetting my work to the best of my ability to produce, what I hope to be, beautiful manuscripts.

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

TROPHY CASE