Post by Eugene 2.0 on Aug 4, 2023 6:48:51 GMT
Existential Instantiation (or Existential Elimination) Analogy in Propositional Logic
In propositional logic we know theorems of conjunction elimination and disjunction introduction. With them we can interpret the predicate logic formulas:
Another story with two other predicate logics rules, which are being used for completing the proof sequences to get some important theorems in predicate logic. I guess we can trace similar rule in propositional logic. This time I want to view EI (or EE) here, that this rule has an analogue in propositional logic.
This is, by the way, how the existential instantiation looks like:
First of all, this rule is at least weird. Why so? In numerous textbooks additional prescriptions say that 'y' doesn't appear before, however 'y' can appear, but what is impossible is to have Ay before, not just a variable 'y'. I'll show how it works.
Secondly, we want to say for why this rule in predicate logic and what does it mean? It means that if we assume or prove somehow that from a certain S we can trace something that is Ay, we can assume Ay. And I'm going to start right from its analogy in propositional logic.
Do you remember dilemmas? These formulas are interesting that it cannot be entailed within standard forms of axioms, but it can have the inference of it in the Russell-Whitehead systems of axioms. Anyway, the broader variant of this formula tells us exactly what we're told applying the existential instantiation rule in predicate logic.
1. ((p→q)&(r→q)&(pvr))→(qvq),
2. (qvq)→q, tautology
3. ((p→q)&(r→q)&(pvr))→q, HS 1, 2
I guess it's obvious how can we get a dilemma. Anyway, if we want to check a certain dilemma we need to parallel paths. It works like this in proofs:
1. (p→q), (r→s), p ⊢ (qvs) (assumption 1)
2. (p→q), (r→s), r ⊢ (qvs) (assumption 2)
3. ⊢ pvr (it was given, or conjunction elimination)
4. ⊢ qvs (we can derive this from both assumptions)
It must be noted that each new assumption derive the consequent, so we can stop even after completing the 1st assumption, but along with it we have to take into account what was taken. So, this is just the same instruction we use for the existential instantiation in predicate logic. Check this out:
Note, that using Pa or Pb there is incorrect, but that was done only to illustrate. However, all other nuances are saved, and we can say that the rule in predicate logic requires us to think in such way that is similar to the way of proving in propositional logic.
Again, when we do any existential instantiation rule requires us to use another new variable, because those variable along with a specific predicate can repeat a certain formula, otherwise the method of proving cases would be broken. We need to assume parallel cases for the dilemma (as p, r above).
Simply saying, the existential elimination rule is nothing, but a wider way of dilemmas in propositional logic, and it shares the same limits and the same requirements. Because of that there's nothing serious to object for considering proofs in predicate logic to analogues in propositional logic. And I just showed this.
In propositional logic we know theorems of conjunction elimination and disjunction introduction. With them we can interpret the predicate logic formulas:
p&q → p :: ∀xAx → Ay
p → pvq :: Ay → ∃xAx
Another story with two other predicate logics rules, which are being used for completing the proof sequences to get some important theorems in predicate logic. I guess we can trace similar rule in propositional logic. This time I want to view EI (or EE) here, that this rule has an analogue in propositional logic.
This is, by the way, how the existential instantiation looks like:
∃xAx ⊨ Ay, if 'y' doesn't appear anywhere before
First of all, this rule is at least weird. Why so? In numerous textbooks additional prescriptions say that 'y' doesn't appear before, however 'y' can appear, but what is impossible is to have Ay before, not just a variable 'y'. I'll show how it works.
Secondly, we want to say for why this rule in predicate logic and what does it mean? It means that if we assume or prove somehow that from a certain S we can trace something that is Ay, we can assume Ay. And I'm going to start right from its analogy in propositional logic.
Do you remember dilemmas? These formulas are interesting that it cannot be entailed within standard forms of axioms, but it can have the inference of it in the Russell-Whitehead systems of axioms. Anyway, the broader variant of this formula tells us exactly what we're told applying the existential instantiation rule in predicate logic.
DE: ((p→q)&(r→s)&(pvr))→(qvs), this is the ordinary form
DE: (p→q), (r→s), (pvr) ⊢ qvs and it's rule form
A particular change can show that this formula above is also a simple dilemma:
1. ((p→q)&(r→q)&(pvr))→(qvq),
2. (qvq)→q, tautology
3. ((p→q)&(r→q)&(pvr))→q, HS 1, 2
I guess it's obvious how can we get a dilemma. Anyway, if we want to check a certain dilemma we need to parallel paths. It works like this in proofs:
1. (p→q), (r→s), p ⊢ (qvs) (assumption 1)
2. (p→q), (r→s), r ⊢ (qvs) (assumption 2)
3. ⊢ pvr (it was given, or conjunction elimination)
4. ⊢ qvs (we can derive this from both assumptions)
It must be noted that each new assumption derive the consequent, so we can stop even after completing the 1st assumption, but along with it we have to take into account what was taken. So, this is just the same instruction we use for the existential instantiation in predicate logic. Check this out:
∃xPx ⊨ Py :: p ⊨ q :: Pa → PavPb :: PavPb=Py
∃xPx ⊨ Py :: r ⊨ s :: Pb → PavPb :: PavPb=Py
Note, that using Pa or Pb there is incorrect, but that was done only to illustrate. However, all other nuances are saved, and we can say that the rule in predicate logic requires us to think in such way that is similar to the way of proving in propositional logic.
Again, when we do any existential instantiation rule requires us to use another new variable, because those variable along with a specific predicate can repeat a certain formula, otherwise the method of proving cases would be broken. We need to assume parallel cases for the dilemma (as p, r above).
Simply saying, the existential elimination rule is nothing, but a wider way of dilemmas in propositional logic, and it shares the same limits and the same requirements. Because of that there's nothing serious to object for considering proofs in predicate logic to analogues in propositional logic. And I just showed this.