Natural deduction and predicate logic.

Images are sometimes not shown due to bandwidth/network limitations. Refreshing the page usually helps.

You are currently reading a thread in /sci/ - Science & Math

You are currently reading a thread in /sci/ - Science & Math

Thread images: 2

Anonymous

Natural deduction and predicate logic. 2016-01-25 08:50:49 Post No. 7809225

[Report] Image search: [iqdb] [SauceNao] [Google]

Natural deduction and predicate logic. 2016-01-25 08:50:49 Post No. 7809225

[Report] Image search: [iqdb] [SauceNao] [Google]

Hi ,

Can somebody tell me if line 10 is correct ? Did I do a mistake?

∀x(A ∨ B) ⊢ ∀x A∨B , Note: x is not free in B .

1.∀x(A∨B) premise

2.¬(∀A∨B) assumption

3.x0

4.(A∨B) [x/x0] (∀xe),1

5.A[x/x0] ∨ B x is not free in B

6.B Assumption

7.∀x A ∨ B (Vi),6

8.⊥ (¬e) 2,7

9.A[x/x0] (⊥e),8

10.∀xA (∀x)i,3-9

11.∀A∨B (vi),10

12.⊥ (¬e) 2 , 11

13.¬¬(∀A∨B) (¬i),2-12

14.∀A∨B (¬¬e) ,13

>>

>>7809225

What book are you using? I've only worked with propositional logic in Fitch style deduction systems, not predicate logic.

>>

What the fuck is that shit, can't you write trees ? That proof should be trivial and I have no idea what's going on.

>>

Line 9 is wrong, you just proved not(B), you cannot use bottom-elim to conclude whatever

>>

>>7809308

Ok, you just didn't write the or-elim on 5, other branch was indeed trivial but you need to write all steps

>>

>>7809225

>2.¬(∀A∨B) assumption

I do not follow this line. why do you assume this ? do you work in FOL ? [only plebs work in FOL]

>>

ok look, this is fucking awesome

>>

>>7809225

I do not understand this since it should be direct that since ''x is not free in B'' you only need to say :

-let x0 st ''A or B''

-which means : let x0 st ''A[x0] or B''

-then since x0 is arbitrary, ''∀x A∨B ''

>>

>>7809318

No, of course he's working in CoC with UA like all the patricians.

>>

∀x(A ∨ B) ⊢ ∀x A∨B , Note: x is not free in B .

But then you will have :

1.∀x(A∨B) premise

2.x0

3.A[x/x0] ∨ B x is not free in B

How do you continue from here to prove that

∀x A∨B

I tried to prove by negation and assumed that ¬(∀A∨B).

>>

>>7809345

forall-intro

>>

>>7809318

He's using classical logic

>>

>>7809225

>using non-intuistionistic rules of deduction

It's like you want to be cucked.

>>

All of you dont know a shit in logic

>>

>>7809297

You are a retard.

>>7809318

That's called an auxiliary assumption. It's an assumption that you use in order to prove something else. In this case OP is assuming it for the sake of contradiction.

First order logic is the best logic. The fact that you didn't understand the basic concept of assumptions shows that you have probably never written a single line of second order logic.

>>7809331

>Calculus of Constructions with Univalence Axiom

>Fitch style notation

kek'd

>>7809353

Classical logic and First order logic are not mutually exclusive. Classical logic just means you have double negation elimination:

not(not(P)) entails P

Which is what OP uses between line 13 and 14.

>>7809363

mah nigga

Though technically classical logic is just a special case of intuitionistic logic.

>>

>>7809225

Hey motherfuckers, first time I seen this shit in my life. What the fuck is it and how do I learn everything about it. I gots me a book from 1960s about propositional calculus or something but I keep reading that the symbols are out of date (an introduction to symbolic logic). What it do hummies

>>

kushelaemak No. 7809418

>>

>>7809418

shut the fuck up man

>>

>>7809418

OP is working in Fitch notation which is used for writing proofs.

https://en.wikipedia.org/wiki/Fitch_notation

I don't know where you can learn it for predicate logic (where you have universal and existential quantifiers in your logic) but for propositional logic you should read The Logic Book. It's actually aimed at philosophyfags instead of math majors so it's a super easy and approachable introduction to formal logic.

Natural deductions are another method of writing proofs.

https://en.wikipedia.org/wiki/Natural_deduction

These come up a lot in computer science and advanced mathematics (eg. categorical logic, homotopy type theory, etc..). For an introduction to this I would recommend the Oregon Programming Languages Summer School lectures on Basic Proof Theory (they're available online for free). You should probably already have some background in formal logic ahead of time though. As an alternative you can learn lambda calculus (I recommend Peter Selinger's notes on Lambda Calculus) and through the Curry Howard Isomorphism understand natural deductions in logic.

There's a third method called "Tableux" or "Truth Trees".

https://en.wikipedia.org/wiki/Method_of_analytic_tableaux

I believe this is also covered in The Logic Book but if not you can find a description of it in Simpson's Mathematical Logic lecture notes.

>>

>>7809405

So the proof is correct ?

>>

>>7809453

I have no idea. I've never learned how to use Fitch style derivations with predicate logic. I was under the assumption that no one did it because many statements aren't provable (because validity in predicate logic isn't decidable). I'd be interested in learning and could probably tell you if it's correct or not if I could get ahold of a resource that details the rules.

>>

>>7809462

so learn it

>>

Ok :)

>>

>>7809462

Ok :)

>>

>>7809468

I asked anon for the book they were using.

>>

Let x = 0. Let A == "x != 17" and let B == "x = 17". Then "forall x, (A or B)" holds, but "(forall x, A) or B" does not hold. Therefore, your proof can't possibly be right.

Also, stop being a faggot and write your open terms with parameters; it will make things ever so much simpler. Compare:

Let x0 = 0, A(x) == (x != 17), B(x) == (x = 17). Then "forall x, (A(x) or B(x))" holds, but "(forall x, A(x)) or B(x0)" does not holt.

>>

>>7809479

This is what I thought at first but then I noticed OP had a note that says x isn't free in B.

I agree that it would help if OP wrote their predicates with a list of free variables as parameters.

>>

>>

I can't prove it without the faggot notation

>>

>>7809508

That's the intuition, yes. However that is not a proof.

>>

>>7809508

Yes. But this is immediately obvious if you write A(x) and B, in general; then your flag says "forall x, A(x) or B", and on line 4 you immediately derive "A(x0) or B".

>>

https://cs.uwaterloo.ca/~plragde/cs245/06-prednd.pdf

>>

https://homepage.univie.ac.at/christian.damboeck/ps06/clemente_nat_ded.pdf

Thread images: 2

Thread DB ID: 463530

All trademarks and copyrights on this page are owned by their respective parties. Images uploaded are the responsibility of the Poster. Comments are owned by the Poster.

This is a 4chan archive - all of the shown content originated from that site. This means that 4Archive shows their content, archived. If you need information for a Poster - contact them.

If a post contains personal/copyrighted/illegal content, then use the post's