Logic - 2016-08-23 (page 1 of 2)

user131753

13:25

@user21820: After your suggestion, I started to read some mathematical logic. But the very thing that strikes me is the concept of "finite string of symbols". How exactly do we define the concept of "finiteness" here?

user21820

14:06

@toto: Hey sorry I didn't see your message. Any question?

@user170039: We have no choice but to accept string manipulation in our meta-system.

toto

Hu, well actually yes, i read some stuff about formal proof and fitch style

And actually i had some difficulties to understand some laws of inference

especially the for all introduction

user21820

Ok sure just ask if you've questions. Let me address user170039's question for now.

Give me a few minutes.

toto

okay

user21820

@user170039: Basically the thing is that we cannot define everything. Ultimately we run into intrinsic circularity

one of which is that we need to understand strings of symbols.

NL: Let me use ML to denote natural language and MS to denote the meta-system. I'll distinguish when I'm talking in NL and when I'm talking in MS.

NL: To begin studying logic at all we need to set up MS. The most basic requirements is that MS axiomatizes strings (over some fixed alphabet) and their properties.

NL: Suppose we take ASCII as the alphabet, and we let MS have axioms like "forall strings x,y ( x+y is a string )". Here "+" is a binary operation that is valid for strings and is supposed to mean concatenation.

NL: We also let MS have axioms like "forall string x and k in N ( x[k] in A )", where "in A" denotes "is a symbol in the alphabet". Note that MS doesn't actually need set theory, but it's convenient to use similar notation.

user131753

You can use MathJax, I can read them in my computer.

user21820

14:14

NL: Hello! Alright, thought it would be harder for me to type and read haha.. Since every time MS uses "$A$" it would be in the form "$\in A$", we can systematically replace it by a predicate if we like.

user131753

I don't understand what you mean by "MS doesn't actually need set theory". Can you explain?

user21820

NL: Rewrite every occurrence of "x in A" as "Alph(x)".

NL: This means we can make do with "Alph" just being a predicate symbol in the language of MS.

NL: We will never need to use "Alph" as an object in MS.

user131753

The problem is, when you are talking about predicates as being formal symbols in the MS, you need to set up Meta-MS and the regression can continue ad infinitum.

user21820

NL: Same for the notion of "string" and "$\mathbb{N}$".. You can rewrite "$\forall x \in String\ ( \cdots )$" as "$\forall x\ ( String(x) \to \cdots )$". We will never use "$String$" as an object.

NL: Yes that is why I said it is an intrinsic circularity.. To set up MS, our NL I'm using now needs to already know about strings.

NL: The important difference is that NL contains all kinds of natural language nonsense. The MS we wish to set up will not.

NL: Or so we hope. By including as few specific axioms as we need, we hope to have a clean meta-system within which we can then study other formal systems.

NL: But at the core we cannot escape the circularity. See math.stackexchange.com/a/1334753/21820 where I describe what I believe are the only two circularities in mathematics.

user131753

But we need to be sure that "[t]he MS we wish to set up will not contain all kinds of natural language nonsense", don't we? We can't leave that to hope.

user131753

14:22

So, why bother about formalization at all?

user21820

@user170039: We can't hope to prove it. But we can hope to convince others that it is sound.

user131753

So, logic is based on belief?

user21820

That is the reason for Hilbert's original goal; if mathematics could be reduced to finitely describable rules, then both camps (basically finitistic and infinitistic) would agree.

Let's put it this way.. Classical logic was based on belief. We empirically observe that we can assign truth values to sentences about reality and then combine them via boolean operations and reason about them and obtain correct conclusions if we started with only correct sentences.

The only sticky issue raised recently is that LEM seems fishy. But actually it's not. Certainly it is not constructive, but it is surely true about the reality. Any sentence about reality is either true or false, even if we cannot figure out which.

user131753

Let's be clear about some things. Do you mean that since Hilbert didn't want logic to be based on belief and so he wanted mathematics to be reduced to finitely describable rules?

user21820

I mean that Hilbert didn't want logic to be based on too much belief. The finitistic camp were not happy with infinite objects. If they could be convinced that infinitary mathematics as done by the other camp was actually consistent, it helps to make them feel comfortable that perhaps it is not meaningless after all.

But to convince them, it would be no use to use infinitary arguments to do so!

That is what Godel proved impossible. The incompleteness theorems really show that no purely finitistic argument can prove the consistency of PA.

user131753

14:29

Now I get it.

user21820

So we can't hope to achieve Hilbert's goal, but at least we can try to minimize our required beliefs.

That we do by first setting up MS.

If everyone agrees on MS, then we can use MS from then on.

And everyone will have to agree with all the consequences that MS can prove.

Does it make sense?

user131753

Sure.

user21820

That is also why I take pains to say that MS does not need to be a set-theory.

Although most modern logicians take ZFC as their MS!

> the very thing that strikes me is the concept of "finite string of symbols". How exactly do we define the concept of "finiteness" here?

Back to your this question...

In what context did you read this, can I ask?

user131753

While reading predicate calculus from a book on mathematical logic.

user21820

Ah okay.. I was wondering because I used that phrase a lot in my answers on foundations haha..

So for the modern logician, it's easy because in ZF we can define "finite" quite simply.

For a weak MS, we don't even define it because we don't need to.

All we need is our axioms for strings to be just good enough.. for example..

MS: forall x in String ( len(x) in N ).

MS: [all the axioms for N as a discrete semi-ordered ring, plus induction]

NL: These axioms allow MS to be able to reason about strings and importantly prove results about strings using induction on the length. "len" is some function symbol.

NL: So don't be surprised if you see your logic textbook use the axiom of choice, because modern logic assumes ZFC. But note that Godel's incompleteness theorem is very constructive; he purposely ensured it was, so that everyone cannot deny that it is true.

@user170039: So is what I sketched enough or do you need more details?

user131753

14:43

But still, the formalisitic position of mathematics is problematic philosophically. Is there no way of founding mathematics using NL?

user21820

Mathematicians in the past have been using NL.. sure, but nobody can be confident it is sound. Remember Newton's infinitesimals whose square is zero?

And even Euler did some infinite series manipulations that were invalid.

user131753

But claiming that Euler's manipulations (say) were invalid required one to be rigorous. I don't think that is same as being formal.

user21820

Rigour is only possible through formalization.

user131753

Why so?

user21820

Otherwise one could ask you, how do you know your mathematics is rigourous and mine/Euler's is not?

The only way you can answer is by setting up some formal system which both of us agree with the inference rules.

And then you show that my reasoning leads to provably false sentences, while yours doesn't.

That is why only after the ε-δ definition of limits was introduced, were we able to say conclusively whether or not some handwavy argument is rigorously valid or not.

By the way, when I say "formal" I don't mean that we must write all mathematics in a precise formal language, but merely that it must be clear to others that it can be written in some formal system should one desire to.

Few mathematicians today do their work in formal systems, unlike software engineers.

user131753

14:54

I think I understand. But should I have any doubts in future, can I again talk about this?

user21820

Sure. I also want to say a bit more about NL.

user131753

Thanks.

user21820

On first thought it seems that there is nothing quite wrong with NL, as long as we try to stick to unambiguous phrasing.

Right? Most science is done in NL anyway, and we seem fine.

user131753

Sure.

user131753

More precisely, I think that most science use syllogisms implicitly in their "proof".

user21820

14:56

In fact, NL is quite fine, but one must be very careful because NL can talk about all kinds of weird sentences that are grammatical and unambiguous but not about reality.

3

A: Is Godel's modified liar an illogical statement?

Your question has two main facets. The first is that you did not grasp the way logic does not fall to the liar paradoxes. The second is that there are deeper reasons as to why we have such apparently innocuous sentences in natural language that seem to defy assimilation into formal logic systems....

See in particular Quine's paradox in the later part of my post.

user131753

By the way, what exactly are "unambiguous sentences"?

user21820

Heheh good question. That's one of the pitfalls of using NL.

In my post sentences about reality can be considered to be unambiguous, but Quine's sentence is an unambiguous sentence that is not about reality.

We could define "unambiguous" recursively. Suppose "X" and "Y" are unambiguous noun phrases. Then we stipulate that "X is Y" is an unambiguous sentence. And so on.

If we stipulate enough axioms about unambiguity, we should be able to establish that Quine's sentence is unambiguous (as any native speaker will agree with).

user131753

But you need to ascertain that there indeed exists $x$ and $y$ which are "unambiguous".

user21820

Yes that's why I said it's recursive.. If you don't have any axioms to 'bottom out', you get nothing provably unambiguous at all.

I could say "1" and "sentence" and "phrase" are unambiguous noun phrases, for example.

user131753

Sure. But then we defining things arbitrarily (much in the similar way we define finite strings).

user21820

15:05

Yes, this is the big problem with NL.

user131753

Still, the mathematics we do is not strictly formal. So, I was wondering whether it is at all possible to base the foundation of mathematics on informal logic.

user21820

There is nothing that needs to be done if that is what you want, since it is already in informal logic.

user131753

I don't understand. What do you mean?

user21820

What makes mathematics useful is that almost all of it can be formalized, so we can be certain that anyone who accepts the formal system (usually ZFC) has to accept all mathematical theorems that have been proven so far (and written in semi-informal papers).

If mathematics was simply based on informal logic alone, then we have no such guarantee whatsoever.

Don't forget Russell's paradox. Naive set theory is what a lot of mathematicians use, and how do you know they don't manage to prove some theorem because they got a contradiction somewhere in the way Russell did?

user131753

Maybe because they informally use Naive set theory but formally (we believe) they use $\sf{ZFC}$.

user131753

15:11

Or some such axiomatic set theoretic system.

user21820

Yes those that know ZFC or some other formal system will work informally but always check mentally that it can be translated.

But some don't, and I've observed some professors go and ask others who know ZFC in detail about usage of things like the axiom of choice.

Anyway if you've finished reading about Quine's sentence (or the rest of the post), feel free to tell me what you think about it. I've read most other explanations (usually by philosophers) and as a logician I personally feel mine is the most correct. It turns out Kripke's notion of "grounded" is similar to my "about reality", in case you want to read about it.

user131753

I will try. But I think it will take time. For now I have to go. Thanks again.

user21820

As for informal mathematics, you may be interested in books.google.co.uk/books?id=ZIHs6Kar0vIC&pg=PA9.

@user170039: Sure, see you around next time. Just ping me!

@toto: So what are your questions?

toto

Well, that was something trivial i think, but i'm not sure to grasp it

it's about the universal introduction rule

user21820

Just ask then.

What about it?

toto

15:17

do you see what i'm talking about

well, i don't exactly understand what it means

user21820

Ah.

toto

they say

n in N, P(n) => for all n in N, P(n)

and, i'm not sure to get it exactly

user21820

Which text is this again?

toto

from my logic book

they do not used =>

but the "demonstrate" symbol

user21820

|-?

toto

15:19

yes

user21820

well okay so it's not too different from my Fitch-style system?

toto

well, it's the same i think

user21820

Good. Then it's easy to explain

toto

okay

user21820

Firstly recall the -> rules.

toto

15:20

well, to deduce a->b

user21820

The introduction rule allows you to get from ( A |- B ) to ( A -> B )

toto

we must suppose a and then prove b

then it gives use a->b

user21820

Yes and that's how the rule captures the meaning of implication.

toto

yes

user21820

We need the other rule of course to make the capture correct.

The other rule is Modus Ponens.

from A , ( A -> B ) we can get B.

toto

15:22

a->b and a |- b

yes

user21820

Yea this makes "A -> B" behave as if it is no different in meaning from "A |- B". The same goes with the "forall".

toto

what do you mean by the same goes with the forall ?

user21820

The introduction and elimination rules make "forall x in S ( P(x) )" behave the same as:
|Given x in S
|---------------
|P(x).

The former is a single sentence with a truth value.

The latter says that in the subcontext where you have an object x in S, you can derive P(x).

Stated this way, they obviously mean two different things. But the rules make them essentially interchangeable, in the sense that if you have one then you have the other.

toto

i don't understand

user21820

Let's look at the implication again. Whenever you have:
|A
|--
|B
you can derive:
A -> B
and vice versa.

toto

15:27

yes

from A->B we can say A|-B, true

user21820

The former says something about what you can derive, namely in the subcontext where A is true then you can derive B.

The latter is a single sentence with a truth value.

It is precisely the introduction and elimination rules that make both interchangeable.

The former gives the latter via -> introduction.

The latter gives the former via -> elimination.

toto

yes

user21820

Similarly
|Given x in S
|---------------
|P(x).
gives
forall x in S ( P(x) ).
via forall introduction.

And the reverse is via forall elimination.

toto

aaahhh

i see

yes but

user21820

Perhaps you want to ask, why have such rules?

toto

15:31

why can we say that forall x in S(P(x)) is obviously true

yes, i mean, why do it works

well actually wait a sec, i'll tell you precisely what i don't get

user21820

Oh well the rule is clearly sound. You just must read the meaning of the rule correctly.

|Given x in S
|---------------
|P(x).
means that under the context where x in S, you can derive P(x).

Note that in my specification of the rule at:
http://math.stackexchange.com/a/1684204/21820

toto

cause, in my book they says

user21820

Here x must be an unused variable.

toto

give x in S, P(x) where x is an unbound variable in P(x)

gives

forall x in P(x)

user21820

Hmm yes, but that's not the starting point.

See my ∀sub rule. One can only construct a ∀ subcontext using an unused variable.

toto

15:36

okay

user21820

So that makes it such that if you manage to prove P(x) in that subcontext, it really applies to any possible given x in S.

Since there is nothing that controls what the x could be except that you know it is in S.

So if you manage to prove P(x), it is because your argument only relies on x in S.

toto

i see okay

it works, thanks :)

oh by the way

user21820

Great!

amWhy

@user21820: Do I know you from a different user name (i.e. Have you changed your username anywhere between 1.5 years ago and now?

toto

have you some excercices ?

user21820

15:37

@amWhy: Nope my username has been the same since I joined Math SE. But who do you think I am?

@toto: Yes I have, I'll just paste them here.

toto

cool, cause i need some practice

amWhy

Just curious, because I've been around here for a long time (away from March '15- May '16)...have done a lot in logic here, but don't immediately recognize your username. But I'm very glad you started a chat for logic!

Hello @toto...I'm not trying to interrupt!

user21820

@amWhy: Ah I see; well I've been answering logic questions in the past few months or so, very rarely earlier.

Problem 1. Given any assertions A,B, prove the following:
(A ⇒ B)∧¬B ⇒ ¬A.
Problem 2. Given any assertions A,B,C,D, prove the following:
(A∨B)∧(A ⇒ C)∧(B ⇒ D) ⇒ (C∨D).
Problem 3. Given any assertions A,B, prove the following, which are commonly known as De Morgan’s rules:
¬(A∨B) ⇔ ¬A∧¬B.
¬(A∧B) ⇔ ¬A∨¬B.
Problem 4. Given any assertions A,B, prove the following, which is commonly known as absorption:
A∧B∨¬B ⇔ A∨¬B.

These are for propositional logic.

toto

@amWhy, no prob don't worry ^^

okay

hu seems hard for me xD

for the first one

i'll try to suppose (A ⇒ B)∧¬B

and then get not(A)

(i just want some help for the first, for the others i'll do it by myself on my spare time)

so

user21820

First we break down as much as possible.
If ( A -> B ) and not B:
| A -> B.
| not B.
| ...
| not A.

No direct route seems possible, so we try negation introduction.
If ( A -> B ) and not B:
| A -> B.
| not B.
| If A:
| | ...
| | Contradiction.
| not A.

Can you fill in the blank?

toto

15:47

ah, we can freely suppose A -> B and not B ?

yes sure i can

from If A: it gives us B (modus ponens)

but, we suppose not(B)

user21820

It's not exactly freely suppose. It comes from the first context (assumption) and conjunction elimination.

toto

but we find out that not(B)

so contradiction

user21820

Yes that is right.

You should learn to write in the formal format

toto

"It's not exactly freely suppose. "

that's what i don't understand

when i can suppose something or not

user21820

That's why you should learn to follow the rules strictly. Does your book also use Fitch style?

toto

15:50

no, they use trees

but, i read fitch style

user21820

Never mind you're a programmer so try doing it the way I did. In more detail it goes like this:

toto

that's the same rules

user21820

( A -> B ) and not B -> not A. [-> intro]

See carefully, at every point we are using an inference rule on sentences we know to be true in the current context.

toto

you're ri

right*

but

why and-elim do not create a subcontext ?

user21820

because if you have a sentence "A and B" that is true in the current context, by definition of "and" it means that both "A" and "B" are true in the current context.

toto

15:55

okay, i though each rule create a context

user21820

Same for [-> elim], also called modus ponens.

toto

a context is only created when you suppose something ?

user21820

Technically there are no inference rules that create contexts. Yes you can at any time create a new subcontext and specify some restriction on it.

In my system there are only two possible subcontexts.

One is the conditional subcontext (when you suppose something)

and the other is the universal subcontext ("Given x in S")

toto

okay but one thing which is hard to understand for me

when you conclude something

from a subcontext

why do the conclusion apply to the upper subcontext ?

user21820

Not in all cases, clearly.

toto

15:58

for example, you mark a contradiction

and so you conclude that not A is the in the upper context

why ?

user21820

There are only two ways you can get out of a conditional context. You already accept the [-> intro] rule right? That is one.

This [neg-intro] rule is another, and is precisely the reasoning behind proof by contradiction.

Transcript for

♦ $Mathematics$ Logic

Transcript for

♦ Logic

♦ $Mathematics$ Logic