I Do you believe that continuum is Aleph-2, not Aleph-1?

[micromass]

You still didn't explain (or even made a hint) how category theory can replace logic.

Sorry forgot. First, I want to ask you what you think logic means. Do you think we need logic before set theory? Or are you talking about mathematical logic that is only developed once set theory is?

 

[Demystifier]

Sorry forgot. First, I want to ask you what you think logic means. Do you think we need logic before set theory? Or are you talking about mathematical logic that is only developed once set theory is?

I think of logic as something we need before set theory. (At least first order logic, admitting that second order logic can be thought of as "set theory in sheep's clothing".)

 

[micromass]

I think of logic as something we need before set theory. (At least first order logic, admitting that second order logic can be thought of as "set theory in sheep's clothing".)

The logic before set theory can't be modeled by category theory, but I wouldn't call that first order logic. In my opinion, first order logic requires set theory. First order logic can be done with category theory perfectly.

 

[Demystifier]

In my opinion, first order logic requires set theory.

Can you give an argument or a reference for that statement?

 

[stevendaryl]

In my opinion, first order logic requires set theory.

The semantics of first-order logic perhaps requires set theory, but first-order logic itself is just syntax plus rules of inference. It certainly doesn't require set theory. It would be circular if it did, because set theory is axiomatized using first-order logic.

 

[micromass]

Can you give an argument or a reference for that statement?

See any logic book, eg Hinman. It will work inside set theory already.

 

[micromass]

The semantics of first-order logic perhaps requires set theory, but first-order logic itself is just syntax plus rules of inference. It certainly doesn't require set theory. It would be circular if it did, because set theory is axiomatized using first-order logic.

What is your definition of first order logic?

 

[stevendaryl]

What is your definition of first order logic?

First-order logic is a language together with axioms and rules of inference for sentences in that language.

The language has:

• propositional operators: and, or, not, implies
• quantification operators: forall and exists
• function symbols
• relation symbols
• variables
• constants

The axioms (axiom schemas, actually) are things such as

Phi(t) implies exists x Phi(x)

The rules of inference typically are just modus-ponens and universal introduction.

 

[micromass]

How many variables do you typically have?

 

[Demystifier]

See any logic book, eg Hinman. It will work inside set theory already.

In that book, a formal discussion of set theory does not appear before Chapter 6. Of course, the concept of a set is used already in Chapter 1, but it is used only in the informal sense, not in the sense of set theory.

 

[micromass]

In that book, a formal discussion of set theory does not appear before Chapter 6. Of course, the concept of a set is used already in Chapter 1, but it is used only in the informal sense, not in the sense of set theory.

And uuh, what exactly IS a set in the informal sense? Note that he uses the axiom choice in the first two chapters too!

 

[Demystifier]

And uuh, what exactly IS a set in the informal sense?

A collection.

Note that he uses the axiom choice in the first two chapters too!

Uhh, perhaps it tells more about the book than about logic. I believe that most logic textbooks do not commit that crime.

 

[micromass]

A collection.

I have no problem with that. The problem is that from the outset, they start working with countable or otherwise infinite sets. It is my point of view that you can't do this without a formal set theory in place.

Uhh, perhaps it tells more about the book than about logic. I believe that most logic textbooks do not commit that crime.

Then your logic books do not treat the compactness theorem, completeness theorem and Löwenheim-Skolem theorems, all of which can be proven to need the axiom of choice!

 

[Demystifier]

Then your logic books do not treat the compactness theorem, completeness theorem and Löwenheim-Skolem theorems, all of which can be proven to need the axiom of choice!

OK, you convinced me, it's very hard to talk about logic without having some notions of sets. But the opposite, to talk about sets without having some notions of logic, is even harder. So where should we start? Should we completely abandon the idea that mathematics has a well defined foundation? (Or perhaps my avatar was right that we should found mathematics on type theory, no matter how much things become complicated then?)

 

[micromass]

OK, you convinced me, it's very hard to talk about logic without having some notions of sets. But the opposite, to talk about sets without having some notions of logic, is even harder. So where should we start? Should we completely abandon the idea that mathematics has a well defined foundation? (Or perhaps my avatar was right that we should found mathematics on type theory, no matter how much things become complicated then?)

See also this: http://mathoverflow.net/questions/22635/can-we-prove-set-theory-is-consistent

It's a chicken vs the egg problem. What comes first? Logic or set theory. In either case, we are forced to accept some non-formalized stuff. Either we accept some "god-given" logic, or we accept a "god-given naive set theory", or both. I don't see a way out of this. It is my personal believe that we can give an accurate but nonformal description (or intuition) of what logic is, what a proof is and what a set is. With these we can create formal logic and formal set theory. We can then prove a lot of cool theorems about logic and set theory. But these will not be theorems about our naive nonformal system. Rather, it will be theorems about the logic and set theory we mimicked inside our nonformal system.

 

[Demystifier]

See also this: http://mathoverflow.net/questions/22635/can-we-prove-set-theory-is-consistent

It's a chicken vs the egg problem. What comes first? Logic or set theory. In either case, we are forced to accept some non-formalized stuff. Either we accept some "god-given" logic, or we accept a "god-given naive set theory", or both. I don't see a way out of this. It is my personal believe that we can give an accurate but nonformal description (or intuition) of what logic is, what a proof is and what a set is. With these we can create formal logic and formal set theory. We can then prove a lot of cool theorems about logic and set theory. But these will not be theorems about our naive nonformal system. Rather, it will be theorems about the logic and set theory we mimicked inside our nonformal system.

That definitely makes sense!

But consider this. Let non-formal logic and non-formal set theory be called Log1 and Set1. Likewise, let Log2 and Set2 be their formal incarnations. And suppose that Log1 and Set1 are given. As the next step, what should we develop first, Log2 or Set2? So far I thought that Log2 should be formulated before Set2, but now it seems that it doesn't matter.

 

[micromass]

That definitely makes sense!

But consider this. Let non-formal logic and non-formal set theory be called Log1 and Set1. Likewise, let Log2 and Set2 be their formal incarnations. And suppose that Log1 and Set1 are given. As the next step, what should we develop first, Log2 or Set2? So far I thought that Log2 should be formulated before Set2, but now it seems that it doesn't matter.

Indeed, it doesn't matter so much. However, in my point of view, I reject any use of infinite sets in Set1 including the axiom of choice which is a statement about infinite sets. I am prepared to accept potential infinity. If we do this, then we cannot develop the completeness theorem or Löwenheim-Skolem theorem in Log2 unless you already developed Set2. So if I want to formalize Hinman's book in my pet system it goes as follows: non-formal logic and set theory first Log1 and Set1 then I create a formalized set theory (trying to avoid actual infinity) Set2 that satisfies ZFC or the finitely-axiomatizable NBG. Here is where Hinman begins where he develops Log2 then in a later chapter he develops axiomized set theory which is Set3

Of course, if you have no problems with infinite sets in your nonformal logic and stuff like the axiom of choice (I can imagine that you're a Platonist that accepts these universes as really existing), then you can work entirely inside Set2 and Log2 and there is no reason for a Set3

But whatever we do we always can go on: we can build inside Setn a logical system Logn+1 and a set theory Setn+1

 

[Demystifier]

I reject any use of infinite sets in Set1 including the axiom of choice

This is something I always thought but was afraid to say. Thanks for spelling it explicitly!

 

[Stephen Tashi]

What comes first? Logic or set theory.

In addition to that question, we can ask when the notion of "order" is to be introduced.

Before we can observe that an author did one thing before another, we must have the notion of things being done in some order.

 

[Demystifier]

Before ...

And before defining the word "before" we must first define some words before that.

 

[stevendaryl]

How many variables do you typically have?

If you're saying that you need to already have an informal notion of a collection in order to make sense of logic, that's probably true. But you certainly don't need any set theory. Set theory is a theory of sets. I wouldn't say that any time someone mentions a collection, they are using set theory.

 

[stevendaryl]

Indeed, it doesn't matter so much. However, in my point of view, I reject any use of infinite sets in Set1 including the axiom of choice which is a statement about infinite sets. I am prepared to accept potential infinity. If we do this, then we cannot develop the completeness theorem or Löwenheim-Skolem theorem in Log2 unless you already developed Set2.

The Lowenheim-Skolem theorem is a theorem ABOUT first-order logic. That doesn't mean that you need it to do first-order logic. Set theory is required to prove facts about the natural numbers, but children learn to use natural numbers before they learn set theory.

You do not need set theory in order to use first-order logic, even if set theory is used to study first-order logic.

 

[micromass]

If you're saying that you need to already have an informal notion of a collection in order to make sense of logic, that's probably true. But you certainly don't need any set theory. Set theory is a theory of sets. I wouldn't say that any time someone mentions a collection, they are using set theory.

In usual definitions of first order logic they set a countable collection of variables. Furthermore, there is an infinite collection of ZFC axioms. Countable and infinite do not make sense outside of an axiomatic set theory.

 

[micromass]

but children learn to use natural numbers before they learn set theory.

That is irrelevant. If you take the natural numbers as a priori knowledge that is god given, then so be it. But you need to be specific about it. In the same way, you need a set theory in order to define first order logic.

 

[micromass]

The Lowenheim-Skolem theorem is a theorem ABOUT first-order logic.

And uh, in what system are you proving things about first order logic?

 

[stevendaryl]

That is irrelevant.

No, it's not. It's clearly true that you don't need set theory in order to do arithmetic. You don't need set theory in order to do first-order logic. If it is possible to do X without knowing anything about Y, then I would say that X does not need Y.

In the same way, you need a set theory in order to define first order logic.

I would say "In the same way, you DON'T need set theory in order to define first order logic".

I certainly learned first-order logic before I learned set theory, and it was invented before set theory was invented, so what exactly do you mean by saying that you "need" set theory? I can teach someone how to do proofs in first-order logic without ever mentioning sets, so how, exactly, do I "need" set theory? I really don't understand what you're talking about.

 

[stevendaryl]

And uh, in what system are you proving things about first order logic?

That doesn't matter, but I assume it is in an informal system of first-order logic plus set theory. There is a distinction between doing first-order logic and proving things about first-order logic. Set theory typically is needed for the second, but not for the first.

 

[stevendaryl]

In usual definitions of first order logic they set a countable collection of variables. Furthermore, there is an infinite collection of ZFC axioms. Countable and infinite do not make sense outside of an axiomatic set theory.

Once again, you're confusing (1) proving things about first order logic with (2) using first order logic. You need set theory (or something similar) to do (1), but not (2). You can prove, using set theory, that there are an infinite number of axioms of ZFC. But that doesn't mean that you need set theory in order to say what the axioms of ZFC are. ZFC is specified using axiom schemas. That means that you give a pattern for an axiom, and any first-order logic sentence that matches that pattern is an axiom. You can certainly prove using set theory that there are infinitely many axioms matching the schema, but such a proof is not needed to do set theory.

 

[micromass]

No, it's not. It's clearly true that you don't need set theory in order to do arithmetic. You don't need set theory in order to do first-order logic. If it is possible to do X without knowing anything about Y, then I would say that X does not need Y.
I would say "In the same way, you DON'T need set theory in order to define first order logic".

I certainly learned first-order logic before I learned set theory, and it was invented before set theory was invented, so what exactly do you mean by saying that you "need" set theory? I can teach someone how to do proofs in first-order logic without ever mentioning sets, so how, exactly, do I "need" set theory? I really don't understand what you're talking about.

Why does it matter what you can teach? This is s a discussion on how to formalize mathematics, not on how to teach it. I can very easily teach calculus without limits, does that mean that it's not necessary.

 

[micromass]

Once again, you're confusing (1) proving things about first order logic with (2) using first order logic. You need set theory (or something similar) to do (1), but not (2). You can prove, using set theory, that there are an infinite number of axioms of ZFC. But that doesn't mean that you need set theory in order to say what the axioms of ZFC are. ZFC is specified using axiom schemas. That means that you give a pattern for an axiom, and any first-order logic sentence that matches that pattern is an axiom. You can certainly prove using set theory that there are infinitely many axioms matching the schema, but such a proof is not needed to do set theory.

I see you conveniently ignored the necessity of countably many variables.

And now you talk about axiom schema's. I thought you said first-order theories required axioms? What's an axiom schema then?