Is the category of all axioms a small category or a large category?

Is the category of all axioms a small category or a large category?

Other urls found in this thread:

ncatlab.org/nlab/show/syntactic category
docs.google.com/forms/d/e/1FAIpQLSeTCgXK20O9XzS2ltzcQjrBhHJiU7w442Cg3a4XP0lvVhtNXQ/viewform?usp=sf_link
youtu.be/CAUo5aNmvz8
en.wikipedia.org/wiki/Arrow's_impossibility_theorem
en.wikipedia.org/wiki/Comparison_of_electoral_systems
youtu.be/T9z3YQkKCLo)
twitter.com/SFWRedditGifs

I don't know what a category is but aren't there only like ten axioms in ZFC? Sounds small to me.

>he thinks that ZFC is the smallest theory
>not Peano Arithmetic

lmao that's like 2 axioms, 0 being a natural number and that 0 has a successor.

Sorta related:

What do working theoreticians think of HoTT?

I can't take it seriously because HoTT-Coq sounds like gay porn.

zfc has literally infinite axioms dude

You may want to rethink that statement

>this retarded system
>Peano
How do you get arithmetic from these axioms? How do you know it exists? In your system: 1=4, 1=/=4, 1=/=1, 1=0, etc.

>1=4
Well no, because 4 isn't the first (1) successor of 0. If σ is the successor function, then you get the number four (4) at the fourth recursion: σ(σ(σ(σ(0)))) = 4.

Now I'm interested, how would that category work?

I know there's a category of all mathematical statements, where a morphism from P to Q amounts to a proof of Q from P (under some ambient axiomatic system).

You could consider the category of all axioms (say, in ZFC) as a full subcategory, but it doesn't sound particulary interesting.

You didn't prove sigma is surjective

Axiom 1:
(i) ℕ is a set
(ii) 0 ∈ ℕ
(iii) σ : ℕ --> ℕ
Axiom 2: ~(∃n ∈ ℕ | σ(n) = 0)
(I.e. zero is not a successor)
Axiom 3: ∀x,y ∈ ℕ : σ(x) = σ(y) ==> x=y
(Sigma injective)
Axiom 4: Suppose S ⊆ ℕ such that
(i) 0 ∈ S, and
(ii) n ∈ S ==> σ(n) ∈ S, for an arbitrary n ∈ ℕ.
Then:
S ⊆ ℕ ⋀ 0 ∈ S ⋀ [∀n(n ∈ S ==> σ(n) ∈ S)] ==> S = ℕ

Axiom 4 makes σ surjective over its codomain ℕ by induction

>N is a set

Wrong

>ℕ is a set
Not really. First, because Peano is independent of set theory and second because if "N is a set" was an axiom then there is the implicit axiom of "sets exist" which means that implicitly you are assuming all the axioms of set theory, and that defeats the purpose of the exercise.

Retarded undergrad students may internet Peano as the set of axioms that say "N is a set" but in reality the whole of axioms of Peano tell us that N may be treated like a set. For example, the first axiom tells us that [math] 1 \in \mathbb{N} [/math] is a valid statement.

This does not mean that N is a set in the sense of formal set theory, all it says is that within this theory you can invoke the sentence [math] 1 \in \mathbb{N} [/math] when writing a proof. You may even interpret this axiom informally as "1 exists".

Norman pls go

How do you fuck up this much with only two axioms?

This is even worse than the phenotype meme

"all axioms" will depend on the language you want to talk about.

Given a set theory U, you can take any set X and consider the group G = (X, id_X) with one element (the identity). Of course, those groups are all isomorphic. Nevertheless, it means you have a group for each set, and thus the class of all such object doesn't form a set.
I suppose in a similar way, you could attempt to argue that for each set X, you can take the predicate P_X the uniquely characterizes X, and take e.g. "there exists and A such that P(A)" as an axiom. Then all such axioms alone would form a class and the corresponding category wouldn't by U-small.

If I needed to make sense of the question, really, I'd take it you speak of the syntactic category for a theory
ncatlab.org/nlab/show/syntactic category

The set of all strings of finite length is countable. The set of all axioms is a subset of the set of all strings of finite length.

>inb4 >set

>The set of all strings of finite length is countable.
define "string"

What if the strings use characters from an infinite alphabet?

If they are finite sentences in a finite or countably infinite alphabet it is small

Functions from {1..n} to an alphabet of characters.

All axioms that can be stated by humans are stated in finite languages.

*languages with a finite alphabet

I am writing a research paper on the logistics of increasing renewable energy. Part of the paper is conducting an investigation, so I am doing a survey concerning people's opinions on the topic. It focuses on renewable and fossil fuel energy, nothing on nuclear, so sorry if you're passionate about that. Please help out by responding. Here's the link: docs.google.com/forms/d/e/1FAIpQLSeTCgXK20O9XzS2ltzcQjrBhHJiU7w442Cg3a4XP0lvVhtNXQ/viewform?usp=sf_link

Sorry, I did not mean to post this here.

You forgot these:
- The successor function is injective
- Zero is not the successor of any natural number

Otherwise the algebraic structure ({0}, S) where S(0) = 0 would satisfy your axioms.

It's true. Specification and replacement are axiom schemas (infinite sets of axioms). NBG set theory is finitely axiomatized though.

The successor is not surjective. It is injective. Consider zero.

Hi Nikolaj. How have you've been? Haven't see you here for quite a while

I fell for the cryptocurrency meme and got into smart contract programming
youtu.be/CAUo5aNmvz8

Right now I'm coding a decentralized voting dApp and want to implement some of the many systems. Here are some pointers

en.wikipedia.org/wiki/Arrow's_impossibility_theorem
en.wikipedia.org/wiki/Comparison_of_electoral_systems

I'm open for all kinds of contributions, whether on the logic, overview or coding side, and it's easy money on the side too. Write me :^)

Also, I think, in what I said before,
>the predicate P_X the uniquely characterizes X
was a blunder

I envy how you manage to cover so many subjects. You definitely got talent unlike me.

Meanwhile, I still try to land a career in academia and so far it's been damn hard. Mostly due to lack of talent.

Also, it was I who had some talks with you on constructive math over here.

Well in math it all comes together.

What was your stance in in constructive math? In the blockchain world, I actually reached out (youtu.be/T9z3YQkKCLo) to a startup that uses F*, a dependently typed language, to do "on chain" financial transactions. I was about to try and write a compiler for that NEO blockchain in Haskell, but the community has other needs.
I don't like when people talk themselves down like you do. Sure, whether you make it is a game of luck (like who wants to be a millionair), but not slowing down a a minimum criteria. If you find time and are somewhere interested, really look if this voting topic interests you. You can also easly make 10^4 moneys in the blockchain world for afternoon jobs right now. I wrote a trading bot (for bittrex with python) some months ago and will also continue to work on that next August, for people interested.

Where is it hard and with what topic?