Logic - 2019-06-15

user21820

10:44

@user2103480 It does, but I'm not a researcher in mathematical pedagogy, so all I can provide to you is my personal experience. Firstly, when I was an undergraduate student, I used my Fitch-style system in every single course I took, including for examinations, after I learnt about Fitch-style in a first-year course and adapted it to be user-friendly.

Not one of my professors failed to understand my Fitch-style proofs (precisely because of my adaptations), and during at least two exams I caught an invalid quantifier switch that I had performed in an intuitive leap when brainstorming before writing out a formal proof. Without my system, it is entirely possible for me to have made those mistakes, and indeed one classmate made exactly the same mistake in one case, and took a while to be convinced of the mistake after the exam.

That's me. I've taught quite a number of students the same Fitch-style system as well, and all the students who put in the effort to learn to use it also appear to stop making the various logical errors that are common among students.

Furthermore, even those who have not mastered using the system, but who at least understand the system, can more easily understand explanation of any logical errors they make, when their attempt is translated to Fitch-style to make clear where the problem is.

user2103480

Academically, I feel similarly. I studied vellemans "how to prove it" before I started uni, and he manages pretty pretty well to teach informal natural deduction

user21820

@user2103480 I totally agree! That very book is one of those I recommend for beginners!

in Basic Mathematics, Jun 6 '18 at 17:05, by user21820

How to Prove It is a good introductory book to real mathematics, that is, definitions and theorems and proofs.

user2103480

11:00

It helped me tremendously, and while almost all the other students struggled during the first year, it was a breeze to me, in contrast to my experiences in school

user21820

@user2103480 I am very not surprised by that. Incidentally, I learnt logic from many years of olympiad experience, which was before reading that book, so I cannot estimate its effect on me. But when I read it I found it very nice, and it's a pity most students never read it.

user2103480

@user21820 Yeah, and if I could, I would rewrite the german syllabus to include an intro to proofs course. It was horrible to watch (and years later, correct as a TA) the proof attempts of fellow students. Ofc you cannot blame it on them, how should they deduce by just a few examples how first order logic works?

(And in addition to that, the formalization of objects like functions in the language of set theory)

user21820

@user2103480 Exactly my feeling. As a TA, I always spend at least one lesson to try to explain the core ideas of Fitch-style deduction, namely contexts (represented via indentation), which include the if-subcontext and ∀-subcontext, and show how proof-by-contradiction is completely transparent from the Fitch-style viewpoint. And then I use it throughout the course. Sadly, however, not every student appreciates; a number of them simply want grades over understanding.

user2103480

But to return to the core topic, I dont know how far the skills acquired in maths classes carry over to everyday life. I think they do carry over, but we all are heavily biased

user21820

@user2103480 But I would disagree with focusing on teaching the encoding of functions in set theory. It is an artifact of the choice of ZFC as the foundational system, and not inherent to mathematics. One can easily set up a foundational system equivalent to ZFC where functions are more naturally handled.

user2103480

11:09

@user21820 well, it's impossible for them to know how great the befenits are. We've probably all been lazy students at some point

@user21820 if you include the formalization of ordered pairs, I somewhat agree. I must say though that it was really helpful to me to know that "a function is a set of ordered pairs such that ..."

user21820

@user2103480 I think we see many examples in politics and abuse of statistics, and we will only see more and more as the ratio of junk to value on the internet increases.

@user2103480 Incidentally, there are kind of two levels of abstraction we can stop at if we aim to design a practical formal system as strong as ZFC. The first level is to keep the function type FN(S,T), namely functions from S to T, encoded as the set of a specific kind of subset of S×T, but leave ordered pairs as native objects that are not stipulated to be sets. I do this here.

I personally do like further abstraction, where even functions are not encoded, but there is one main problem if we want ZFC strength: We may need to add a few notational devices so that we can easily handle replacement elegantly and intuitively (which is why I didn't do it in that post). We can talk about this in further detail if you're interested.

user2103480

True. But my prime experience with statistics was exemplaric: We had to study it in a tough, measure theoretical stochastics course, and I had troubles understanding all the definitions. Naturally, I asked my peers, who mostly gave the insightful answer: "Isnt that easy? You just memorize the formula"

user21820

@user2103480 Lol! I didn't mean mathematical statistics; I meant what lay people call statistics. Like...

'So, uh, we did the green study again and got no link. It was probably a--' 'RESEARCH CONFLICTED ON GREEN JELLY BEAN/ACNE LINK; MORE STUDY RECOMMENDED!'

user2103480

I managed to figure the stuff out myself, nobody cared when I tried to explain, and the exam fucked most of them over :D so by now, my picture is that almost nobody understands statistics, not even mathematicians (those people werent stupid!)

@user21820 xkcd on point as always

user21820

@user2103480 You are right; everyone (mathematicians included, myself included) must sit down and very carefully analyze statistical studies or probability paradoxes to know what exactly is going on. Those who are lazy often end up confused or misled.

My biggest gripes with popular statistics is the cavalier way they treat confidence intervals, related to the misleading use of testing against the null hypothesis.

user2103480

11:22

@user21820 Do you maybe have any pdf of that? Although I shouldn't be wasting time with that tbh, I gotta study forcing and homotopy type theory lol

user21820

@user2103480 No, I don't, but there's no hurry we can discuss this any other time you like.

user2103480

@user21820 I think I already knew this post, but now that I glanced over it again, I think I am gonna print this post out as soon as I am TA again. Thank you! I was looking for a comparatively short introduction to proofs, but didnt find any good stuff online

user21820

@user2103480 Okay you're welcome, and please let me know if you spot any typos in that post!

user2103480

@user21820 then I'll take a rain check!

user21820

@user2103480 Sure next time then! =)

@user2103480: By the way, another important thing that I consider a part of logic (but many teachers fail to) is type-checking, which would eliminate most misconceptions and nonsense generated by students. See my post here for example. Unfortunately, many math teachers fail to see the problem as clearly as we do, because they themselves lack knowledge of a deductive system...

user21820

11:54

5

Q: Generalized graph-minor theorem?

Consider the following generalized graph-minor theorem: GM($κ,λ$): Given any collection $S$ of $κ$ simple undirected graphs each with less than $λ$ vertices, there are distinct graphs $G,H$ in $S$ such that $G$ embeds as a minor into $H$. Then the Robertson-Seymour theorem is GM($\aleph_0,\...

user2103480

13:41

@user21820 isnt type checking in these cases just "checking whether the expression is well-defined"?

user21820

@user2103480 Yup. I'm sure you know how many students don't even know how to do that...

user2103480

I find the new type theoretic perspective I'm starting to grasp pretty interesting. In a sense, type checking is also proof checking, right?

user21820

@user2103480 Yes only if the logic is constructive in some suitable sense. I prefer not to conflate type-checking (the programming-language notion) with type-judgement in type theories.

They are very similar, but many common type theories forbid subtyping or type-conversion, which is not good for intuitive mathematics.

user2103480

I've read countless times that the logic of type theories is (should be) intuitionistic. I haven't seen much of type theory so I'm wondering how one even "defines" the logic of a type theory. In the dependent, intensional type theory I've seen, the logic seems to be just the logic that you get when interpreting all the constructions via propositions-as-types

('Define' does not need to be completely formal)

user21820

Well, I think it's a serious mistake for many people to conflate "type theory" with "MLTT" or "CoC" or similar type theories, just because they are common examples. It's just like conflating "set theory" with ZFC.

11

A: What do logicians mean by "type"?

I am not looking for a formal definition of a type so much as the core idea behind it. I can find several formal definitions, but I've found they don't really help me to understand the underlying concept, partly because they are necessarily tied to the specifics of a particular type theory. If...

In the above post I give an informal overview to some basic notions that should be common to all foundational systems that can aspire to being called type theories.

And one thing great about all of them is that they treat functions natively, and not as encoded objects.

user2103480

13:54

That's why I specified it to dependent, intensional type theory

user21820

Indeed that's why it's a mistake for people to claim that they must be intuitionistic.

Transcript for

♦ $Mathematics$ Logic

Transcript for

♦ Logic

♦ $Mathematics$ Logic