Natural deduction and predicate logic.

>>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.

>>7809486
Oh right, x is NOT free in B. Disregard the first part of >>7809479, then.
The second part, however, holds all the more, and OP should stop being a faggot with his faggot notation.

I can't prove it without the faggot notation

>>7809491
do this work >>7809326
??

>>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

File: Untitled.png (10KB, 590x163px) Image search: [Google]

10KB, 590x163px

>>7809308

>>7809517
>>7809521
Thanks! I'll give these a read as soon as I get a chance.