Re: Some Error in Dag Prawitz 1970 Paper

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?