How tableaux for QL works
we supplement rules from PL with rules governing identity and the quantifiers
- tableaux for QL is also sound and complete- but we will not address that
- use it as a proof system
QL Tableaux Rules
1) every thing is identical to itself
“identity is reflexive”
a=a will always be true
2) identity is based on the indiscernibility of identicals
“if a=b, then anything true of a is true of b and vice-versa.”
Anything we can say of one, we can say of the “other”
We can substitute one name for the other in a sentence, and we will never turn a truth into a falsehood
Rule # 1: Identity is reflexive
|
|
a=a
Rule #2: indiscernibility of identicals
if we have a=b on a branch, and some sentence S involving a on that branch, we can introduce to that branch the sentence that results from substituting any number of occurrences of a in S with b
a=b S | | S(b/a)
ex. if we have a=b on a branch and Ga→Fc, we can write Gb→Fc, replacing a with b
ex 2. if we have a=b on a branch and Ga→Fa, we can write Gb→Fa, Ga→Fb, or Gb→Fb, each of which is obtainable by replacing one of more occurence of a with b
Existential quantifier ∃xFx
we have ∃xFx on a branch, saying that something is F
- if something is F, we can give it a name
- we could call it a, then conclude that a is F, ie. Fa
- more than one thing might be F, but that’s okay, with the tableaux rules we are just saying what Must be true given the sentence in question
- we don’t know how many things are F, but we know that one thing must be, at least, so all we can conclude is that one thing, a, is F
Crucial caveat
- “a” must be a name that we haven’t used before on this branch
- we are introducing a New name for that thing that is F– we can’t assume that the thing that is F is the same thing we’ve already said something about
- so if a name has already been used on a branch, we can’t use that name as the name for the thing that is F, we have to pick a new name
Test the consistency of
∃xFx
∃xGx
∃xFx ✓
∃xGx ✓
|
Fa
Gb- something is F, give it a name “a”
- something is G, give it a name “b”
- we can’t name the two things the same and we have no reason to think that it is the very same thing that is in F and in G
Thus, every time we deal with a new existentially quantified sentence, we replace every occurence of the bound variable with a name that is new to that branch
Universal quantifier ∀xFx
we have ∀xFx
Everything is F
- for any name we like, we can put it in place of the bound variable and get a true sentence
If everything is F, then a is, so we can get Fa
If everything is F, then b is, so we can get Fb… etc
- We NEVER tick off a universally quantified sentence, because we are never finished with it- we can always apply the rule to it again with a new name
- we simply make a list of the names we have used, so that we know there’s no need to use That name again
∀xFx /a,b
|
Fa
Fb
and so on...But while I can use any name I like with the universal quantifier, in practice I only want to use names that already appear on the branch, or if there are none then one new name
REMEMBER: I am trying to get a contradiction on the branch, and the best shot at doing so is to use names that are already in play, because then I might contradict one of the sentences that I already have
Order of application of rules
Always want to apply the rule for any Existentially quantified sentences before dealing with Universally quantified sentences
- the existential quantifiers will give us our names, that we can then use for the universal quantifier rule
1) negated quantifier rules
2) existential quantifier rules
3) universal quantifier rules
Negations of quantifiers
We rely on equivalences- if it’s not the case that everything is F, then at least one thing fails to be F
¬∀xFx ✓
|
∃x¬Fx
And if it’s not the case that something is F, then everything fails to be F
¬∃xFx ✓
|
∀x¬Fx
* trick to remember this, the negation jumps over the quantifier, and you swap quantifiers
Test set {∃x(Fx∧Gx), ∀x(Gx→Hx), ¬∀xHx} for consistency
steps
1) list sentences
2) deal with negated quantifiers
3) we have 2 existential and one universal, deal with existential first
- introduce a new name to replace for the variable x
Branching universal quantifiers
remember, first deal with negations, then existential, and universal at last, plugging in the names (“a”, “b”, etc) used into x for the universal sentence
- when a branch stemming from a universal sentence remains open, it does not mean it is complete
- it is never complete, thus we never check off the original sentence, as we could continue plugging in names
- however, if it hasn’t closed by then, it is not going to close, because the names used in the set of sentences have already been used
- after this make a model on which the set of sentences are all true
Models for Tableaux in QL
Testing for consistency
- if consistent will get a model
Can also test for validity by testing for consistency the premises and the negation of the conclusion
Domain- the things named by every name on this branch
D: {a, b}
then we construct the extensions for the predicates to make the simple predications or their negations that appear on the branch to be true
I(a) = a i(b) = b
I(F) = a --- F is true for a I(G) = a ---- G is true for a, but false for b ---- ¬Gb remains open, not Gb, G is not b I(H) = a --- H is true for a --- ¬Hb remains open
