Zadaj formalny vyrok. Napr. :

Kde:


Ak sa jedna o ekvivalenciu, tak ju dokaz v smere:
A) - zlava doprava
B) - zprava dolava



Ine priklady (z cviceni):
Dokazatelne priamo:
p>((p>q)>((~r>s)>((s>~p)>(r)))) ...argument ze nutne existuju jednoduche objekty
(~pvq)>((p^~r)>((~p=~s)>(s^q))) ... funguje
((p=r)^(qvs))>(r>(~q>(p^s)))...funguje
((p>r)^(q>r))>(~r>(~p^~q))...funguje
((~p^q)>~r)>(r>(q>p))...funguje
(p>s)>((s>~r)>((~r>t)>(p>t))) ... Qui bibit, dormit; qui dormit, non peccat; qui non peccat, sanctus est (ergo: qui bibit sanctus est).
(p>(q^r))>((~q^~r)>(((q^r)>(~u^~w))>(~p>((~q^~r)^(u^w))))) ... Ak vesmir vznikol, tak ma pociatok a koniec./Melissos
((ovp)>r)>((q>o)>(((q^r^s)>t)>(q>(s>t)))) ... Ak sa Rimania domnievali, ze su v nebezpecenstve...
Dokazatelne nepriamo:
(~p>(q^~q))>p...funguje
(((p^s)v~q)^(~q>(~sv~p)))>((~rv~(~pv~s))>(qv~r))...funguje
(p>~p)>~p...uvedie priamy dokaz, hoci uz robi nepriamy
Ekvivalencie:
(q>(r>p))=((r^~p)>~q)...funguje
(~(p^r)>~(~s^q))=((q>(p^r))vs)...zatial nedospeje k zaveru v smere A
((~q^~r)v~p)=((qvr)>~p)...funguje
Predikatorova logika-vyroky:
Ex(~P[x]>Q[x])=((ExP[x])v(ExQ[x]))...zlava doprava funguje ciastocne, opacne vobec
Ex(A[x]vB[x])=(~(ExA[x])>(ExB[x]))
Vx(P[x]>(Q[x]^R[x]))>((~Q[a]^~R[a])>(Vx((Q[x]^R[x])>(~U[x]^~W[x]))>(Vx(~P[x])>Vx((~Q[x]^~R[x])^(U[x]^W[x]))))) ... Ak cosi vzniklo, tak ma pociatok a koniec./Melissos
Vx(K[x]>Z[x])>(Vx(Vy((H[y,x]^K[x])>(H[y,x]^Z[x]))))..Ak kazdy kon je zviera, tak kazda hlava kona je hlavou zvierata
Vx(Vy((C[x,y]^T[y])>T[x]))>(Vy(L[y]>T[y])>(Vx(D[x]>Ey(L[y]^C[x,y]))>Vx(D[x]>T[x])))....Clovek je telesny. Dusa je castou cloveka. Dusa je telesna.
Vx(Vy(P[x,y]>L[x,y]))>(Vx(Vy((H[x]^C[y])>P[x,y]))>Vx(Vy((H[x]^C[y])>L[x,y])))...Protikladne sa lieci protikladnym. Protikladom horucky je chlad. Horucka sa lieci chladom
Vx(P[x]>(M[x]vN[x]))>((~(ExM[x])^~(ExN[x]))>~(ExP[x]))...Nemoznost pohybu podla Krona
Vx(B[x]>(S[x,a]v~S[x,a])) >( Vx((B[x]^S[x,a])>(Vy(W[y]>S[x,y])V(Ey(W[y]^S[x,y])^Ey(w[y]^~S[x,y])))) >( (Vx(B[x]>Vy(W[y]>S[x,y]))>~(Ey(W[y]^Z[y]))) >( Ey(w[y]^Z[y]) >( Vx(B[x]>~(Vy(W[y]^S[x,y]))) ))))...Nie je pravda, ze sa Boh stara o vsetky veci
Sylogizmy:
Vx(F[x]>S[x])>(Ex(L[x]^~S[x])>Ex(L[x]^~F[x]))..Vsetky filozofky su sebavedome. Niektore logicky nie su sebavedome.
Vx(~H[x]>~P[x])>(Vx(H[x]>~S[x])>Vx(P[x]>~S[x]))...Ziadny nestastny clovek sa spokojne nepochechtava. Ziadny stastny/happy clovek nestona....funguje
Vx(C[x]>S[x])>(C[a]>S[a])...Vsetci ludia su smrtelni. Sokrates je clovek. Sokrates je smrtelny
Vx(P[x]>B[x])>(~B[a]>~P[a]) ... Vsetci psy bresu. Ja nebresem. Ja nie som pes.
Vx(K[x]>P[x])>(Z[a]>(Vx(Z[x]>K[x])>P[a])) ... Vsetky kovy su vodice.Koruna uhorskeho krala je zo zlata.
Vx(P[x]>S[x])>(Vx(S[x]>~H[x])>(Vx(~H[x]>N[x])>Vx(P[x]>N[x]))) ... Qui bibit, dormit; qui dormit, non peccat; qui non peccat, sanctus est (ergo: qui bibit sanctus est).
Vx(S[x]>M[x])>(Vx(M[x]>D[x])>Vx(S[x]>D[x]))... Vsetko spravodlive je mravne. Vsetko mravne je dobre. Teda vsetko spravodlive je dobre.

Pricom:
^....konjunkcia
v....disjunkcia
~....negacia
=....eqvivalencia
>....implikacia
p,q,r,s,t,u,w....vyrokove premenne
V....vsetky
E....existuje
x,y,z....individuove premenne
a,b,c....individuove konstanty
P,Q,R,S....Predikaty

....

....

....

....

....

....

....

....

....

....

....

....

....

....