Re: Drinker Paradox again (Re: Some Error in Dag Prawitz 1970 Paper)

Because ∃x ∀y (P(y) → P(x)) is not intuitionistically
valid, it is also the case that for a witness a
we have that ∀y (P(y) → P(a)) isn't provable.
Because otherwise the existential property would be
violated. Lets try this here:
:- show((![y]: (p(y) => p(a)))).
Fehler: Direktive fehlgeschlagen.
user auf 5
Yeah it is indeed not provable. At least when we
trust the above proof search. But its also easy
to see since ∀y and → are invertible, to prove it,
we would have to prove:
p(y) |- p(a)     with y ∉ p(a)
where the side condition is from the ∀y inversion.
So the counter example is this proof:
|- ¬ ∀x ¬ ∀y (P(y) → P(x))
Mild Shock schrieb:

The counter example is a variant of the
Drinker Paradox. Its actually a horrid counter
example, since it shows something much
 more disturbing. This here is
intuitionistically provable:
 /* intuitionistically provable */
|- ¬ ∀x ¬ ∀y (P(y) → P(x))
 But this here isn't intuitionistically
provable:
 /* not intuitionistically provable */
|- ∃x ∀y (P(y) → P(x))
 So the Dag Prawitz approach of modelling the
existential quantifier ∃x as ¬ ∀x ¬, which he
repeats over and over in other papers, and
 in his natural deduction booklet, is a very
strong form of existential quantifier. Not the
intuitionistic existential quantifier.
 Mild Shock schrieb:

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?
>

>