Logic - 2017-12-13

user21820

03:47

@LeakyNun You are missing something. Please read the context of my statement carefully. That statement was ambiguous, so let me state it clearly:

> It is not true in general that ( if one premise is false then you have a valid argument ).

This was in response to @LastIronStar stating the following (which is wrong):

23 hours ago, by LastIronStar

I think if even one of your premise is false then argument is automatically VALID

@LastIronStar: That is why I purposely wanted you to stop thinking in terms of premises and conclusions, until you actually get the point of logic.

Have you understood the last example I gave of a valid Fitch-style proof?

14 hours ago, by user21820

If ( not B ) and ( A implies B ):
  [In this context either "A" is true or "not A" is true.]
  If A:
    A.
    A implies B.
    B.
    not B.
    Contradiction!
    [In this context we deduced that "B" and "not B" are both true, which is impossible.]
  not A.
  [Since the subcontext where "A" is true is impossible, "not A" must be true.]

And the accompanying explanation.

LastIronStar

Hi @user21820

user21820

@LastIronStar: Hello!

LastIronStar

04:02

now to get to work on that proof you've given!

i am having hard time following this proof

notational issues i guess

as in i don't know it

user21820

Just go line by line and specify which line you don't get.

LastIronStar

what does it mean to have an inner loop with multiple statements?

user21820

It just means that all of them are individual assertions within that inner context.

Each one of them is made within that context.

If you know programming, it's exactly the same.

Do you know programming?

LastIronStar

yes i do

for example, what's throwing me off is B is followed by not B

user21820

Then there's a much easier way to view the proof. Let me rewrite in program-style.

You prefer Python or C/Java style?

LastIronStar

04:10

C

user21820

Okay perfect.

You know assert, right?

LastIronStar

it's like a IF+break

it checks if input of assert is true if not, it breaks the function and exits

user21820

More or less yes. assert P; will throw an error if P is false at that point that the assertion is executed.

Give me a minute.

LastIronStar

sure

user21820

bool imp(bool p,bool q) { return (p?q:true); }
bool a,b;
if( !b && imp(a,b) )
{
	if( a )
	{
		assert a;
		assert imp(a,b);
		assert b;
		assert !b;
		assert false;
	}
	assert !a;
}

The first line is just to define implication.

Remember I said in my definition a valid proof is one where every single statement is true in its context?

In the program version, a valid proof is one where every single assertion passes (no assertion error).

LastIronStar

04:20

yeah imp function is basically =>

user21820

Check that the above program indeed is a valid proof.

LastIronStar

what are we proving again?

i see just need to check that all assertions are true

user21820

Yes, are they? Is there any assertion that fails?

LastIronStar

reading give me a sec

why do you need an assert 'a' inside the loop of If( a )?

user21820

It is a direct translation of the non-program-style proof!

15 hours ago, by user21820

If ( not B ) and ( A implies B ):
  [In this context either "A" is true or "not A" is true.]
  If A:
    A.
    A implies B.
    B.
    not B.
    Contradiction!
    [In this context we deduced that "B" and "not B" are both true, which is impossible.]
  not A.
  [Since the subcontext where "A" is true is impossible, "not A" must be true.]

LastIronStar

04:23

ok then i should have asked then itself

but the question remains doesn't it?

user21820

What question?

LastIronStar

1 min ago, by LastIronStar

why do you need an assert 'a' inside the loop of If( a )?

or even assert imp(a,b) for that matter

user21820

I don't need anything. The point is whether you agree the program-style proof is valid (no assertion error).

LastIronStar

it has an error

user21820

Where?

LastIronStar

04:24

in the context of !b, assert b will break the proof's validity

user21820

Well you are wrong.

Think carefully.

LastIronStar

i hoped so

user21820

If you don't believe me, you could simply run the program!

And observe for yourself that no matter what truth-values you give to a,b, the program will pass!

LastIronStar

ok so assert allows execution of post-code if it is true assertion right?

user21820

Yes.

LastIronStar

04:28

so assert(a) & assert of (imp(a,b)) will not throw

user21820

Right.

Why?

LastIronStar

but when it reaches assert(b), it should throw!

@user21820 context

user21820

No back up.

Right.

Look at the definition of imp.

By that definition if you manage to successfully assert a and assert imp(a,b), you must succeed in asserting b.

Agree?

LastIronStar

ok i'm pukka confused

so let

user21820

Do you agree with that one deduction?

That in any place where you can assert a and imp(a,b) you can assert b safely.

LastIronStar

04:31

yes i agree

user21820

Then now notice that in that place we assert both b and !b.

That should normally throw an error.

Right?

That's what's confusing you right?

LastIronStar

what is confusing me is that shouldn't the program always throw at assert(imp(a,b)) when its context is a(is true) & !b(is true)

user21820

What you're clearly missing is that an assert statement is only executed if you reach that statement to begin with.

You have reasoned correctly that the first two asserts must pass (if reached), and agreed that the third must hence also pass (if reached).

The fourth (namely assert !b) must pass (if reached) since it's also guaranteed from the context (if-condition).

So the only way that is all possible is... Can you see it?

LastIronStar

so this is a contradiction which means the context is not true

but that is only if we assume that assert(imp(a,b)) pass in the given context

user21820

Because the whole thing is within the outermost context.

So once it enters the outermost if-structure we know that imp(a,b) must be true.

@LastIronStar And right! The reasoning shows that the innermost context cannot hold.

That is why the last assertion (assert !a) is valid.

Got it?

LastIronStar

04:44

one sec

afk

i have TA duties, i will ping once i see it

ok?

user21820

Okay! See you later!

user21820

05:05

For reference, you can run the following complete program:

#define assert(p) { if(!p) { printf("Line %d: False assertion!\n",__LINE__); return 0; } }
#define trace { printf("Line %d: Reached\n",__LINE__); }
#include<stdio.h>
bool imp(bool p,bool q) { return (p?q:true); }
void input(bool &p) { int t; scanf("%d",&t); p=t; }
int main()
{
	bool a,b;
	input(a); input(b);
	trace;
	if( !b && imp(a,b) )
	{
		trace;
		if( a )
		{
			trace;
			assert(a);
			assert(imp(a,b));
			assert(b);
			assert(!b);
			assert(false);
		}
		assert(!a);
	}
	assert(!a); // Invalid, unlike the above assertions. Find an input that fails it!

On TutorialsPoint's Compile CPP online.

If you use a compiler that supports assert, then you can remove the first #define preprocessor-statement.

On that online compiler, you have to enter the input data into the Stdin tab before pressing Execute.

LastIronStar

07:52

Hi @user21820 there?

Leaky Nun

08:23

@LastIronStar hi

LastIronStar

@LeakyNun Hello

Leaky Nun

0

Q: On the way to prove ((p=>q)=>p)=>p.

I found this post and it raises a question: Use Fitch system to proof ((p ⇒ q) ⇒ p) ⇒ p without any premise. ONLY FOR FITCH SYSTEM. In the answer, the line 2 and 3 make two opposite assumptions. I have to say this seems kind of unnatural to me (to assume something and the contrary at the same ti...

@LastIronStar another person confused about assumptions, just like you

maybe you can help him out

LastIronStar

@LeakyNun well, i don't believe that your assumption is a good default either

Leaky Nun

@LastIronStar sorry :c

LastIronStar

@LeakyNun yes checking it out

Leaky Nun

08:28

@LastIronStar I ask you because I don't know how to start explaining

LastIronStar

@LeakyNun TBH, i'm still not convinced by 820's explanation completely. I will answer it maybe by tomorrow based on my understanding :)

user21820

09:58

@LastIronStar Well there are 3 steps you can do to convince yourself. (1) Run the program I wrote and test all possible inputs and check that it has no assertion error in all cases. This establishes that the proof is valid according to my definition, because every sentence is true in its context. (2) Delete all the assert statements in the program, and add them one at a time in order. Convince yourself that each one can be safely added without possibility of assertion error. If you get stuck reread:

5 hours ago, by user21820

What you're clearly missing is that an assert statement is only executed if you reach that statement to begin with.

Which I think you're no longer clearly missing, but you're not yet fully accepting of its consequences. =)

(3) The above reasoning is exactly the same as the reasoning behind the deductions in the English proof. Namely, the real meaning of the English proof can be taken to be given by the program!

(3+) Notice that the best reasoning ought to explain why the program will have no assertion error, without having to test all possible inputs. That reasoning will likewise explain why the English proof deduces only true sentences in their context without regard to the actual truth values of the propositions involved.

I have to go now, but if you don't fully grasp the above explanation then please pinpoint exactly where you're stuck.

LastIronStar

12:46

@user21820 I get the output false assertion for couple of cases

Leaky Nun

@LastIronStar code?

user21820

@LastIronStar Did you actually read the output message to see what was false?

And read the comment in the code on that very line.

LastIronStar

@user21820 oh lol

such a troll

@LeakyNun yeah

user21820

Sorry I really didn't intend to fool you.

I wanted to emphasize the point that an assertion may hold inside a subcontext but not necessarily outside it.

So you've to comment/delete that line to get the one for the original proof.

LastIronStar

np

Leaky Nun

12:48

@user21820 looks like your CS degree is finally useful here :P

user21820

@LeakyNun My words are failing me. I've been using computability so many times and you tell me "finally useful here"? =P

Leaky Nun

well

those are all theoretical :P

LastIronStar

MAYOR OF LONDON ALERT

Faraday is now triggered :P

user21820

@LeakyNun Very funny man. Those explicit independent sentences are now just theoretical, are they?

Leaky Nun

@user21820 ah come on

i don't know what I'm talking about

just pretend I said nothing

user21820

12:52

Lol.

LastIronStar

relax you two, just focus on teaching me this stuff :P

user21820

@LeakyNun We're both kidding, right?

Leaky Nun

sure

user21820

@LeakyNun: By the way, here's something I just posted related to what we previously discussed.

1

A: Can there be two different math?

Yes. Let $S$ be our chosen foundational system. Even if we somehow know that $S$ is $Σ_1$-sound, we still cannot rule out the possibility that $S$ is $Σ_2$-unsound! Here truth and arithmetical soundness are of course defined with respect to the natural numbers in the meta-system. First conside...

@LastIronStar: Please ignore this. Seriously too high-level. Sometimes I think LeakyNun ignores it as well.

LastIronStar

@user21820 you don't have to tell me twice, it is totally OHT right now

you are talking about your answer right?

user21820

12:56

@LastIronStar Just in case you thought it was relevant to what I was teaching you. That would be a big confusion.

When you've learned enough logic, I will be glad to explain to you. =)

LastIronStar

@user21820 that's the plan

Leaky Nun

@user21820 I think our "intended" logical system is S1-sound right

user21820

@LeakyNun We hope, of course.

If not it would be philosophically meaningless.

Secret

Just learnt this today from some AI guy in the symposium: https://en.wikipedia.org/wiki/Non-monotonic_logic

will deal with it after forallx

LastIronStar

@user21820 Can you tell me how all of this connects back?

user21820

12:58

@LastIronStar Are you satisfied with the explanation I gave of the program's valid assertions?

3 hours ago, by user21820

@LastIronStar Well there are 3 steps you can do to convince yourself. (1) Run the program I wrote and test all possible inputs and check that it has no assertion error in all cases. This establishes that the proof is valid according to my definition, because every sentence is true in its context. (2) Delete all the assert statements in the program, and add them one at a time in order. Convince yourself that each one can be safely added without possibility of assertion error. If you get stuck reread:

3 hours ago, by user21820

(3) The above reasoning is exactly the same as the reasoning behind the deductions in the English proof. Namely, the real meaning of the English proof can be taken to be given by the program!

Leaky Nun

@user21820 is it also S2-sound?

user21820

3 hours ago, by user21820

(3+) Notice that the best reasoning ought to explain why the program will have no assertion error, without having to test all possible inputs. That reasoning will likewise explain why the English proof deduces only true sentences in their context without regard to the actual truth values of the propositions involved.

@LeakyNun We also hope so. After all, we hope it is fully arithmetically sound.

Otherwise there is some arithmetic sentence that it proves that is not true for the natural numbers!

That would not be great.

Leaky Nun

@user21820 is our system useless?

user21820

@LeakyNun Which system? I'm confident that PA is sound, and ACA is sound, but I'm not confident that ZFC is sound.

Leaky Nun

@user21820 no, our "intended" system

the system that exists in our minds

LastIronStar

13:01

@user21820 I agree the program is correct and that it is a VALID argument. but i'm not able to put my finger on why this is so. right now i'm still searching for the intuition

Leaky Nun

the "one true arithmetic"

user21820

@LastIronStar Okay take your time to mull over it, and let me know if you want more explanation on any point.

LastIronStar

@Secret hi

@user21820 yeah

user21820

@LeakyNun I'm not sure what you mean by that. A set theorist has ZFC in his/her mind most of the time. I have predicative higher-order arithmetic in mine lots of the time. What about you?

Leaky Nun

@user21820 I mean the one in Euclid's mind

user21820

13:03

Hmmm...

LastIronStar

@user21820 just so we are on the same page all of this is about answering this question: Can a valid argument be made invalid by the addition of a new premise?

user21820

@LastIronStar All of this is supposed to give you a full grasp of basic logic (at least propositional logic) in one go, and as a happy by-product answer your that question.

Secret

[forallx page 6]

user21820

@Secret: Since you are here, you should also follow along and make sure you understand everything I'm saying.

Secret

I just joined thus I have not read what you are lastironstar is up to yet

so uh, whee does that conversation start?

user21820

13:08

@Secret: I'll quote the main points that you need to know:

I gave this example Fitch-style proof:

yesterday, by user21820

If ( not B ) and ( A implies B ):
  If A:
    A.
    A implies B.
    B.
    not B.
    Contradiction!
  not A.

With this inline explanation:

24 hours ago, by user21820

If ( not B ) and ( A implies B ):
  [In this context either "A" is true or "not A" is true.]
  If A:
    A.
    A implies B.
    B.
    not B.
    Contradiction!
    [In this context we deduced that "B" and "not B" are both true, which is impossible.]
  not A.
  [Since the subcontext where "A" is true is impossible, "not A" must be true.]

And this corresponding program:

9 hours ago, by user21820

bool imp(bool p,bool q) { return (p?q:true); }
bool a,b;
if( !b && imp(a,b) )
{
	if( a )
	{
		assert a;
		assert imp(a,b);
		assert b;
		assert !b;
		assert false;
	}
	assert !a;
}

You can play with it yourself or run my full working code given here.

LastIronStar

yesterday, by user21820

The essence of logic is that I shall ensure that this remains true throughout every proof.

this is kind of still zen to me

user21820

The "this" refers to:

yesterday, by user21820

I will call a proof valid as long as it satisfies my rule, namely that every sentence in it is true in its context.

9 hours ago, by user21820

In the program version, a valid proof is one where every single assertion passes (no assertion error).

Secret

what operator is "?"?

user21820

(p?x:y) returns x if p is true but returns y if p is false.

It's a C/C++/Java/Javascript syntax.

Based on this, check that what I said in the three comments starting here are correct.

@Secret: That's all you need to read. Please ask if you have questions.

Secret

13:23

---> Uh, we need the boolean values of a,b to compute a => b in the if (a ) statement, where is the boolean of b specified there?

user21820

@Secret Run my full working program if you are not sure how to use the fragment.

Euclid had ratios and geometrical figures in mind. He did have a notion of natural numbers, but I don't think he had even the notion of induction in mind. This had to wait for Peano, who did not have a proper system in mind either. Notice that Peano's Arithmetic had a second-order induction axiom, but he did not specify any set-existence axioms/schemas, so that induction axiom is useless.

Either way, for us to talk about whether a system is arithmetically sound, we must first have a computable translation mapping from arithmetical sentences to sentences in the system. Then we can say that …

Secret

14:14

(Ok, I really cannot do that had I don't a) run the program and b), work through the truth tables line by line). But anyway, I found:
Let xy be truth values of the pair ab
1. TT and TF will terminate the program with a false assertion
2. Only FF made it into the first if statement, All other xy skip the first if and head straight to the 2nd assert(!a) because (!b and a=>b) will give false

Since of the 4 possible truth value permutations of ab, 2 of them will give a false asseertion, it follows that the logical statement coded by this program is invalid

Leaky Nun

14:46

@user21820 I know the system wasn't well-defined

I was talking about precisely that vague system

user21820

@Secret You too didn't read the output.

It tells you which line is false. And that line tells you why it is invalid.

@LeakyNun Well then we can't say much except that it is vague? I'm not really getting your point. Of course every logician or mathematician thinks that his idea of reality is arithmetically sound with respect to his notion of real-world naturals.

The thing is that it is meaningless to talk about a model being arithmetically sound, so "idea" here must refer to some kind of conceptualization.

Leaky Nun

@user21820 I think it still boggles a mind that there is always some sentence about natural numbers that nobody can prove or disprove

user21820

@LeakyNun By the way, "precisely that vague system" is an oxymoron. =P

Leaky Nun

@user21820 :P

user21820

@LeakyNun There are two ways out. (1) Reality is uncomputable. (2) PA is unreal.

Leaky Nun

15:00

@user21820 but every axiom of PA is real...

user21820

9

A: What are the arguments for and against "one true arithmetic"?

In short: The so-called definition of natural numbers as those that can be obtained from 0 by adding 1 repeatedly is circular, but there is no viable alternative, which already makes it impossible to uniquely pin down natural numbers mathematically. Worse still, there does not seem to be ontologi...

See the section I wrote concerning the question of whether PA has a physical model.

Leaky Nun

btw do you have any proof for second-order incompleteness?

@user21820 (3) our logical system is flawed, just like how second-order "destroys" the semantic-completeness theorem

user21820

@LeakyNun That can be considered subsumed under (2) in the sense that PA refers not just to the axioms but to the entire system including the classical logic base.

Leaky Nun

ok

user21820

@LeakyNun The incompleteness theorem shown in my post does not care whether your system is first-order or second-order or alien-kind. It applies as long as there is a proof verifier. So whether you have something that looks like second-order or not, it succumbs.

Leaky Nun

15:06

and which step of completeness fails for second order?

user21820

I don't understand that question.

Just run the proof on whatever system you have and you get an explicit independent sentence.

@LeakyNun If you're talking about semantic-incompleteness, we discussed this before and I gave second-order PA as one of many examples.

Leaky Nun

@user21820 yes, but I'm not asking for examples

I'm asking which step in the proof of semantic-completeness fails for second-order

user21820

At first you asked for a proof, so you agree a proven example would suffice? Now you're asking for the place it fails in the proof. Well you got to pick your proof. In the Henkin construction it's trivial it only constructs objects, not sets. How can it ever produce a second-order model?

Leaky Nun

I see

user21820

Note that second-order logic with Henkin-semantics is semantically complete.

@LeneCoenen: Hello! All inquiries about (mathematical) logic are welcome!

user21820

15:30

@LeakyNun: See the following as well about Henkin semantics:

4

A: Is there a deductive system for second-order logic that is complete with respect to Henkin semantics?

It is very easy to name such a deductive system, although it depends on exactly what you call "Henkin semantics". Recall that a prototypical completeness theorem states that a formula is derivable in a deduction system $\mathcal{D}$ if and only if the formula is true in each of a class of structu...

Basically, whatever it is you want, as long as you can interpret it in first-order logic somehow, you can use your favourite deductive system for first-order logic and have completeness with respect to the first-order interpretation.

Transcript for

♦ $Mathematics$ Logic

Transcript for

♦ Logic

♦ $Mathematics$ Logic