Immanuel Kant was convinced that he knew it all

[godelian]

Arithmetic has no axioms. ... Its propositions are all synthetic, without being derived from general concepts alone, but through the construction of magnitudes in time.

1781, Immanuel Kant, Critique of Pure Reason, A164/B205

https://en.m.wikipedia.org/wiki/Informal_mathematics

Informal mathematics means any informal mathematical practices, as used in everyday life, or by aboriginal or ancient peoples, without historical or geographical limitation. Modern mathematics, exceptionally from that point of view, emphasizes formal and strict proofs of all statements from given axioms. This can usefully be called therefore formal mathematics. Informal practices are usually understood intuitively and justified with examples—there are no axioms.

https://en.m.wikipedia.org/wiki/Peano_axioms

The axiomatization of arithmetic provided by Peano axioms is commonly called Peano arithmetic.

Gemini.

Peano's axioms were first published in 1889 by Giuseppe Peano in his book "The principles of arithmetic presented by a new method" (Latin: Arithmetices principia, nova methodo exposita). The book presented a formal system for defining natural numbers using a set of axioms.

If you do not like something, it is very unlikely that you will be any good at it:

On this account, I shall not reckon among my principles those of mathematics.

1781, Immanuel Kant, Critique of Pure Reason

Being utterly wrong, is what inevitably happens when you do not know what you are talking about. Immanuel Kant was truly the Grand Master of misguided word salads.

[Martin Peter Clarke]

Who isn't? Even Socrates was being prescriptive. What about you?

[Skepdick]

Being utterly wrong, is what inevitably happens when you do not know what you are talking about.

If we take "Don't know what you are taking about" -> "Being utterly wrong" as a valid implication.

Couple it with the observation that you have no idea what you are talking about when you talk about Mathematics; or the Platonic realm.

Then I guess it's a theorem that you are utterly wrong.

[godelian]

Couple it with the observation that you have no idea what you are talking about when you talk about Mathematics; or the Platonic realm.

This post is not about Platonism.

[godelian]

Who isn't? Even Socrates was being prescriptive. What about you?

I did not prescribe but describe a glaring error. Arithmetic does have axioms, unlike what Kant incorrectly prescribed/described on the matter.

[Skepdick]

I did not prescribe but describe a glaring error. Arithmetic does have axioms, unlike what Kant incorrectly prescribed/described on the matter.

Arithmetic does not have axioms. Arithmetic has axiomatizations.

The axiomatic systems produces by the process of axiomatization are not arithmetic.

If we find that our axiomatizations allow us to prove 2+2=5 we wouldn't conclude that arithmetic is broken. Instead, we'd conclude our axioms are inadequate and need revision.

Kant was wrong about many things. But not about this.

[Martin Peter Clarke]

Somebody with more patience and tolerance of your hate speech will have to quote you mate. Might be a long wait.

[godelian]

Arithmetic does not have axioms. Arithmetic has axiomatizations.

The axiomatizations are not arithmetic.

Well, what Kant implied, was that it is not possible to describe the foundations of the arithmetic system by a collection of rules expressed in (first-order) logic, similarly to Euclidean geometry. There are also alternative axiomatizations for geometry. What Kant meant, is that there is no axiomatization possible.

ChatGPT: Does arithmetic have axioms?

Yes, arithmetic has axioms. These are foundational rules or assumptions used to define the basic properties of numbers and operations like addition and multiplication. Most common system: Peano Arithmetic (PA)

Peano Arithmetic is a formal system that axiomatizes the natural numbers (0, 1, 2, …). Its axioms include:
Zero is a natural number.
Every number has a unique successor.
Zero is not the successor of any number.
If two numbers have the same successor, they are the same.
Induction axiom schema: If a property holds for 0 and holds for n implies it holds for n+1, then it holds for all natural numbers.
Addition and multiplication are also defined recursively within PA, and their properties (like associativity, commutativity, distributivity) can be derived from these axioms.

Why axioms?
Axioms serve as the starting point for building all theorems of arithmetic. They ensure that arithmetic reasoning is rigorous, consistent, and well-defined within a logical framework.

A consequence of Kant's view is that nothing would be provable about the natural numbers.

That was a wrong view, even already in 1781. Most notably, Fermat and Euler had already discovered quite a few theorems in arithmetic, while providing (informal) proofs. The deductive nature of arithmetic was already quite well understood. Kant does not mention Fermat or Euler in his Critique of Pure Reason. I even doubt that he was familiar with their otherwise famous work. Kant did not like mathematics, did not use it, but still felt confident enough to make incorrect statements on the matter.

If we find that our axiomatizations allow us to prove 2+2=5 we wouldn't conclude that arithmetic is broken. Instead, we'd conclude our axioms are inadequate and need revision.

I don't think so. There are surprising theorems in arithmetic. It does not lead to changing the axioms. It leads to accepting the results.

[Skepdick]

Arithmetic does not have axioms. Arithmetic has axiomatizations.

The axiomatizations are not arithmetic.

Well, what Kant implied, was that it is not possible to describe the foundations of the arithmetic system by a collection of rules expressed in (first-order) logic, similarly to Euclidean geometry. There are also alternative axiomatizations for geometry. What Kant meant, is that there is no axiomatization possible.

If he actually said that then he beat Godel to the realization.

I don't think so. There are surprising theorems in arithmetic. It does not lead to changing the axioms. It leads to accepting the results.

If anything surprises your core arithmetic intuition - it's no longer arithmetic.

You learned arithmetic as a child through counting, grouping objects, basic operations - not through studying axioms.
When the axioms surprise you - the axioms are always wrong as descriptions of arithmetic, even if they might be interesting as formal systems in their own right.

Surprise == new information.

[godelian]

Well, what Kant implied, was that it is not possible to describe the foundations of the arithmetic system by a collection of rules expressed in (first-order) logic, similarly to Euclidean geometry. There are also alternative axiomatizations for geometry. What Kant meant, is that there is no axiomatization possible.

If he actually said that then he beat Godel to the realization.

Gödel was perfectly happy to describe the foundations of the arithmetic system by a collection of rules expressed in (first-order) logic, similarly to Euclidean geometry. Gödel proved, however, that such axiomatization cannot be both consistent and complete. Gödel did not say that such axiomatization was not possible altogether.

Furthermore, comparing Gödel with Kant is quite a stretch. Gödel was an excellent mathematician. Kant was not. Kant was a philosopher who thought that it was possible to successfully philosophize about mathematics without knowing particularly much about it.

[Skepdick]

Well, what Kant implied, was that it is not possible to describe the foundations of the arithmetic system by a collection of rules expressed in (first-order) logic, similarly to Euclidean geometry. There are also alternative axiomatizations for geometry. What Kant meant, is that there is no axiomatization possible.

If he actually said that then he beat Godel to the realization.

Gödel was perfectly happy to describe the foundations of the arithmetic system by a collection of rules expressed in (first-order) logic, similarly to Euclidean geometry. Gödel proved, however, that such axiomatization cannot be both consistent and complete. Gödel did not say that such axiomatization was not possible altogether.

Furthermore, comparing Gödel with Kant is quite a stretch. Gödel was an excellent mathematician. Kant was not. Kant was a philosopher who thought that it was possible to successfully philosophize about mathematics without knowing particularly much about it.

You continue to miss the point for reasons that we will all gladly infer for ourselves.

An axiomatization of arithmetic is not arithmetic.

So the very notions of consistency or completeness become ill-defined.

What would it even mean for an axiomatization of arithmetic to be complete; or consistent with respect to arithmetic?
What the fuck would it even mean for a map of Paris to be consistent; or complete with Paris?

All the Gödel magic evaporates when you recognize that sentences have no agency to say anything about themselves.
"This sentence is not provable" says nothing unless you anthropomorphize agency into it.

It's really really simple! Can you delegate it to a machine? Is it mechanizable/computable? Can you encode its essence geometrically and into a formal language? That's it!

[godelian]

All the Gödel magic evaporates when you recognize that sentences have no agency to say anything about themselves.
"This sentence is not provable" says nothing unless you anthropomorphize agency into it.

Godel's syntactic template causes quite a bit of confusion:

S ↔φ(⌜S⌝)

It just expresses that sentence S has property φ. This sentence is not "talking about itself". People make too much of it.

It's really really simple! Can you delegate it to a machine? Is it mechanizable/computable? Can you encode its essence geometrically and into a formal language? That's it!

In a sense, I agree. If a machine cannot verify a proof, then it is not mathematics.

[Skepdick]

All the Gödel magic evaporates when you recognize that sentences have no agency to say anything about themselves.
"This sentence is not provable" says nothing unless you anthropomorphize agency into it.

Godel's syntactic template causes quite a bit of confusion:

S ↔φ(⌜S⌝)

It just expresses that sentence S has property φ. This sentence is not "talking about itself". People make too much of it.

I mean you can read those squiggles that way. It's just a meaningless formalism.

The English example is pretty straight forward "this sentence is unprovable".

In a sense, I agree. If a machine cannot verify a proof, then it is not mathematics.

Tell me how a machine verifies an infinite proof.

[godelian]

All the Gödel magic evaporates when you recognize that sentences have no agency to say anything about themselves.
"This sentence is not provable" says nothing unless you anthropomorphize agency into it.

Godel's syntactic template causes quite a bit of confusion:

S ↔φ(⌜S⌝)

It just expresses that sentence S has property φ. This sentence is not "talking about itself". People make too much of it.

I mean you can read those squiggles that way. It's just a meaningless formalism.

The English example is pretty straight forward "this sentence is unprovable".

The English sentence is not authoritative. It is only the sentence in first-order logic that matters:

G ↔¬prov(⌜G⌝)

A more literal interpretation in English is:

Unknown sentence G does not have the property "provable".

Gödel makes use of the diagonal lemma to prove that there is a nonempty set/class of such sentences G in arithmetic. I guess that you can also interpret it as:

This sentence does not have the property "provable".

Or even:

This sentence is not provable.

The following expresses that some sentence S is long:

S ↔long(⌜S⌝)

It is a stretch but you can probably interpret it as:

This sentence is long.

I am not a fan of that interpretation. I definitely prefer:

Some sentence S is long.

In a sense, I agree. If a machine cannot verify a proof, then it is not mathematics.

Tell me how a machine verifies an infinite proof.

ChatGPT

In infinitary logic, formulas and proofs can be infinitely long.

Such systems are not used in most of mainstream mathematics because:
They violate finitary constraints of ordinary formal systems (like ZFC or PA)
They cannot always be mechanically verified
Compactness and completeness often fail

https://en.wikipedia.org/wiki/Infinitary_logic

An infinitary logic is a logic that allows infinitely long statements and/or infinitely long proofs.[1] The concept was introduced by Zermelo in the 1930s.[2]

Some infinitary logics may have different properties from those of standard first-order logic. In particular, infinitary logics may fail to be compact or complete. Notions of compactness and completeness that are equivalent in finitary logic sometimes are not so in infinitary logics. Therefore for infinitary logics, notions of strong compactness and strong completeness are defined. This article addresses Hilbert-type infinitary logics, as these have been extensively studied and constitute the most straightforward extensions of finitary logic. These are not, however, the only infinitary logics that have been formulated or studied.

Considering whether a certain infinitary logic named Ω-logic is complete promises to throw light on the continuum hypothesis.[3]

According to the wikipedia page, infinitary logic is a legitimate and well-established research domain with potentially promising results.

[Skepdick]

The English sentence is not authoritative. It is only the sentence in first-order logic that matters:

G ↔¬prov(⌜G⌝)

I really just can't parse that... Can you give me semantics for the "↔" operator.

I don't even understand why this is a binary operator when both the LHS and RHS are a function of G.