The main Problem is we cannot fully identify
the existential quantifier with the negation
of the universal quantifier with a negated argument
in minimal and intuitionistic logic. Here some
computer experimentation. This direction
works fine, namely we have even in minimal logic:
1. |__∃x P(x) A
2. | |__∀x ¬P(x) A
3. | | P(a) E∃ 1
4. | | ¬P(a) E∀ 2
5. | | ⊥ E¬ 4, 3
6. | ¬ ∀x ¬P(x) I¬ 2, 5
7. ∃x P(x) → ¬ ∀x ¬P(x) I→ 1, 6
But the other direction doesn't work, requires
Reductio Ad Absurdum (RAA) indicated by **:
1. |__¬ ∀x ¬P(x) A
2. | |__¬ ∃x P(x) A
3. | | |__P(a) A
4. | | | ∃x P(x) I∃ 3
5. | | | ⊥ E¬ 2, 4
6. | | ¬P(a) I¬ 3, 5
7. | | ∀x ¬P(x) I∀ 6
8. | | ⊥ E¬ 1, 7
9. | ∃x P(x) ** RAA 2, 8
10. ¬ ∀x ¬P(x) → ∃x P(x) I→ 1, 9
The maximum we can do is a kind of Markov rule,
not minimal logic valid. But intuitionstic logic
valid, since it uses Ex Falso Quodlibet (EFQ)
indicated by *:
1. |__(∃x P(x) ∨ ∀x ¬P(x)) ∧ ¬ ∀x ¬P(x) A
2. | ∃x P(x) ∨ ∀x ¬P(x) E∧₁ 1
3. | ¬ ∀x ¬P(x) E∧₂ 1
4. | |__∀x ¬P(x) A
5. | | |__P(a) A
6. | | | ¬P(a) E∀ 4
7. | | | ⊥ E¬ 6, 5
8. | | ¬P(a) I¬ 5, 7
9. | | ∀x ¬P(x) I∀ 8
10. | | ⊥ E¬ 3, 9
11. | | ∃x P(x) * EFQ 10
12. | ∀x ¬P(x) → ∃x P(x) I→ 4, 11
13. | |__∃x P(x) A
14. | | P(b) E∃ 13
15. | | ∃x P(x) I∃ 14
16. | ∃x P(x) → ∃x P(x) I→ 13, 15 17. | ∃x P(x) ∨ ∀x ¬P(x) → ∃x P(x) E∨ 16, 12
18. | ∃x P(x) E→ 17, 2
19. (∃x P(x) ∨ ∀x ¬P(x)) ∧ ¬ ∀x ¬P(x) → ∃x P(x) I→ 1, 18
But when one proves ~ ∀x ~ A(x), this doesn't
mean one also assumes ∃x A(x) | ∀x ~A(x).
Mild Shock schrieb:
It seems this paper is flawed:
SOME RESULTS FOR INTUITIONISTIC LOGIC WITH SECOND
ORDER QUANTIFICATION RULES
Dag Prawitz - 1970 https://www.sciencedirect.com/science/article/abs/pii/S0049237X08707572
The cut elimination might be valid.
But I guess he is jumping to conclusions
when he thinks that a proof:
|- ~ ∀x ~ A(x)
Has the existence property. The flaw
is easy to spot. He thinks that a proof,
with the non-invertible left hand ∀:
∀x B(x) |- C
Implies nevertheless a certain form of
invertibility in that there are terms
t1, .., tn such that we have a proof:
B(t1), ..., B(tn) |- C
Unless B is restricted to some special
set of formulas, I suspect that the above
is fallacious.
Any counter example that shows the fallacy?
--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)