Logic - 2018-03-04

MatheinBoulomenos

3:11 PM

@user21820 hello

user21820

@MatheinBoulomenos: Hello!

MatheinBoulomenos

Do you know this book? springer.com/de/book/9781447145578

user21820

@MatheinBoulomenos No I don't. However, I first read about Gentzen's LK and LJ on Wikipedia, which you may be interested to look at if you haven't already:

Sequent calculus

Sequent calculus is, in essence, a style of formal logical argumentation where every line of a proof is a conditional tautology (called a sequent by Gerhard Gentzen) instead of an unconditional tautology. Each conditional tautology is inferred from other conditional tautologies on earlier lines in a formal argument according to rules and procedures of inference, giving a better approximation to the style of natural deduction used by mathematicians than David Hilbert's earlier style of formal logic where every line was an unconditional tautology. There may be more subtle distinctions to be made...

A curious feature of LK is that it is perfectly symmetric for classical logic, but the symmetry is gone for intuitionistic logic.

MatheinBoulomenos

Yeah, intutionistic logic is treated in this book and I want to learn that a bit at some point, not because of some foundational skepticism on my part, but because it shows up in categorical logic

user21820

@MatheinBoulomenos Oh. Intuitionistic logic is in my opinion better understood (and compared with classical logic) in a Fitch-style system, not a sequent-style system.

MatheinBoulomenos

3:26 PM

As a comment on that lemma about extensions of field homomorphism, I wanted to show you that as an example of a proof technique that is commonly used in algebra that you would probably find problematic. This result is used (also for uncountable fields) frequently in field theory and algebraic number theory. Infinite Galois theory wouldn't work without that and infinite Galois theory is commonly used in algebraic number theory or algebraic geometry over fields which are not algebraically closed

It's even worse: most papers in arithmetic geometry cite SGA4 (or cite a paper that cites SGA4 etc.) and SGA4 works with Grothendieck universes

user21820

@MatheinBoulomenos I'm aware that a lot of set theorists and algebraists like the kind of results that in some sense can only be obtained in a set-theoretic universe that is 'ideal'. As you probably know, I find it problematic in the same way I do not think elegance is a good criterion if we are actually concerned with truth.

For example, elegance is what drove Hilbert's dream that there is a proof in a foundational system of its own consistency. It's also why a lot of set theorists like to assume AC rather than not assume it. It's also why the early pioneers in foundations thought there would not be a problem in identifying set and ( set → bool ), to phrase it from a modern type theory viewpoint.

And it's practically the sole reason for having the axiom of foundation in ZFC. I think even algebraists (who aren't set theorists) don't care about foundation haha..

MatheinBoulomenos

3:45 PM

yeah, I don't really care about foundation

user21820

@MatheinBoulomenos Until it proves a contradiction and hence proves the negation of every theorem you have proven? =)

MatheinBoulomenos

I don't think that's going to happen

user21820

Or perhaps it proves that itself proves a false arithmetical sentence. This is a more subtle problem, but would still doom the system. And this is what I personally worry about when it comes to ZFC. I don't actually believe ZFC is inconsistent, but I don't see clear evidence that ZFC is arithmetically sound.

MatheinBoulomenos

But how do we know what true arithmetical sentences are?

user21820

We don't, but any reasonable meta-system MS has its notion of N. ZFC can be used as a meta-system, and so if ZFC proves "ZFC proves 'not P' for some false arithmetical sentence P", then ZFC is doomed.

MatheinBoulomenos

3:51 PM

Is there any reasonable system that we know is arithmetically sound?

user21820

@MatheinBoulomenos As for what's going to happen in the future, I'm sure you know that Frege had more or less completed his voluminous work without realizing his system was inconsistent due to Russell paradox. Also, lest you think this is an isolated incident, note that there have been many other attempts at foundations throughout history including in recent proof systems that turn out to have subtle inconsistencies.

@MatheinBoulomenos As far as I can see, the only way we can ever hope to be quite sure of arithmetical soundness is via philosophy and empirical evidence. So I am quite confident that ACA is arithmetically sound.

And ACA can be extended further to higher-order in a predicative fashion. I am confident that those are all arithmetically sound too.

MatheinBoulomenos

I'm not saying noone should worry about foundations. But I don't want to

user21820

I know.

=)

It can give one a splitting headache.

MatheinBoulomenos

And elegance and generality are still important criteria for me. For example, constructive commutative algebra is nice and valuable, but I don't want to restrict myself to polynomial rings in finitely many variables over a restricted set of fields.

Prime ideals are absolutely essential for doing abstract commutative algebra. Without some form of choice, there are non-zero commutative rings without prime ideals

I don't mean necessarily criteria for truth

skullpatrol

Elegant simplicity rarely gives anyone a splitting headache :P

user21820

4:02 PM

@MatheinBoulomenos Actually I don't quite understand what you mean here. I'm saying that ultimately we cannot afford to have an unsound foundation. Either we believe that our foundation (such as ZFC plus whatever extra axioms we want) is arithmetically sound, and happily work within it, or we have to be extremely careful if we aren't sure. Because it's better to have inelegant and restricted theorems that are true, than to have elegant theorems that are false.

@skullpatrol Russell's paradox was elegant and simple, and I bet it gave Frege a headache. =P

skullpatrol

Russell was a giant :P

user21820

@MatheinBoulomenos But I wish to say something about what we can do even without foundations as 'daring' as ZFC.

MatheinBoulomenos

@user21820 okay sure, we need to believe in the foundations we work with. But I can still value elegant and general mathematics over inelegant and specialized mathematics

skullpatrol

But, yes you do have a point about the limitations of human language @user21820

user21820

Like what I did for algebraic closures, the core algebraic fact is that given any field F and a well-ordering of F, we can construct the algebraic closure of F in a manner that is difficult to dispute is sound, and prove its uniqueness up to isomorphism. I would say that this is the actual content of the fact, and it should be very independent of foundations.

MatheinBoulomenos

4:07 PM

The existence of maximal ideals only depends on the boolean prime ideal theorem

user21820

I'm not sure about that; they are proving equivalent to BPIT over ZF.

I'm talking about the foundations-independent core fact.

The non-algebraic part of the usual statement that is dependent on foundations is the part where we construct a well-ordering of F. This may not always be possible in foundations that are not as daring as ZFC, because after all ZFC arose from the attempt to retain the boolean set membership and identification of set and ( set → bool ) but curtail it to try to avoid inconsistency.

So it's just like the situation before and after ZFC. Many results in mathematics will be only a bit affected if someone finds a problem in the foundations.

MatheinBoulomenos

In the past, how long did it take to discover these inconsistencies?

skullpatrol

You forgot to mention Wittgenstein?

user21820

@skullpatrol What about him? A lot of what he says does not seem to have much value with respect to foundations of mathematics...

@MatheinBoulomenos I don't know much, but apparently Russell himself didn't discover his paradox directly either, but came via an indirect route.

skullpatrol

nvm, this is getting too philosophical for my limited abilities

user21820

4:18 PM

plato.stanford.edu/entries/russell-paradox mentions that the Burali-Forti paradox was discovered earlier in 1897, and Russell discovered his in 1901.

I found this HSM post, but only glanced through it:

9

A: How did Russell arrive at the paradox demonstrating the inconsistency of naive set theory?

Russell was not the first to discover "his" paradox. By June 1901 when he arrived at it (it was not published until the first edition of Principia in 1903), it was already known for a while to the Hilbert's circle at Göttingen. Russell did not belong to that circle, so his rediscovery was indepen...

I think if ZFC is inconsistent a proof of contradiction may not be easy to find. This reminds me; at one point Reinhardt cardinals were thought to be an elegant closure to all the large cardinal axioms for ZFC. And then later they were found to be inconsistent with ZFC (but not yet known to be inconsistent with ZF).

From the Wikipedia page on that, there is an interesting linked PDF that suggests that very likely there is a system involving ZF plus Berkeley plus some choice that has a deep inconsistency.

Berkeley cardinals are even stronger than Reinhardt cardinals, but also still not known to be inconsistent with ZF.

Oh and there's this joke:

62

A: What if Current Foundations of Mathematics are Inconsistent?

If I found an inconsistency in mathematics, I would write up solutions to the six remaining Clay problems, collect my six million, retire and let you guys sort out the mess.

Anyway I've to go off soon, so see you all next time! =)

MatheinBoulomenos

4:41 PM

See you @user21820

Transcript for

♦ $Mathematics$ Logic

Transcript for

♦ Logic

♦ $Mathematics$ Logic