====== Logika - Zadanie 100. ======
Dowodzenie implikacji wprost polega na założeniu poprzednika i wyprowadzeniu zeń następnika. Ponieważ strzałeczki są dwie, osiągamy w końcu:
  * W założeniu: $[\exists x. (\phi \Rightarrow \psi)] \wedge \forall x. \phi$
  * W celu: $\exists x. \psi$
  * Weźmy więc tego $x$, dla którego z $\phi$ wynika $\psi$ i skorzystajmy z faktu, że dla każdego $x$ jest $\phi$.
  * Wtedy w szczególności dla naszego $x$ jest $\phi$, a że $\phi \Rightarrow \psi$, to i $\psi$.
  * Koniec.

====== Inny dowód ======

$(\exists x. (\phi \Rightarrow \psi)) \Rightarrow (\forall x. \phi) \Rightarrow (\exists x. \psi) $

Sprawdzimy, czy powyższa formuła jest prawem rachunku kwantyfikatorów. 

Definicja. Formuła jest prawem rachunku kwantyfikatorów, jeżeli jest spełniona przy każdej interpretacji symboli funkcyjnych i relacyjnych.

Jeśli formuła ta jest tautologią, to zanegowanie jej musi dać nam formułę, która jest sprzeczna. Mamy wtedy:

$\neg [(\exists x. (\phi \Rightarrow \psi)) \Rightarrow (\forall x. \phi) \Rightarrow (\exists x. \psi)] \equiv (\exists x. (\phi \Rightarrow \psi)) \wedge \neg ((\forall x. \phi) \Rightarrow (\exists x. \psi)) \equiv (\exists x. (\phi \Rightarrow \psi)) \wedge (\forall x. \phi) \wedge \neg (\exists x. \psi)) \equiv (\exists x. (\phi \rightarrow \psi)) \wedge (\forall x. \phi) \wedge (\forall x. \neg \psi))$

Należy zatem udowodnić, że powyższa (zanegowana) formuła jest zawsze fałszywa.

Załóżmy więc nie wprost, że jest prawdziwa dla pewnej ustalonej interpretacji. Wtedy dla każdego x $\phi$ jest prawdziwa, oraz dla każdego x $\neg \psi$ jest prawdziwa, więc $\psi$ jest dla każdego x fałszywa, co stoi w sprzecznościz prawdziwością $\exists x. (\phi \Rightarrow \psi)$, ponieważ, skoro dla każdego x $\phi$ jest prawdziwa a $\psi$ jest fałszywa, to implikacja $\phi \Rightarrow \psi$ dla każdego x jest fałszywa. Nie może zatem istnieć x dla którego $\phi \Rightarrow \psi$ jest prawdziwa.

Zatem zanegowana formuła nie może być nigdy prawdziwa, jest więc zawsze fałszywa. Z tego natomiast wynika, że formuła wyjściowa jest zawsze prawdziwa, jest więc prawem rachunku kwantyfikatorów, cnu.

Jest to propozycja dowodu i nie jestem jej całkowicie pewien. Jeśli ktoś znajdzie błąd, to byłbym wdzięczny za informację i konstruktywną krytykę ;-).