Proof Trees for First Order Logic | Attic Philosophy
ฝัง
- เผยแพร่เมื่อ 9 ก.ค. 2024
- How do proof trees work in first-order logic? Let me show you! We'll see how the rules work for quantifiers and for identity. We'll build on proof trees for propositional logic, which I cover in this video:
• Logic tutorial: how to...
00:00 - Intro
00:37 - [Link to PL trees]
01:14 - Rules for connectives
01:25 - Rules for Quantifiers
01:51 - Negated quantifier rules
02:49 - Universal quantifier rule
04:21 - Example
05:02 - Re-using the Universal Rule
06:29 - Existential Quantifier rule
07:39 - Example
08:48 - Link to ND E rule video
09:31 - Rules for identity
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 #philosophy
What does the proof tree show? Does it show that a first order logc statement is derivable given certain assumptions? If so, does that mean we have a means of determining the if a sentence is derivable in any first order logic systwm with a finite number of axioms?
It’s a way of checking whether a given conclusion follows logically from given premises. Since FOL isn’t decidable, it’s not a method that will always give you an answer.
@@AtticPhilosophy OK. So my understanding is that for propositional logic for any given sentence we can use the proof tree process to determine if the sentence is a tautology. If it is not a tautology, the process will give us an example of a truth assignment that will result in the sentence being false. In addition, this process can be done in a purely automated way. We can do the same by the use of truth tables and exhaustively going through each combination of truth assignment for each propositional variable.
For predicate logic, we also have a proof tree process. Typically when it is used we use a judicious choice of variables when using the universal quantifier rule in order to show the sentence is valid (could we also use the same process to show it is not valid?). In principle, however, we could choose every variable in our tree whenever we encounter a universal quantifier (so the process could be subject to automation). The problem is, if we do this, on some (most??) occassions the process will never stop and so we will not know if it is valid or not. Is that right? If so, if we come across a new first order logic sentence that we wish to prove, would it be worthwhile puting it through the proof tree process first to see if we get a result? (also bearing in mind that most axiomatic systems we are interested in e.g. ZFC have effectively an infinite number of axioms!).
@@Simon-lb2iu Yes that's right. There's infinitely many examples for which you will get an answer and infinitely many for which you won't! There's also large fragments of FOL which are decidable (= guaranteed answer). In practise, it's often easy to see a tree has got itself into a never-ending loop.
I really like this presentation of the method of analytic tableaux. I have two questions if that's okay. 1) Does this proof calculus satisfy the completeness theorem? I suspect it does, but I don't know how hard it would be to prove. 2) Can we remove = as a special symbol by replacing it with a binary predicate E that's an equivalence relation, but also a congruence with respect to every predicate symbol, and get a proof calculus that's just as powerful, but less convenient?
Yes, it’s complete for the main logics, with slightly different rules. It’s easy to prove completeness, because the rules closely mirror the semantic clauses - it’s much easier than the completeness proof for natural deduction, for example. The rules for identity say it’s a reflexive, symmetrical, and transitive relation which allows substitution, so yes, any equivalence relation with those rules would do.
2:53 is really unintuitive and I do not understand why.
But ok, I got it. Still not 100% sure how it is going to be used, but I am no longer incredulous.