ghosttown much?

21820 is a regular here and proficient at logic

he is not on atm, but this room is very active in general for logic problems

well, thanks

I'll pose my question

copy-pasting from the Mathematics room:

first of all, here are the 8 rules: pastebin.com/fpkgaVR0

and these are some additional rules: pastebin.com/Pua3gBNX

// easiest one was probably
¬E1
¬¬A ⊦ A
1. ¬¬A      by data
2. ¬A → ¬¬A
  1. ¬A     assume
  2. ¬¬A    by 1
3. ¬A → ¬A
  1. ¬A     assume
  2. ¬A     by 3.1
4. A        by ¬E 2,3

// so I tried to do
¬E2
¬A → B, A → B ⊦ B
1. ¬A → B   by data
2. A → B    by data
3. (A ∧ ¬A) → B
  1. A ∧ ¬A assume
  2. A      by ∧E 3.1
  3. B      by →E 2
4. (A ∧ ¬A) → ¬B
  1. A ∧ ¬A assume
  2. A      by ∧E 4.1
  3. ¬A     by ∧E 4.1
  4. B → A
    1. B    assume
    2. A    by 4.2
  5. B → ¬A
    1. B    assume
    2. ¬A   by 4.3
  6. ¬B     by ¬I 4,5
5. ¬(A ∧ ¬A) by ¬I 3,4

to finish it, I need to prove the de-morgan rules

and I'm fairly stuck at that point

I obviously googled it to get some hints, but there seem to be differing standards for which are the base rules, and what you can do within natural deduction

so I'm not sure I'll find what I'm looking for by googling

this would end with

6. A ∨ ¬A   by magic 5
7. B        by ∨E 1,2,6

but what is magic

I have a feeling I don't even need de morgan in this scenario, as all I need to prove is that A ∨ ¬A, which is a tautology

but it could be solved with de morgan

I'm also not looking for full solutions, just hints

@towc These 8 rules are insufficient. You cannot prove ( A and B implies B ) using those rules.

See here for one standard minimal set of rules for propositional logic:

you mean (A ∧ B) → B ⊦ B?

No? What I wrote is a tautology. Your lecturer's system cannot prove it.

I'm still not sure what you wrote

A ∧ B ⊦ B?

( (A∧B)→B ) is a tautology, and your lecturer's system cannot prove it, so it is inadequate for propositional logic.

how would you prove it with your system?

I'm not even sure how you'd formalize what you said

maybe ⊦ (A ∧ B) → B?

If A and B:
  A and B.
  B.
A and B implies B.

1. (A ∧ B) → B
  1. A ∧ B    assume
  2. B        by ∧E 1.1

that's what it would look like in the format he showed us

oh, right, the "subcomputational boxes" (as he calls them) are not included in those inference rules

@towc That's invalid. Look at the rules you gave me. It does not permit line 1.2.

conjuction elimination is at line 6 of the pastebin

there are 2 bins: first one contains the base rules, and second has the derived rules

base rules: pastebin.com/fpkgaVR0

@towc I told you already just now that those rules are insufficient.

conjunction elimination is in those rules

@towc In particular, conjunction elimination given there is incorrect.

well, he gave us two versions, I only noted down one of them

the other derives B instead of A

I didn't think it would matter, but I guess it does

@towc Yes it does.

The tautology I stated above cannot be proven with the rules you noted down, because the one you omitted is needed to prove that.

ok, hold on, let me see what else I omitted, and I'll make another paste

I think that's the only one

there are more omissions in the derived rules

"∨I" also is incorrect.

should also have B v A?

Yes.

It's not redundant.

while it would be for vE, right?

@towc That one is symmetric so one will do.

alright, with these rules in place, how do I show something like ¬E2?

(¬A → B, A → B ⊦ B)

here are the revised base rules: pastebin.com/MEEecCPE

Anyway after adding the missing rules you have a system that is close enough to the one in my post. Every rule you listed is one of the rules in my post. I do need to say that your lecturer's system is pedagogically not good because he is using "⊢" in two different ways, which I'm sure almost all students don't realize or don't understand.

again, these are just my notes. There's a good just I'm misunderstanding something

If that symbol is used both in describing the rules and inside a proof, then it's technically wrong.

In any case, I'll stick to my system so that there is no confusion. You can translate to yours easily.

here's what his format actually looks like:

Hi, Can I ask something here if it is not private chat ?

@towc Aha so his is better. Good we're getting somewhere.

@AjwadTaqvi It's not a private chat, and you can ask. But I'll answer towc's inquiry first.

I'm not sure which symbols to use to keep those in a single line

thanks @user21820

the ⊦ seemed like a good match. Any other suggestions?

@towc Unfortunately, some people use the same symbol for both. I grumble, but can't do anything about it. As long as you know that it is not the same thing, that's fine we'll just live with it.

Let's get to your question then since the system is clear now.

thanks

@towc As you said, it's easy if you can prove ( A or not A ). This you can do via 'proof by contradiction'.

If not ( A or not A ):
  ...
  Contradiction.
A or not A.

It's your turn to figure out how to fill the "..." in.

I tried that, and got somewhat stuck

¬A → B, A → B ⊦ B
1. ¬A → B   by data
2. A → B    by data
3. ¬(A ∨ ¬A) → ¬(A ∨ ¬A) trivial
4. ¬(A ∨ ¬A) → A ∨ ¬A
  1. ¬(A ∨ ¬A)  assume
  2. A →

I'm not sure how to show 4

I know I must be able to, but don't know what I can use to get there

@AjwadTaqvi this is probably not the right chatroom

look for a php room

assuming you mean the php framework

yes..

go to stackoverflow

and look for the php room

right

@AjwadTaqvi Right this is the wrong chat-room. Please read the room description before posting. Go to SO and then go to chat from there to find the correct room.

where is SO ?

you might want to look for a certificate in googling

Oh thats cool :)

@towc Well starting from the outline I wrote, there is practically only one option, which is to create a new If-subcontext.

what would be the condition of the subcontext?

1. If (not A):
  1. B    by data
2. If A:
  1. B    by data
3. If not (A or not A):
  1. If (I'm still confused)

@towc Try something. I'm not sure why you keep stating the other assumptions, because as you observed ( A or not A ) is a tautology, and the ND system we are using can prove any tautology, so you should just focus on proving ( A or not A ) from no assumptions whatever.

That's why I asked you to start with what I wrote.

oh, fair enough

If not ( A or not A ):
  If ?: // Just try the simplest possible thing and see what you get.
     ...
  ...
  Contradiction.
A or not A.

something that comes to mind is If A:, then showing that it would imply not A, but I can't seem to manage to do that with what I have

I can't seem to be able to reduce or modify that not (A or not A) so I can use it somehow

and I'll need to use it somehow, otherwise I wouldn't get a contradiction

@towc You don't need to get "not A". From "A" you can get something that already gives you a contradiction.

you say that, but I still can't think of anything :/

Just go through all the rules one by one and see which of them apply.

If not ( A or not A ):
  If A:
     // What can you do here in 1 step?
  ...
  Contradiction.
A or not A.

I can add A or not A by disjunction introduction

And doesn't that give you the contradiction you need?

that would surely lead to a contradiction, which would show you can't have A, and you'd need to prove the same so you can't have not A

but I'm not sure how to formalize the fact that it gives you a contradiction

Write what you have down, in my system.

not with my rules

I think I see it in your rules, though

If not (A or not A):
  If A:
    A or not A    by disj. intr.
  If not A:
    A or not A    by disj. intr.

let me finish it with your rules now

oh no hold on, I'm still confused

I was looking at a set of other rules before I came here, and I was thinking about those

(intrologic.stanford.edu/notes/chapter_04.html)

@towc What you have written is correct, but you can see you're not able to get the conclusion you want.

The ⇒restate rule allows you to pull in statements.

Use that.

"⊥" is the symbol for "contradiction".

so that would give me this:

If not (A or not A):
  If A:
    A or not A    by disj. intr.
    not (A or not A) by →restate
  If not A:
    A or not A    by disj. intr.
    not (A or not A) by →restate

which would ensure (not A) or (not not A)

but I'm not even sure how to formalize that it gives me that

oh, I can

@towc Your lines 3,4 can be used to get...

If not (A or not A):
  If A:
    A or not A        by disj. intr.
    not (A or not A)  by →restate
  not A               by contradiction
  If not A:
    A or not A    by disj. intr.
    not (A or not A) by →restate
  not not A           by contradiction

which would mean (not A) and (not not A) by conj. intr.

then what

@towc Then just 1 step would give you the desired conclusion? (Don't even need "not A and not not A"). Just 1 step from what you wrote.

I don't see how

oooh

it's already a contradiction

Exactly.

But there's a much shorter proof.

Let's try again:

please show

If not ( A or not A ):
  If A:
     A or not A.
     not ( A or not A ).
     Contradiction.
  not A.
  ... // Just 1 step.
  Contradiction.
A or not A.

What can you do there?

I can use an disjunction introduction and prepend A or?

would that work?

@towc Yes.

huh

And it's easy to translate back to your lecturer's system. Just read off each sentence (ending with a full-stop) and put all the governing headers on the other side of the "|−". Like line 3 becomes:

not ( A or not A ) , A |− A or not A.

⊦ A ∨ ¬A
1. ¬(A ∨ ¬A) → A ∨ ¬A
  1. ¬(A ∨ ¬A)    assume
  2. A → (A ∨ ¬A)
    1. A          assume
    2. A ∨ ¬A     by ∨I 1.1.1
  3. A → ¬(A ∨ ¬A)
    1. A          assume
    2. ¬(A ∨ ¬A)  by 1.1
  4. ¬A           by ¬I 1.2,1.3
  5. A ∨ ¬A       by ∨I 1.4
2. ¬(A ∨ ¬A) → ¬(A ∨ ¬A)  trivial
3. A ∨ ¬A         by ¬E 1,2

this is what it looks like in my system

I'll write it down on paper later

but urgh, this is happening somewhat often. I now understand the proof and it seems fairly straight forward

but if you were to ask me to do another proof, I'd probably get stuck

do I just keep practicing until they just "cllick", or are there some rules of thumb that you suggest I use?

for example, I was clearly stuck on deciding what type of contradiction I was trying to create

I picked one arbitrarily (also because you hinted at it), and many hurdles later, it just kind of worked

I guess there's some patterns you get used to and know how to solve, but maybe there's a nicer way to know what to do

@towc It's largely a matter of practice and experience. But some systems are better than others. I'm of course biased, but I am sure that anyone using my system can become proficient at using logic faster than with any significantly different system. Your lecturer's one is quite close, and you can view it as just a different way of expressing the contexts. The major difference is that his is troublesome to use (you have to keep repeating the context...

well, thanks for all the help :)

I have a feeling I'll be here often over the next of the course

Sure you're welcome, even after your course is over. =)

@towc There is actually a systematic way to get the proof of anything that can really be proven, sort of by reversing the rules. But I don't have time to explain.

does it have a name?

I'm off to a lecture anyway

Ok see you.

No name that I know.

@Secret @towc: If you want practice, you can try the list of exercises I gave here, and post your attempt (in my Fitch-style system) in this room, and I will check. Feel free to omit all lines in square-brackets.

I'll be off now. See you next time.

In propositional logic, are well-formed formula, sentence, expression, statement, and proposition are all synonyms of each other?