@kit: Hello!

@user21820 Salve!

You can find me either here or here, as I set up these two rooms to cater for logic and more basic stuff.

@kit: It would also be good to know if you have programming experience.

Because it's much easier to explain in terms of programming if you do know a programming language.

Oh alright great. I personally like the logic side of math.

Yes I have some understanding. Mostly Python and Haskell.

Okay then it should actually be rather easy to explain to you the technical side of logic. It is difficult without programming background. But firstly, see if you get what I'm saying in my answer to your question, and we can discuss here if you like.

Great, I'll get back to you once I'm done.

Sure.

@kit: Please skip the article about the four-colour theorem for now. It was just an aside that may be of general interest.

alright

Still reading, and if it's important for you to understand my competence in programming here's a question I posted on stackoverflow <https://stackoverflow.com/questions/45849782/why-program-flow-control-executes-‌​randomly>

Sorry, I thought that would have made it a hyperlink..

@kit To make a hyperlink type something like [link text](link address).

@user21820 It'll take me several passes to understand it, but I'm getting an idea so far.

But it's okay you don't have to link it.

Ah thanks

@kit To speed up your idea getting, I can explain a bit about formal proofs here, since the answer I wrote just now didn't assume programming background.

Oh ok

Long time ago, mathematics was really very handwavy, and nobody had a clear idea what a mathematical proof should be like. The consequence was that there were a lot of incorrect proofs. Even great mathematicians like made very basic logical errors, because logic had not yet been formalized. But today, after programming languages were invented, there is a very easy definition of "formal system" that I can give you and you can immediately understand.

A practical formal system is simply a computer program that expects a pair (p,x) as input, where p and x are strings, and outputs "yes" if p is a valid proof of the sentence x, and "no" otherwise.

It may seem that I haven't defined "valid proof", but actually the point is that what is "valid proof" is completely determined by the formal system (the program) itself.

For example, here is a simple example formal system. Let K be the program that given the pair (p,x) simply ignores p and outputs "yes" if x = "1+1=2" and "no" otherwise.

Is this prolog? or what is it?

Any language that you like. In Python it would be:

oh

def K(p,x): return "yes" if x=="1+1=2" else "no";

I need double-equal, right?

p isn't used in that is it?

Yea so K is a silly and useless formal system.

But it gives you an idea that really a formal system can be any program that always outputs "yes" or "no" on an input pair of strings.

single or double quotes for strings

Both are the same in Python, I think.

Yes

One important question is, what kind of formal system do we think is useful for us to make predictions about the real world.

And for that purpose humans invented classical logic (in modern form called first-order logic).

I won't explain first-order logic today, but I can briefly describe to you an example formal system based on first-order logic.

cool

First look at just this section of the wikipedia article, titled Equivalent axiomatizations.

Do you know what the symbols mean?

The upside down A is "for all"?

The rest I know

Yes, and the other one is "exists".

ok

Now, why did we invent this particular set of sentences? It is because it seems to be true when interpreted in the real world to refer to natural numbers encoded in physical medium, such as binary strings or whatever you like.

Without interpretation, these remain just symbol strings without meaning.

But when we use our human minds to interpret these sentences to assert something about the real world (such as about binary strings), then for some inexplicable reason all these 15 axioms seem to hold!

You would also have to interpret "+" and "·" and "<" and "0" and "1". But I'm sure you know how to do that, in the sense that each of them can be interpreted as the result of running some program on the binary strings.

Does this make sense so far?

I believe so

So those are the axioms. I still haven't explained how we can use them, but first-order logic is precisely what we need in order to use them.

The first one is a formal definition of the property that addition is associative.

Yeap.

Most you would have learned in middle-school or something. Except for axiom 14, which nobody teaches but everyone assumes when they need it.

Okay so now to explain how we can use first-order logic to use those axioms.

ok

First-order logic is a notion that comprises both a language and a deductive system. The language you partly know already, including the intended meaning of the logical symbols ∀,∃,¬,∧,∨,⇒,=.

The language also includes the notion that we have predicate-symbols and function-symbols.

I forgot the meaning of the backwards 'E'.

exists.

right

For ∀ll. There ∃xists.

Gotcha, clever memory aid - haha

I always thought that it was the original reason for the symbols, but now I'm not so sure haha..

A function-symbol is a symbol that is used to denote a function. What is not stated in the linked axiomatization is that each of + and · is a function-symbol with 2 inputs of type N (natural numbers) and 1 output of type N.

"binary-operators" right?

Right! I was just going to say that we use the equivalent mathematical expression that +,· are binary operations on N.

I think that's what they call them in Haskell.

Haskell is very much mathematically designed.

cool alright

I love it

We also say that N is closed under + and ·.

I shouldn't say "equivalently" because you still need to specify "2 inputs" somewhere.

For some years I was getting no where with Python, and after learning Haskell, due to it's logic (that I later found to be based off lambda calculus) is what I was look for. And consequently I now have a hard time with imperative languages :(.

Oh, what's 'closed' mean?

Haha.. I have heard and read a lot about Haskell but have never actually used it before.

@kit It just means that when you apply + to N, the result is still in N. Same for ·.

It's terrific for recursive algorithms :).

ohhh ok

At this point I must tell you that there are many variants of first-order logic. What I am describing to you now is the most natural variant (corresponds closest to natural language), which if you need to check references next time, is called "many/multi-sorted first-order logic".

It was some time ago but I learned that in a cliff notes algebra book.

All are as powerful, in the sense that you can translate mechanically from any one variant to another.

But some are more intuitive than others.

Yes, yes, you're right. I'm just picky!

In particular, the axiomatization I linked has bounded quantifiers (the "∈N" is the bound.) So if you pick up a book on logic and find that the quantifiers are unbounded, that is one-sorted first-order logic.

Now about predicate-symbols.

Wait.. "find that the quantifiers are unbounded" what's another example of 'unbounded'?

"∀x ( x=x )" has an unbounded "∀" quantifier.

Meaning that the number could be anything?

or variable*

Well, literally an unbounded quantifier ranges over the whole world/universe.

Gotcha

That is why I prefer many-sorted logic, where we are more explicit with the typing of variables, just like in programming with strict typing.

So unbounded doesn't mean 'anything' but any number that it's a set of. Is that a better description?

No "∀x ( x=x )" literally means "every object x is equal to itself".

Oh sorry, I was still stuck on: unbounded

Whereas "∀x,y∈N ( x+y∈N )" means "Given any naturals x and y, their sum is a natural.".

The definition is closer to that it can be any number that it's part of a set of.

@kit There are no "sets" in pure logic. Just think of "∈" as a symbol and nothing more for now.

Ohh?

Yea.

Ok I'll try to keep that in mind.

Now to predicate-symbols.

PA has one of them.

"<" is a binary predicate-symbol on N. This means that when you apply it to 2 inputs from N, the output is a truth-value (boolean).

Sorry if we're going off your original topic, but what part of mathematics would sets be a part of?

@kit Set theory. Modern set theory is mostly about ZFC set theory, which is a system based on first-order logic.

ohhhh... ok. Thanks for that.

Haskell has cool ways of making set comprehensions.

But yeah, I get the binary predicate

In most modern mathematics, not much set theory is needed. In fact, many-sorted first-order logic plus arithmetic (PA) and a little bit more suffices for almost all mathematics that has been applied to the real world. I can explain this in more detail another time.

So the output is always a boolean value

Yup, and you already know what the boolean operations do, so I don't have to explain that.

Is this touching on ... Type Theory? Haskell has a type system, but I couldn't understand it outside of Haskell.

Sorry for the interjections, but it doesn't annoy you for me to interrupt you with questions like this?

Type theory (like "set theory") is another umbrella term for a variety of foundational systems. Historically, set theory won in terms of common acceptance in mathematics due to sociological and historical factors. But many modern mathematicians informally work in some unformalized foundation that has bits of both set theory and type theory.

At school I couldn't pay attention to teachers in a classroom setting, I was only able to be attentive if I can ask questions in the middle.

@kit No your questions are fine. If you don't ask now, later you may forget.

Great great, thanks ^^

Ok, and like set theory, type theory isn't a part of first-order logic?

Haskell's type system is not so much a type theory, because it's just used to make sure your variables have the correct types, and not to enable you to perform any logical deductions.

Yes first-order logic is underneath most foundational systems.

Ohhh ok. That's why then.

ok

Some type theories are not compatible with classical logic, but let's not go there yet.

So, back to what I said about first-order logic comprising both a language and a deductive system. I have described what the language is like for many-sorted first-order logic. Now for the deduction system.

Remember I said that a formal system in general is just a program that does such and such, which I call a proof verifier program.

But that's not practical enough. First-order logic is a simple kind of formal system, where there are deductive rules that tell you what you can deduce from what.

I'll give you one example proof from PA.

Oh, I took a logic coarse on Coursera so you know. Not that I fully understood the material though -haha.

Most of what you're saying is new to me and helps set forth definitions. I only have a very basic understanding uptil the induction method. My math skills wasn't good enough for the later part of the course.

Here I have used twice the same rule, called ∀-elimination. You may know it by other names. It's just the notion that if you have a true "∀" sentence you can apply it to anything that it, well, applies to, to get a new true sentence.

So it basically becomes a stored variable?

I'm not sure what you mean by that.

The rule is just relying on the meaning of "∀".

I substituted (x,y,z) with (1,1,1+1).

Oh sorry. Yes the substitution was what I was referring to, never mind it.

The crucial fact about first-order logic is that it has only a finite (and few) number of such deductive rules and yet is powerful enough to prove every sentence that is necessarily true given the axioms! This is the first non-trivial result of logic, first proven by Godel and later proven by Henkin using an improved proof.

I won't prove it now, but I think at this point you can roughly understand that it is a marvelous claim.

Yes I do

With binary alone look at what we can do with computing.

brb, afk

I need to go now too.

@kit: See you next time!

@user21820 Oh yes and thank you. I did have more questions about some definitions such as what does 'formal logic' mean and what it's relationship to first-order logic.

@kit Sure. We can have that discussion over in the Logic room, but perhaps not today as I have stuff to do. Briefly, "formal logic" is a very broad umbrella that covers practically all formalizations of 'logical reasoning', including different systems based on different logics. First-order logic is just the logic that has given us almost all practical results.

You can also just post any logic-related question there, and if I am not around, you can rely on LeakyNun or Allessandro for answers.

@user21820 Ohhh.. ok I think I understand. So some logic, such as inductive reasoning, is invalid, but part of formal logic?

Oh cool thanks ^^

Sorry I don't seem to be able to edit my post. What I ment was: Some logic, such as inductive reasoning, although it's not always accurate is under the umbrella of 'formal logic'?

No need to edit (there is a time limit for editing); you can just post again.

And let's continue in the logic room; I quoted you and will reply there.