AU - cv3

Pohadka: Ostrov, lide jsou poctivci/lhari, k tomu mohou byt jeste elitni. Existuji tam kluby, elitnaci maji sve kluby. Existuji doplnkove kluby, takze kazdy, kdo neni v klubu Milujeme_Justina_Biebera_A_Nesnasime_Mrkew je v klubu Justin_Bieber_Je_Tulpas_A_Mrkev_Si_Strkam_Uplne_Vsude. Ke kazdemu klubu existuje alespon jeden clovek, ktery tvrdi, ze je jeho clenem.

Mame dokazat, zda-li existuje alespon jeden neelitni poctivec.

Predikaty: c(X)…X je clovek, ~c(X) znaci klub e(X)…elitni p(X)…poctivec X, ~p(X)..lhar X k(C,K)…C je clenem klubu K

Axiomy:

• Elitni poctivci tvori klub:

fof(el_poc_klub,axiom, ( ?[x] (

     ~c(x) & ![y] (  c(y) & p(y) & e(y)  )
   )

⇔ k(y,x)

–nebo jen– c(y) ⇒ ¹⁾ ⇔ k(y,x)) –end–

) ).

* Elitni padousi tvori klub (jen pridat 1 negaci): fof(el_pad_klub,axiom, ( ?[x] (

     ~c(x) & ![y] (  c(y) & ~p(y) & e(y)  )
   )

⇔ k(y,x)

) ).

* Kazdy clovek c, kdo neni v klubu Kl, je v klubu Dopl: fof(dopln_klub,axiom, ( ![Kl] (~c(Kl) ?[Dopl] ( ~c(Dopl) ![c]( c©

~k(c,Kl) <=> k(c,Dopl)

) )) ) ).

* Ke kazdemu klubu k existuje clovek c, ktery tvrdi, ze je jeho clenem: fof(clen,axiom, ( ![k] (~c(k) ?[c] ( c© & ( (p© & k(c,k))

(~p© & ~k(c,k)) ) ))

–nebo– p© ⇔ k(c,k) –end– ) ).

* Otazka: Existuje jeden neelitni poctivec? fof(neel_poc,conjecture, ( ?[x] (c(x) & p(x) & ~e(x) ) ) ).