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?

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

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?

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)