Recimo samo da smo ja i logika u svadji i to teskoj Profesor logike koristi prirodnu dedukciju i hilbertovski sistem kao metode dokazivanja da su formule teoreme. I sve posmatra kao planarna drveta. Moj problem je sto ga nista ne shvatam a imam oko mesec, mesec i po dana da ga spremim pa me sve vise hvata panika. Moj problem je sto on u toj njegovoj prirodnoj dedukciji radi zadatak bukvalno ni iz cega, ima kao sedam pravila iz kojih dokazuje da su formule teoreme. I sad on bira na neki meni ne razumljiv nacin formule koje ce mu biti u listovima drveta i onda ide do korena koje mu je formula koju treba dokazati.
Evo slike kako to radi (ne znam da li moze u lateksu to uopste da se predstavi):
[dispmath]\bigl(A\to\left(B\to C\right)\bigr)\to\bigl(\left(A\to B\right)\to\left(A\to C\right)\bigr)[/dispmath]
[dispmath]\left(2\right)\quad\frac{\displaystyle\frac{\left[A\to\left(B\to C\right)\right]_3\enspace\left[A\right]_1}{B\to C}\quad\frac{\left[A\to B\right]_2\enspace\left[A\right]_1}{B}}{\displaystyle\frac{\displaystyle\frac{\displaystyle\frac{\displaystyle C}{\displaystyle A\to C}\enspace1}{\displaystyle\left(A\to B\right)\to\left(A\to C\right)}\enspace2}{\displaystyle\bigl(A\to\left(B\to C\right)\bigr)\to\bigl(\left(A\to B\right)\to\left(A\to C\right)\bigr)}\enspace3}[/dispmath]
Da li ste se susretali sa ovim? Meni je od svega najteze sto ja ne znam kako da mu izabrem te formule koje su na vrhu.
Pravila izvodjenja su mu:
[dispmath]\frac{A\qquad B}{A\land B}\enspace\text{uvođenje konjunkcije}\qquad\qquad\frac{A\land B}{A}\qquad\frac{A\land B}{B}\enspace\text{eliminacija konjunkcije}[/dispmath]
[dispmath]\begin{array}{l}
\\
\displaystyle\frac{A}{A\lor B}\qquad\frac{B}{A\lor B}\enspace\text{uvođenje disjunkcije}
\end{array}\qquad\qquad\begin{array}{l}
\hspace{8ex}\left[A\right]_*\quad\left[B\right]_*\\
\displaystyle\frac{A\lor B\quad C\qquad C}{C}\;*\enspace\text{eliminacija disjunkcije}
\end{array}[/dispmath]
[dispmath]\begin{array}{ll}
\hspace{2ex}\left[A\right]_*\\
\displaystyle\frac{B}{A\to B}\;*\enspace\text{uvođenje implikacije}\qquad & \displaystyle\qquad\frac{A\to B\qquad A}{B}\enspace\text{eliminacija implikacije}\\
\\
& \qquad\hspace{1ex}\left[A\to\bot\right]_*\\
& \displaystyle\qquad\frac{\qquad\bot\qquad}{A}\;*\enspace\text{jako svođenje na apsurd}
\end{array}[/dispmath]