Natural Deduction for Quantifiers - Worked Examples | Attic Philosophy

In this tutorial video, we look at two examples of how to use the rules for quantifiers in First-Order Natural Deduction. Make sure you've watched Natural Deduction for Quantifiers first: • Natural Deduction for ...
00:00 - Intro
00:29 - Recap
01:00 - Rules for quantifiers
01:24 - Universal introduction
01:48 - Example: Universal Introduction
04:02 - Existential Elimination
05:04 - Example: Existential Elimination
07:30 - Wrap-up
Related videos:
Natural Deduction for Quantifiers • Natural Deduction for ...
Proofs in Logic • Proofs in Symbolic Log...
How to do Natural Deduction Proofs • How to do Natural Dedu...
Rules for Natural Deduction • Rules for Natural Dedu...
How to use Quantifiers • How to use Quantifiers...
If there’s a topic you’d like to see covered, leave me a comment below!
Links:
My academic philosophy page: markjago.net
My book What Truth Is: bit.ly/JagoTruth
Most of my publications are available freely here: philpapers.org/s/Mark%20Jago
Get in touch on Social media!
Instagram: / atticphilosophy
Twitter: / philosophyattic
#logic #quantifiers #proof

[@tubate20092]

Finally somebody who Takes his time and explains with everyday-words the different meanings of the logic operations

[@AtticPhilosophy]

You're welcome!

[@davehendr1]

This is the best explanation on the use of these rules that I have seen or read. Again, wonderful explanations.

[@AtticPhilosophy]

Thanks!

[@ashleyjfay]

You are a LIFE SAVER!!! I really appreciate your videos, extremely easy to understand.

[@AtticPhilosophy]

Thanks! Glad this one helped.

[@kristianhansen6013]

this is GREAT - arigatou from Japan

[@wenaolong]

On going between the universal and particular or vice versa there is a formal symmetry about the axis of a purely imaginary cut between those domains, an ideal distinction that acts as a bridge between them. Precisely on this axis man becomes the measure of all things.

[@toe_fans]

Best channel on youtube.

[@anisrashidov235]

It could be really helpful if you also posted some worksheets, but other than that, your videos are great.

[@AtticPhilosophy]

I guess it would help, but time!

[@jpc5357]

Great video--(from one prof to another). Can you tell me what program you're using to write the proofs?

[@AtticPhilosophy]

Thanks! I’m handwriting the proofs on an iPad, using goodnotes with a black background. I hit screen record when I start the camera & record audio too, so I can easily match up with the main camera. It’s the easiest way to do handwriting on videos I’ve found so far - still a bit of an effort!

[@jpc5357]

@@AtticPhilosophy I use MS whiteboard. The trouble is that I write a on a Wacom tablet, but it appears on the screen, so my presentations look like they're authored by a child.

[@mamo987]

@@jpc5357 Hi i am wondering if you or Attic philosophy could answer a question of mine about logic ?

[@mickh2023]

I have a question. Can you please tell me if this natural deduction I have made is incorrect?
0 (zero premises)
∀x Ax (assumption)
Aa(b,c) (universal elimination)
∃x Bx (assumption)
Ba(b,c) (assumption / existential elimination's first step)
Ba(b,c) ∧ Aa(b,c) (conjunction introduction)
∃x Bx ∧ Aa(b,c) (existential introduction)
∃x Bx ∧ Aa(b,c) (existential elimination's final step)
a(b,c) is a function with two arguments

[@AtticPhilosophy]

The conclusion follows, but the proof isn’t quite right. When you use existential elimination, it has to be with a new constant, one you haven’t used before. So reorder things: existential assumption first, then universal instantiation with the same constant. Also I guess you want brackets in the conclusion: Ex(Bx & Aa(bc)), else you could get there directly in line 4. It’s also probably better to call the first assumptions *premises*, since assumptions should be discharged by the end of the proof.

[@mickh2023]

​@@AtticPhilosophy Thanks a lot, Yeah, I asked it because I have been creating a cool visual representation of a proof system, I would like to share with you the mental picture I have. That's how I imagine it: when we are given some premises to explore what follows from them, it's basically as if we are given what I call an "axiom set", a set that has some "axioms" in it, and it contains all the formulas that are logical consequences of them. The "zero set" contains no axioms, and it contains all the logical truths of FOL. All axiom sets contain this "zero premise". When we start a new subproof in a proof, I think that what we're doing is, we're creating a superset that contains our axioms (the premises), with the addition of a new one. In this superset, all the logical consequences of our premises are within this superset, but this superset also includes other consequences outside the set of our premises. Here is how I imagine it: A |-- C (this is our original axiom set), we can do this: A, B |-- C , which is a superset of the of the former, and contains all the logical consequences of the former. I noticed that conditional proof is this principle: A, B |-- C is equivalent to
A |-- (B --> C). Conditional proof allows us to work on a superset and put that in our premise set. I picture these sets as circles with formulas inside them, with some of these formulas called "axioms" and highlighted in blue, in which all the rest follows. ZF(C) for example, is one such set, with its 9 or so axioms. In a proof, when make two subproofs independent of each other, we are basically making two supersets whose intersection is our premise set. I have been playing around with the 4 FOL rules of inferences, and I have observed that UI seems to only require that the constant is not present in the axioms entailing the formula, but if its be present in the "logical consequences that aren't axioms", it's ok.
Another way to visualise it is like this (I took inspiration from your videos on modal logic diagrams):
We have our starting set (visualised as a circle) with some axioms (our premises, just floating around in this circle) + our "zero axiom", they are highlighted in blue. We use our rules of inference to deduce logical consequences from these axioms. At any time we can create another set, that has our premises + a new assumption. This set has access to all the logical conclusions of our starting set. We can kind of express this relationship with an arrow between these two.
So yeah, I just really like thinking in diagrams haha. I don't know what you think about it, but I guess I'd just like to share it. I'm relatively new to logic, but it's one of the things I quite like and am passionate about.

[@AtticPhilosophy]

Yes, you can think of premises as 'additional axioms'. In a proof, it's usually important to track what assumptions were used for what. In natural deduction, that's what subproofs do. It's a bit clunky. You might want to take a look at *sequent calculus*, which is a much nicer way to track assumptions in proof (but more complicated).

[@Nicoder6884]

2:12 You keep mentioning prenex normal form, but you have not made a video on what it is or how it works. I happen to know that "prenex" means "all quantifiers are at the beginning of the statement", but it's not very intuitive as to how ∀x(Fx -> Ga) is actually the prenex translation of (∃xFx) -> Ga

[@AtticPhilosophy]

Good spot - I did a video on prenex but, I just realised, never got around to realising it! So thanks for reminding me.

[@semuren]

@@AtticPhilosophy Thank you for these useful videos on basic logic. Has this video you made on prenex normal form (PNF) been posted? If so, could you please share a link or perhaps the exact video name. PNF is mentioned in this video and in the last one, and I can and have looked it up, but I enjoy learning from your videos and so I would really also like to see your video on PNF. Thank you again for your hard work on these videos and for your books (which I have gotten and put on my reading list).