Second-order arithmetic

[Demystifier]

First-order logic is not categorical https://en.wikipedia.org/wiki/Categorical_theory meaning that infinite models cannot be defined uniquely just by axioms. Second-order logic is supposed to avoid this problem, which is one of the motivations for second-order arithmetic https://en.wikipedia.org/wiki/Second-order_arithmetic . But on the other hand second-order logic lacks semantic completeness, i.e., if a property is valid in all models it does not imply that it can be proved by axioms. Isn't this a sort of contradiction? I mean, second-order logic should be able to define a unique model, but at the same time there can be a property of this model that cannot be proved by axioms. Have I misunderstood something? Is there something in second-order arithmetic which is true in the model, but cannot be proved by axioms?

 

[fresh_42]

I am no logician so forgive me if I missed the point. Do Trachtenbrot's theorem or Löwenheim-Skolem match your criteria?

Source: https://www.thi.uni-hannover.de/fileadmin/thi/abschlussarbeiten/hmueller-ba.pdf

The extension to the second order has therefore solved the problem of statements that are too complex by making it too complicated [for automatic constitution and checking of theorems] to be applied to such statements.

 

[Demystifier]

I am no logician so forgive me if I missed the point. Do Trachtenbrot's theorem or Löwenheim-Skolem match your criteria?

The first isn't relevant because it only applies to finite theories. The second isn't relevant because it only applies to first-order theories.

Source: https://www.thi.uni-hannover.de/fileadmin/thi/abschlussarbeiten/hmueller-ba.pdf

I don't speak German, but the claim that too complex is replaced by too complicated is interesting in a funny way.

 

[fresh_42]

The second isn't relevant because it only applies to first-order theories.

But wasn't that your question? Löwenstein-Skolem is valid in $\mathcal{L}_1$ but invalid in $\mathcal{L}_{11}.$

 

[Demystifier]

But wasn't that your question? Löwenstein-Skolem is valid in $\mathcal{L}_1$ but invalid in $\mathcal{L}_{11}.$

That's not my question. My question, or rather confusion, is apparent contradiction between the following two facts:
1. Löwenstein-Skolem is invalid in second order logic.
2. Completeness in the sense of https://en.wikipedia.org/wiki/Gödel's_completeness_theorem
is also invalid in second order logic.
How can both facts be true?

 

[fresh_42]

I don't speak German, but the claim that too complex is replaced by too complicated is interesting in a funny way.

Well, there was a small chance.

That's not my question. My question, or rather confusion, is apparent contradiction between the following two facts:
1. Löwenstein-Skolem is invalid in second order logic.
2. Completeness in the sense of https://en.wikipedia.org/wiki/Gödel's_completeness_theorem
is also invalid in second order logic.
How can both facts be true?

The paper proves both (chapters 4 and 7) so apparent doesn't hold for me. What more could be asked for than proofs? However, I admit I don't understand enough about the subject to follow the arguments. I tried to translate the paper but any automatism only applies to text and not to symbols so I gave up. This ...

is interesting in a funny way.

too, because the paper is too complex (second-order) to be translated by machinery (first-order).

 

[Bosko]

That's not my question. My question, or rather confusion, is apparent contradiction between the following two facts:
1. Löwenstein-Skolem is invalid in second order logic.
2. Completeness in the sense of https://en.wikipedia.org/wiki/Gödel's_completeness_theorem
is also invalid in second order logic.
How can both facts be true?

Can your question be formulated specifically for natural numbers?
I think it would be easier to find an answer that way.

For second-order logic, the original Peano axioms (including the second-order induction axiom) could be used.

Of course, the reduced ( to the first order ) axiom of induction would be used for first-order logic.

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

 

[Demystifier]

Can your question be formulated specifically for natural numbers?
I think it would be easier to find an answer that way.

Let me try this way.

In first order Peano theory:
- The Goodstein theorem cannot be proved from axioms.
- There are many inequivalent models, only one of them corresponds to the usual natural numbers.

In second order Peano theory:
- The Goodstein theorem can be proved from axioms.
- Are there many inequivalent models, or is there only one?
- Is there a property which is valid in every model, but cannot be proved from axioms?

 

[Bosko]

I cannot go deeper into this issue because it requires a lot of time for me that would not be used productively. For me, mathematics is just a tool for building a models of reality.

Edit:
Those imperfections, for me, have no practical significance, but are more philosophically important in terms of the limits of the mathematical model's power.
Also: Axioms of mathematics are only precise beliefs (they have no proof) and the logical method of deriving conclusions is only a striving for logical consistency.

It seems to me, although I am not sure, that you are making a mistake in the logical "sequence" (p=>q modus ponens). The only method for drawing conclusions.

If someone is from New York, then he is from America, but if he is not from New York, it does not mean that he is not from America.

The correct negation is that, if it is not from America it is not from New York.

Edit: The relationship between mathematics and its applications is like the relationship between linguistics and written works of literature

 

[Hornbein]

That's not my question. My question, or rather confusion, is apparent contradiction between the following two facts:
1. Löwenstein-Skolem is invalid in second order logic.
2. Completeness in the sense of https://en.wikipedia.org/wiki/Gödel's_completeness_theorem
is also invalid in second order logic.
How can both facts be true?

I feel like I'm missing something. L-S is not applicable because the conditions for the theorem are not met by second order logic. It's irrelevant so it can't contradict any other theorem about 2nd order logic.

Godel showed that 2nd order was either incomplete or inconsistent (everyone thinks its consistent, so...). "Completeness is invalid" is a non-standard way of putting it. Just "incomplete" is usual.

 

[fresh_42]

Let me try this way.

- Is there a property which is valid in every model, but cannot be proved from axioms?

How do you define valid in this context and wouldn't that turn the property into another axiom?

 

[Hornbein]

How do you define valid in this context and wouldn't that turn the property into another axiom?

You can make anything you like into an axiom but this is considered a poor way to prove something. I recall that there is the requirement that the number of axioms be finite. Otherwise you could just make every statement provable in another more powerful system an axiom and the system would then be complete.

 

[fresh_42]

You can make anything you like into an axiom but this is considered a poor way to prove something. I recall that there is the requirement that the number of axioms be finite. Otherwise you could just make every statement provable in another more powerful system an axiom and the system would then be complete.

That wasn't my point. The key here was "valid in any model, but unprovable". This would make the situation comparable to AC not to "anything".

I like a good polemic, but I think this isn't the place to exchange them. Whether your reply can be considered as good is another question. Your usage of the word poor was certainly offensive and off-topic.

 

[Hornbein]

That wasn't my point. The key here was "valid in any model, but unprovable". This would make the situation comparable to AC not to "anything".

I like a good polemic, but I think this isn't the place to exchange them.

But the axiom of choice isn't valid in all models. You can make the negation of the axiom of choice an axiom and the model is still valid but the now-not-an-axiom axiom of choice is false.

 

[fresh_42]

But the axiom of choice isn't valid in all models. You can make the negation of the axiom of choice an axiom and the model is still valid but the now-not-an-axiom axiom of choice is false.

That is why I asked what "valid" means here!

 

[Hornbein]

That is why I asked what "valid" means here!

IMO it would be better to not use that word about statements within a system and stick with true and false.

Models would be self-consistent or not. Informally one could say that a self-inconsistent model was invalid. They say that in such a model every statement is both true and false. I think that is sort of cool in its own way but then there is not much more one can say so it would not be a fecund source of PhD theses.

 

[Demystifier]

How do you define valid in this context and wouldn't that turn the property into another axiom?

By valid I mean true as in the Godel's completeness theorem for first-order logic:
https://en.wikipedia.org/wiki/Gödel's_completeness_theorem

A simple example is in group theory. There are models of group theory axioms in which all members of the group commute. For example, the group U(1) is one such model of group theory axioms. In U(1), it is true (or "valid") that all members of the group commute. I wouldn't say that this introduces additional axioms, would you?

 

[fresh_42]

By valid I mean true as in the Godel's completeness theorem for first-order logic:
https://en.wikipedia.org/wiki/Gödel's_completeness_theorem

A simple example is in group theory. There are models of group theory axioms in which all members of the group commute. For example, the group U(1) is one such model of group theory axioms. I wouldn't say that this introduces additional axioms, would you?

I would call it an axiom if it led to all groups being Abelian. Whether it is meaningful is a different question. As I already mentioned, I'm no expert in logic so let me ask a question in arithmetic. Will $1\neq 0$ be considered an axiom or a "valid statement"? More general: how can I be sure that something is valid in all models when there is neither a proof nor an axiom?

The definition in the Wikipedia article says:

In logic, specifically in deductive reasoning, an argument is valid if and only if it takes a form that makes it impossible for the premises to be true and the conclusion nevertheless to be false.

I read this as: Adding a valid statement to the set of axioms does not lead to inconsistencies. This is basically the situation AC is in. Such a statement would be indistinguishable from an additional axiom.

 

[Demystifier]

Will 1≠0 be considered an axiom or a "valid statement"?

It's not an axiom in my view. It's derived from the axiom "for any n, S(n)=0 is false" and the definition 1=S(0).

 

[fresh_42]

It's not an axiom in my view. It's derived from the axiom "for any n, S(n)=0 is false" and the definition 1=S(0).

And that is only an inconvenient way to make sure that $1\neq 0$ in my view. You can do - even though a very boring version of - arithmetic by allowing $1=0.$

 

[Hornbein]

I cannot go deeper into this issue because it requires a lot of time for me that would not be used productively. For me, mathematics is just a tool for building a models of reality.

Edit:
Those imperfections, for me, have no practical significance, but are more philosophically important in terms of the limits of the mathematical model's power.
Also: Axioms of mathematics are only precise beliefs (they have no proof) and the logical method of deriving conclusions is only a striving for logical consistency.

It seems to me, although I am not sure, that you are making a mistake in the logical "sequence" (p=>q modus ponens). The only method for drawing conclusions.

If someone is from New York, then he is from America, but if he is not from New York, it does not mean that he is not from America.

The correct negation is that, if it is not from America it is not from New York.

Edit: The relationship between mathematics and its applications is like the relationship between linguistics and written works of literature

"if someone is not from America he is not from New York." is the contrapositive, which always has the same truth value as the original statement. The negation should have the opposite truth value from the original statement. The negation of X is the not operator applied to X. I'm not certain but I think the negation is "if someone is from New York then he may or may not be from America."

 

[Hornbein]

The idea with axioms is to have as few as possible. Group theory has only four.

 

[pasmith]

"if someone is not from America he is not from New York." is the contrapositive, which always has the same truth value as the original statement. The negation should have the opposite truth value from the original statement. The negation of X is the not operator applied to X. I'm not certain but I think the negation is "if someone is from New York then he may or may not be from America."

"If someone is from New York, then they are from America" means "It is not the case that someone is from New York and not from America". Its negation is therefore "Someone is from New York and not from America".

We must also use the correc tquantifiers, so if the initial assertion is "For each person, if that person is from New York then they are from America" then the negation is "There exists a person who is from New York and not from America."

 

[Demystifier]

I've had a very fruitful discussion with ChatGPT about this stuff. Now I think I understand it much better, so let me present my own conclusions, expressed in my own words.

The key point is that, in sufficiently strong axiomatic systems, truth cannot be formalized, as shown by Tarski. This means that truth of some statements cannot be proved from axioms. Instead the truth in mathematics is sometimes determined by other means, such as intuition, or using stronger axiomatic systems (the axioms of which are themselves postulated through intuition). In particular, in second-order logic we quantify over all sets, but the notion of "all sets" cannot be formalized, at least not if "all sets" is interpreted in the full (rather than Henkin) semantics. Human mathematicians reason about "all sets" through these other non-formalized means. The true statements obtained this way are properties of the unique model described by second-order axioms interpreted with full semantics, but their truth cannot be proved formally within this second-order system of axioms. This explains why incompleteness of second-order logic (if a statement is true in all models, it does not imply that it can be proved from axioms) is not in contradiction with categoricity of second-order logic (the axioms can be such that a unique infinite model exists).

Or to make the long story short, truth and formal provability from axioms are different things. A lot of things is known by mathematicians to be true without having a formal proof.

 

[fresh_42]

Instead the truth in mathematics is sometimes determined by other means, such as intuition, ...

A lot of things is known by mathematicians to be true without having a formal proof.

I don't agree with these statements. There are four possibilities in mathematics as I see it.

1. Banach Tarski: Mathematics is not intuitive.
2. Axiom of Choice: Neither AC nor non-AC leads to contradictions.
3. Riemann Hypothesis: Not proven, yet.
4. Gödel: There are undecidable statements.

None of them falls in the category of intuition.

I remember a colloquium when Banach-Tarski was presented and the lecturer's main message was, that its apparent contradiction isn't due to the axiom of choice but to our unintuitive concept of points.

The axiom of choice could be phrased as: If there are baskets of buns, none of which is empty, can you choose a bun from each of them? Most mathematicians refuse to see a difference in whether there are finitely many, countable infinitely many, or uncountable infinitely many baskets and accept the axiom. The fact that set theory is without contradictions with or without the axiom of choice only created a separate branch of mathematics, one that does not use the axiom of choice. And that's what mathematics does: it splits into two different sets of axioms.

The Riemann hypothesis or the extended Riemann hypothesis are believed to be true and they are in a way closest to your statement of intuition versus proof. However, I am not convinced that intuition is the right word to describe the widespread belief that they are true. I think it's more the lack of finding counterexamples in such a large range: ten trillion zeros are on the critical line!, and the fact that algorithms that rely on them work, primarily in cryptology.

Last but not least, Gödel's incompleteness theorems are in my opinion statements that describe the boundary between mathematics and metamathematics or metaphysics as the more common term. It addresses the within in contrast to the outside. I think the subject of this thread is settled in the same context rather than in pure logic. Can we fully describe a language by using this language? I think we can't and every attempt has to fall back using the words for instance. Gödel's theorems formalize this point of view.

I do not see any example of a statement where mathematicians rely on intuition rather than proofs.

 

[martinbn]

...A lot of things is known by mathematicians to be true without having a formal proof.

What do you mean by this? Can you give examples?

 

[Demystifier]

I do not see any example of a statement where mathematicians rely on intuition rather than proofs.

What do you mean by this? Can you give examples?

Let me give some examples:
1. The Godel sentence "This sentence cannot be proved within the axiomatic system in which it is expressed." is true.
2. Peano axioms are consistent.
3. ZFC axioms are consistent.
All these statements are considered true, but cannot be formally proved within the system to which they refer. They, of course, can be proved within a larger system, but a larger system necessarily introduces additional axioms, which themselves are not formally proved, but taken as "obviously true" by intuition.

 

[martinbn]

Let me give some examples:
1. The Godel sentence "This sentence cannot be proved within the axiomatic system in which it is expressed." is true.
2. Peano axioms are consistent.
3. ZFC axioms are consistent.
All these statements are considered true, but cannot be formally proved within the system to which they refer. They, of course, can be proved within a larger system, but a larger system necessarily introduces additional axioms, which themselves are not formally proved, but taken as "obviously true" by intuition.

This is not a lot of things and these are all from the logic/set theory/foundations of math. I misunderstood you, I thought you meant from all areas of math. Somehow expected an example from differential equations or something like that.

 

[Hornbein]

Axioms are assumptions/assertions that cannot and aren't meant to be proven. You have to start somewhere. Usually they seem intuitively true but in a strict sense you aren't supposed to think that. Their value is that sets of axioms are the seeds of interesting mathematics. Take them or leave them.

The game is to minimize such a set of axioms. It is true that there are different sets of axioms that lead to the same logical structures and so are equivalent. That is, axioms in one of these sets can be used to prove any other such set. Choose one such set and go from there.

Euclid began all this back in 300 BC. His set of five axioms was controversial for 2000 years or so. The question was addressed by Hilbert in 1899. Hilbert proposed a set of 21 axioms of Euclidean geometry. It was later proved that one or more could be proved from other subsets of the axioms so they were demoted to theorems. In 2003 the axioms were challenged again as partially relying on intuition when the authors attempted to teach them to a computer. https://en.wikipedia.org/wiki/Hilbert%27s_axioms

I've been told that in Whitehead and Russell's Principia Mathematica the proof of 1+1=2 appears after about a hundred pages of preparation. You can see why mathematicians eventually lost interest in this sort of thing.

 

[fresh_42]

Let me give some examples:
1. The Godel sentence "This sentence cannot be proved within the axiomatic system in which it is expressed." is true.
2. Peano axioms are consistent.
3. ZFC axioms are consistent.
All these statements are considered true, but cannot be formally proved within the system to which they refer. They, of course, can be proved within a larger system, but a larger system necessarily introduces additional axioms, which themselves are not formally proved, but taken as "obviously true" by intuition.

I think these examples are not intuition versus proofs but axioms versus deductions. As I said ...

The fact that set theory is without contradictions with or without the axiom of choice only created a separate branch of mathematics, one that does not use the axiom of choice. And that's what mathematics does: it splits into two different sets of axioms.

and ...

... Gödel's incompleteness theorems are in my opinion statements that describe the boundary between mathematics and metamathematics or metaphysics as the more common term.

Yes, mathematicians shook themselves after the findings of Russell and Gödel, and continued. They introduced the term class in set theory, partly began with new branches with different axiomatic systems, and didn't allow metaphysics to become mathematics. You cannot expect to prove meta statements by means of the basic system.

Gödel's theorems formalize this point of view.

The alternative would have been what physics did. 124 years after Planck's paper, they still discuss the meaning and interpretations of quantum theory. I prefer mathematics's solution: adjust the axiomatic system if necessary, give it a new name, and continue, but do not confuse mathematics with metaphysics, or axioms with real-life truth, whatever this means.