#LyX 1.3 created this file. For more info see http://www.lyx.org/ \lyxformat 221 \textclass article \begin_preamble \usepackage{color} \usepackage{html} \usepackage{fitch} \usepackage{ae} \pagecolor{white} \end_preamble \language esperanto \inputencoding auto \fontscheme default \graphics default \paperfontsize default \spacing single \papersize Default \paperpackage a4 \use_geometry 0 \use_amsmath 0 \use_natbib 0 \use_numerical_citations 0 \paperorientation portrait \secnumdepth 3 \tocdepth 3 \paragraph_separation indent \defskip medskip \quotes_language english \quotes_times 2 \papercolumns 1 \papersides 1 \paperpagestyle default \layout Title Enkonduko al natura dedukto \layout Author Daniel Clemente Laboreo \layout Date Aŭgusto 2004 (revuita en Majo 2005) \layout Standard \begin_inset LatexCommand \tableofcontents{} \end_inset \layout Section Antaŭ ĉio \layout Standard Ĉi tiu kurseto estas disponebla en pluraj lingvoj: \begin_inset ERT status Collapsed \layout Standard \backslash htmladdnormallinkfoot{hispana}{http://www.danielclemente.com/logica/dn.html} \backslash htmladdnormallink{(kaj PDF)}{http://www.danielclemente.com/logica/dn.pdf}, \backslash htmladdnormallinkfoot{esperanta}{http://www.danielclemente.com/logica/dn.eo.html} \backslash htmladdnormallink{(kaj PDF)}{http://www.danielclemente.com/logica/dn.eo.pdf}, \backslash htmladdnormallinkfoot{kataluna}{http://www.danielclemente.com/logica/dn.ca.html} \backslash htmladdnormallink{(kaj PDF)}{http://www.danielclemente.com/logica/dn.ca.pdf}, kaj \backslash htmladdnormallinkfoot{angla}{http://www.danielclemente.com/logica/dn.en.html} \backslash htmladdnormallink{(kaj PDF)}{http://www.danielclemente.com/logica/dn.en.pdf}. \layout Standard \layout Standard \end_inset \layout Standard Formuloj estos plej bele vidataj per la PDF, sed, se ne eblas uzi ĝin, legu la HTML paĝojn. \layout Subsection Kiu mi estas \layout Standard Mi nomas Daniel Clemente Laboreo, aĝas 19 jarojn (en 2004), loĝas en Gavà (Barcelona, Hispanio), kaj lernas komputikon ĉe la FIB (en la \emph on UPC \emph default , Publika Universitato de Katalunio). Tie, en la kurso \emph on ILO \emph default ( \emph on Enkonduko al logiko) \emph default , mi estis instruita ĉi tiun temon. \layout Subsection Kial mi verkas ĉi tion \layout Standard Jen pluraj kialoj: \layout Itemize Ekzistas grava manko en la serĉo \begin_inset Quotes eld \end_inset \emph on natura dedukto \emph default \begin_inset Quotes erd \end_inset ĉe Google. Mi mem bezonis lerni tion antaŭ la ekzameno sed trovis nenion utilan kio povus helpi min. Same per \emph on natural deduction \emph default aŭ \emph on nd \emph default : kvankam troviĝis kelkaj kursetoj, neniu estis sufiĉe bona: ĉu estis miskompren ebla, ĉu iaj specialaj literoj malmontriĝis, ĉu ĝi ne eldiris ĉion (kvazaŭ se iu ajn jam konus logikan rezonadon). Do mi celis aldoni ĉi tiun kurson, kiu eble helpos iun. \layout Itemize Estas temo ŝatata de mi, kaj facila laŭ mia opinio. \layout Itemize Devigas pensi. Eble ĝi ne havas utilegan uzeblecon, sed oni vere penu por solvi kelkajn simplajn, klopodindajn ekzercojn. \layout Itemize Nu, mi konfesas ke tio estis verkata por lerni skribi dokumentojn per \begin_inset ERT status Collapsed \layout Standard \backslash LaTeX \end_inset . Ties lernado ne estas facila, sed rezultoj igas la taskon farinda. \layout Itemize Krome, la Esperantan tradukon mi faris por praktiki la lingvon. Ĉi tiu estas mia unua verko, do bonvolu korekti min! Mi ankaŭ aldonis aranĝon de \begin_inset ERT status Collapsed \layout Standard \backslash htmladdnormallinkfoot{teknikaj vortoj pri logiko}{http://www.danielclemente.com/logica/vortoj.html} \end_inset kun la plej strangajn vortojn mi uzis. \layout Subsection Al kiu ĝi estas adresita \layout Standard Ĉefe, al iu kiu ŝatas logikon, komputikon, aŭ matematikon. Se vi volas antaŭstudi logikajn universitatajn lecionojn, vi ankaŭ gajnos utilajn konceptojn. \layout Standard Ĉi tio ne penas esti kompleta kurso pri natura dedukto, sed ĝi restos nur kiel enkonduko al la temo. Kiam mi plu lernos, mi korektos ĝin se necese, sed ne pligrandigos ĝin per aliaj sekcioj (mi skribus tiujn en apartaj dokumentoj). \layout Subsection Permesilo \layout Standard La tuta dokumento estas \begin_inset ERT status Collapsed \layout Standard \backslash htmladdnormallinkfoot{FDL}{http://www.gnu.org/licenses/fdl.html} \end_inset (kiel GPL ĉe libera programaro, sed por dokumentoj). La fontoteksto estas skribita per LyX ( \begin_inset ERT status Collapsed \layout Standard \backslash htmladdnormallinkfoot{dn.eo.lyx}{http://www.danielclemente.com/logica/dn.eo.lyx} \end_inset ), uzante la makroon \begin_inset ERT status Collapsed \layout Standard \backslash htmladdnormallink{fitch.sty}{http://www.danielclemente.com/logica/fitch.sty} \end_inset de Johan W. Klüwer. Mi ankaŭ uzis la programon \begin_inset ERT status Collapsed \layout Standard \backslash htmladdnormallink{latex2html}{http://www.danielclemente.com/linux/l2h.html} \end_inset (iomete modifitan) por krei la retpaĝon. \layout Standard Vi ja rajtas ŝanĝi tiun artikolon aŭ traduki ĝin al aliaj lingvoj parolataj bone de vi; ankaŭ redistribui aŭ vendi ĝin, kaj aliaj. \layout Section Bazaj konceptoj \layout Standard Ĉia logika afero bezonas klare difinitajn vortojn. Mi nur memorigos la signifon kaj la manieron legi la strangajn simbolojn uzatajn en ĉi tiu dokumento. \layout Subsection Formaligo \layout Standard \emph on Formaligi \emph default signifas skribi esprimon laŭ norma maniero, tiel ke iu ajn povas precize kompreni ĝin. \layout Standard Uzonte logikajn algoritmojn, oni povas pensadi per longaj frazoj kiel \begin_inset Quotes eld \end_inset \emph on Se pluvas kaj mi ne havas pluvombrelon, mi do malsekiĝos \emph default \begin_inset Quotes erd \end_inset . Eblas, ja, sed tio estas tro longa. Anstataŭe, estas pli bone esprimi ĉiun agon per unu litero, kaj uzi tiujn literojn kune de simplaj vortoj, nome \emph on kaj \emph default , \emph on aŭ \emph default , \emph on ne \emph default , aŭ \emph on do \emph default . \layout Standard Jen ekzemplo. Posedante ĉi tiun vortoprovizon: \layout Standard \begin_inset Formula $L$ \end_inset : \emph on pluvi \layout Standard \begin_inset Formula $P$ \end_inset : \emph on havi kun si pluvombrelon \layout Standard \begin_inset Formula $M$ \end_inset : \emph on malsekiĝi \layout Standard La frazon \begin_inset Quotes eld \end_inset \emph on Se pluvas kaj mi ne havas pluvombrelon, mi do malsekiĝos \emph default \begin_inset Quotes erd \end_inset oni povas skribi per \begin_inset Quotes eld \end_inset \emph on se \begin_inset Formula $L$ \end_inset kaj ne \begin_inset Formula $P$ \end_inset , do \begin_inset Formula $M$ \end_inset \emph default \begin_inset Quotes erd \end_inset . \layout Standard Ĉe natura dedukto, oni uzos nur la literan rimedon laŭ ĉi tiuj kondiĉoj: \layout Itemize Tiuj literoj (nomataj \emph on propoziciaj literoj \emph default ) estas majuskle. \layout Itemize Oni normale uzas literojn \begin_inset Formula $P$ \end_inset , \begin_inset Formula $Q$ \end_inset , \begin_inset Formula $R$ \end_inset , \begin_inset Formula $S$ \end_inset , ... kvankam iu ajn estas korekta. \layout Itemize Specialaj simboloj estas uzataj por la operatoroj \emph on kaj \emph default , \emph on aŭ \emph default , \emph on ne \emph default , kaj \emph on do \emph default . \layout Subsection Uzataj simboloj \layout Standard Por esprimi la rilaton inter unu ago kaj alia, ekzistas kelkaj internaciaj figuretoj. La bazajn operatorojn vi konu estas \begin_inset Formula $\vee$ \end_inset , \begin_inset Formula $\wedge$ \end_inset , \begin_inset Formula $\neg$ \end_inset , \begin_inset Formula $\Rightarrow$ \end_inset . La ceteraj estas pli kompleksaj, sed mi montris ilin ĉi tie por ebligi konsultojn (se necese). \layout Standard \begin_inset Tabular \begin_inset Text \layout Standard \series bold Simbolo \end_inset \begin_inset Text \layout Standard \series bold Legata... \end_inset \begin_inset Text \layout Standard \series bold Priskribo \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\vee$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on aŭ \end_inset \begin_inset Text \layout Standard \begin_inset Formula $A\vee B$ \end_inset pravas se unu el la du, aŭ ambaŭ, estas vera aserto. \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\wedge$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on kaj \end_inset \begin_inset Text \layout Standard Por ke \begin_inset Formula $A\wedge B$ \end_inset pravu, \begin_inset Formula $A$ \end_inset kaj \begin_inset Formula $B$ \end_inset estu ambaŭ pravaj. \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\neg$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on ne \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\neg A$ \end_inset nur pravas kiam \begin_inset Formula $A$ \end_inset estas falsa. \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\Rightarrow$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on entenas / do \end_inset \begin_inset Text \layout Standard Montras sekvon. La esprimo \begin_inset Formula $A\Rightarrow B$ \end_inset signifas ke kiam \begin_inset Formula $A$ \end_inset certas, \begin_inset Formula $B$ \end_inset ankaŭ certas. Krome, la implikacio \begin_inset Formula $A\Rightarrow B$ \end_inset estas prava escepte de la okazo \begin_inset Formula $A$ \end_inset vera kaj \begin_inset Formula $B$ \end_inset falsa. Por kompreni ĉi tion, pensu pri iu \begin_inset Formula $A$ \end_inset el kiu sekvas \begin_inset Formula $B$ \end_inset kaj demandiĝu: \emph on eblas ke \begin_inset Formula $A$ \end_inset pravas sed \begin_inset Formula $B$ \end_inset ne? \emph default Iel, malzorgu pri tio, ĉar ne estas necese kompreni tion nun. \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\Longleftrightarrow$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on se kaj nur se \end_inset \begin_inset Text \layout Standard \begin_inset Formula $A\Longleftrightarrow B$ \end_inset estas \begin_inset Formula $(A\Rightarrow B)\wedge(B\Rightarrow A)$ \end_inset . Signifas ke el \begin_inset Formula $A$ \end_inset oni povas dedukti \begin_inset Formula $B$ \end_inset kaj reciproke, do ili estas ekvivalentaj. \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\square$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on falso \end_inset \begin_inset Text \layout Standard Malplena kvadrateto prezentas \emph on falson \emph default (la duuma \emph on 0 \emph default ). Plej teknike, ĝi rilatas al \begin_inset Formula $\{\}$ \end_inset . \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\blacksquare$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on vero \end_inset \begin_inset Text \layout Standard Plena kvadrateto prezentas \emph on veron \emph default (la duuma \emph on 1 \emph default ). Plej teknike, ĝi rilatas al \begin_inset Formula $\{<>\}$ \end_inset . \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\exists$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on ekzistas... \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\exists xPx$ \end_inset estas legata \emph on ekzistas \begin_inset Formula $x$ \end_inset (ikso) tia ke \begin_inset Formula $P$ \end_inset de \begin_inset Formula $x$ \end_inset \emph default . Se ĉe nia domajno estas trovebla elemento tia ke propreco \begin_inset Formula $P$ \end_inset aplikata al tiu elemento certas, tiam la formulo estas vera. \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\forall$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on por ĉiu... \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\forall xPx$ \end_inset estas legata \emph on por ĉiu \begin_inset Formula $x$ \end_inset (ikso), \begin_inset Formula $P$ \end_inset de \begin_inset Formula $x$ \end_inset \emph default . Se ĉiuj elementoj ĉe nia tasko certigas proprecon \begin_inset Formula $P$ \end_inset , tiam formulo pravas. \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\vdash$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on tiam \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\vdash$ \end_inset simbolas \emph on deriveblon \emph default , kio estas la maniero diri \begin_inset Quotes eld \end_inset \emph on kiam ĉio el la maldekstra parto veras, tiam ankaŭ certas ĉio el la dekstra parto \emph default \begin_inset Quotes erd \end_inset . Ekzistas validaj derivoj, kia \begin_inset Formula $P\wedge Q\vdash P$ \end_inset aŭ kia \begin_inset Formula $P\Rightarrow Q,\ Q\Rightarrow R,\ P\vdash P\wedge R$ \end_inset . Ankaŭ estas nevalidaj, kia \begin_inset Formula $P\Rightarrow Q,\ \neg P\vdash\neg Q$ \end_inset . Natura dedukto penas aserti la validecon de derivo. \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\vDash$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on valida \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\phi\vDash\varphi$ \end_inset diras ke \begin_inset Formula $\varphi$ \end_inset estas logika sekvo de \begin_inset Formula $\phi$ \end_inset , do oni skribas per \begin_inset Formula $A\vDash B$ \end_inset la validecon de derivo \begin_inset Formula $A\vdash B$ \end_inset ; tio estas, oni iel pruvis ĝin, do ĝi estas akceptata kiel vera ĉe ia ajn interpreto de la predikatsimboloj. \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\nvDash$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on nevalida \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\phi\nvDash\varphi$ \end_inset signifas ke \begin_inset Formula $\varphi$ \end_inset ne estas logika sekvo de \begin_inset Formula $\phi$ \end_inset . Se oni trovas aron da valoroj ( \emph on modelon \emph default ) kiu certigas \begin_inset Formula $\phi$ \end_inset sed falsigas \begin_inset Formula $\varphi$ \end_inset , nevalideco estas pruvita. \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\Vdash$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on plenumebla \end_inset \begin_inset Text \layout Standard Aro da formuloj estas plenumebla (angle \emph on \begin_inset Quotes eld \end_inset satisfiable \emph default \begin_inset Quotes erd \end_inset ) se ekzistas aro da valoroj ( \emph on modelo \emph default ) kiu certigas la tutajn formulojn samtempe. \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\nVdash$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on malplenumebla \end_inset \begin_inset Text \layout Standard Aro da formuloj estas malplenumebla (angle \emph on \begin_inset Quotes eld \end_inset unsatisfiable \emph default \begin_inset Quotes erd \end_inset ) se nenia aranĝaĵo de valoroj ( \emph on modelo \emph default ) povas certigi la tutajn formulojn samtempe. \end_inset \end_inset \layout Subsection Prioritato de la operatoroj \layout Standard Vidante esprimon, vi devas kompreni kio ĝi estas. Ekzemple: \begin_inset Formula $A\vee B\Rightarrow C$ \end_inset estas implikacio (sed ne estas aŭo!), ĉar \begin_inset Formula $\Rightarrow$ \end_inset estas kalkulota laste (ĝi havas malpli prioritato ol la \begin_inset Formula $\vee$ \end_inset ). \layout Standard Jen la operatoroj, malkreske orditaj laŭ prioritato. \layout Itemize \begin_inset Formula $\Longleftrightarrow$ \end_inset \layout Itemize \begin_inset Formula $\Rightarrow$ \end_inset \layout Itemize \begin_inset Formula $\vee$ \end_inset kaj \begin_inset Formula $\wedge$ \end_inset (sama prioritato) \layout Itemize \begin_inset Formula $\neg$ \end_inset \layout Standard Ĉi tio signifas ke \begin_inset Formula $\neg$ \end_inset estas la plej \begin_inset Quotes eld \end_inset \emph on kunliganta \emph default \begin_inset Quotes erd \end_inset al la proksimaj simboloj. Jen ekzemplo pri kiam kaj kie metu krampojn: \layout Standard \begin_inset Formula $P\vee\neg Q\Rightarrow R\wedge P\Longleftrightarrow\neg(R\vee S)\wedge A\Rightarrow B$ \end_inset estas tute ekvivalenta al \begin_inset Formula $(\ (P\vee(\neg Q))\ \Rightarrow\ (R\wedge P)\ )\Longleftrightarrow(\ ((\neg(R\vee S))\wedge A)\Rightarrow B\ )$ \end_inset \layout Standard Trankvilu, mi ne plu uzos tiel longajn esprimojn. \layout Section Natura dedukto \layout Standard Nun oni devas lerni kio ĝi estas, kiel faru ĝin, kaj ties utilo (se ĝi ja havas). \layout Subsection Por kio ĝi utilas \layout Standard Natura dedukto utilas por pruvi la korektecon de rezonado, aŭ almenaŭ por provi tion. Laŭ la teorio, ĝi estas rimedo \begin_inset Quotes eld \end_inset \emph on por pruvi la validecon de derivo \emph default \begin_inset Quotes erd \end_inset . Jen ekzemplo: \layout Standard Mi diras al vi: \begin_inset Quotes eld \end_inset \emph on Ĉe somero estas varme, kaj nuntempe oni estas ĉe somero, do ja estas varme \emph default \begin_inset Quotes erd \end_inset . Vi komencas kalkuladon, kaj poste diras al mi: \begin_inset Quotes eld \end_inset \emph on Nu, mi ja povas pruvi ke via rezonado estas korekta \emph default \begin_inset Quotes erd \end_inset . Tiu estas la celo de natura dedukto. \layout Standard Ĉiam ne estos tiom facile: \begin_inset Quotes eld \end_inset \emph on se vi malaprobas lecionaron, vi devas ripeti ĝin. Se vi ne studas, vi malaprobos ĝin. Supozu ke vi ne ripetas ĝin. Do tiam, ĉu vi studas ĝin, ĉu vi malaprobas ĝin, ĉu ambaŭ samtempe \emph default \begin_inset Quotes erd \end_inset . Tiu rezonado estas valida kaj povas esti pruvata per natura dedukto. \layout Standard Rimarku ke vi eblas malkredi aŭ malkompreni ĉion kion mi rakontas. Ekzemple, mi asertas: \begin_inset Quotes eld \end_inset \emph on Transistoroj estas etaj kaj feliĉaj; kikero ne estas eta, do ĝi ne estas transistoro \emph default \begin_inset Quotes erd \end_inset . Eĉ se vi malsukcesas kompreni tiujn vortojn, aŭ se vi kredas ke tio estas sensence (ĝi ja estas), vi estu tute certa ke la rezonado estis korekta. \layout Standard Do, donite supozo kia \begin_inset Quotes eld \end_inset \emph on se ĉi tio okazas, tiam okazas ĉi tio alia \emph default \begin_inset Quotes erd \end_inset , natura dedukto eblas konkludi \begin_inset Quotes eld \end_inset \emph on jes, vi pravas \emph default \begin_inset Quotes erd \end_inset . Logike: donite derivo \begin_inset Formula $A\vdash B$ \end_inset , vi povas konkludi ke ĝi estas \begin_inset Formula $\vDash$ \end_inset ( \emph on valid \emph default a). Tiam oni skribas \begin_inset Formula $A\vDash B$ \end_inset ( \begin_inset Formula $A$ \end_inset sekvigas \begin_inset Formula $B$ \end_inset ). \layout Subsection Por kio ĝi malutilas \layout Standard Ĝi ne estas por pruvi la \emph on nevalidecon \emph default de iu supozo. Se mi asertas \begin_inset Quotes eld \end_inset \emph on se matene, ne estas nokte; nun estas matene, do estas ankaŭ nokte \emph default \begin_inset Quotes erd \end_inset vi eble provados longtempe la regulojn de natura dedukto, sed renkontos nenian utilaĵon. Plej eble vi intuos ke la rezonado ne estas valida, kaj nur tiam, oni devos provi aliajn rimedojn -ne natura dedukto- por celi pruvi nevalidecon. Kelkaj el ili estas klarigotaj poste. \layout Standard Do, natura dedukto nur utilas por pruvi validecon, sed ne nevalidecon. Bedaŭrinde, ĉu ne? \layout Standard Nek ĝi estas rimedo por solvi la demandon \begin_inset Quotes eld \end_inset \emph on Kio okazus se...? \emph default \begin_inset Quotes erd \end_inset . Kiam la valideco de \begin_inset Formula $A\vdash B$ \end_inset estu pruvata, oni devas pensi pri ĉio kio okazus se \begin_inset Formula $A$ \end_inset certus, kaj se oni eltrovas ke unu el tiuj aĵoj estas \begin_inset Formula $B$ \end_inset , oni jam finis. Tamen, estas neeble doni finotan liston kun ĉiuj el ili. \layout Subsection Agmaniero \layout Standard Oni estas demandita pruvi la validecon de \begin_inset Formula $\Gamma\vdash S$ \end_inset , kie \begin_inset Formula $\Gamma$ \end_inset (legata \emph on gamma \emph default ) estas aro da formuloj disrompitaj per komoj, kaj \begin_inset Formula $S$ \end_inset estas simpla formulo. \layout Standard Komencante, oni akceptos ĉiujn formulojn el \begin_inset Formula $\Gamma$ \end_inset kiel certaj, kaj, per 9 precizaj reguloj, eltrovos kiuj aliaj aĵoj estas ankaŭ certaj. Nia intenco estas trovi ke \begin_inset Formula $S$ \end_inset ja certas; do ĉi tio ĵus atingite, oni haltiĝos. \layout Standard Iam estos trovebla neniun veraĵon, do oni supozados: \begin_inset Quotes eld \end_inset \emph on nu, mi ne scias se \begin_inset Formula $A\wedge B$ \end_inset ĉiam estas certa, sed se \begin_inset Formula $C$ \end_inset certas, tiam ĝi estas vera sendube \emph default \begin_inset Quotes erd \end_inset . Tiel oni ektrovis iun novan veraĵon: \begin_inset Formula $C\Rightarrow A\wedge B$ \end_inset . \layout Standard Kompreneble, oni ĉiam devas memori kion oni volas atingi, ĉar alie, oni divenus multajn veraĵojn kiuj ja estas veraj, sed estus tute malbezonataj por la nuna ekzerco. Ekzemple, por \begin_inset Formula $A\vee B,\ \neg A\vdash B$ \end_inset oni devas atingi la verecon de \begin_inset Formula $B$ \end_inset . Eble ni eltrovos ke \begin_inset Formula $\neg(A\wedge B)$ \end_inset , \begin_inset Formula $A\vee B\vee C$ \end_inset , \begin_inset Formula $(A\vee B)\Rightarrow\neg A$ \end_inset , kaj tiel plu; sed ni nur bezonas \begin_inset Formula $B$ \end_inset , ne aliaj. Do, se vi devojiĝas de la simpla solvo, vi eble konfuziĝos. \layout Subsection Notacio \layout Standard Eblas diversaj manieroj por skribi naturdeduktajn skemojn. Mi uzos la stilon Fitch, pro esti kiun mi estis instruita, esti facile komprenebla, kaj necesigi malgrandan spacon. Ĝi estas tiel: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard P \backslash Rightarrow Q \backslash \backslash \layout Standard Q \backslash Rightarrow R \backslash \backslash \layout Standard \backslash fh P & H \backslash \backslash \layout Standard \backslash fa Q & E$ \backslash Rightarrow$ 1,3 \backslash \backslash \layout Standard \backslash fa R & E$ \backslash Rightarrow$ 2,4 \backslash \backslash \layout Standard \backslash fa Q \backslash wedge R & I$ \backslash wedge$ 4,5 \backslash \backslash \layout Standard P \backslash Rightarrow Q \backslash wedge R & I$ \backslash Rightarrow$ 3,6 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Standard Ĉi tio pruvas validecon de \begin_inset Formula $P\Rightarrow Q,\ Q\Rightarrow R\vdash P\Rightarrow Q\wedge R$ \end_inset . \layout Standard La skemon oni legas linion post linio, de supre al sube. La maldekstrajn numerojn montras la numeron de ĉiu linio, kaj ĉiam estas laŭorde. \layout Standard La linioj plej supre enhavas ĉiun el la formuloj kiuj troviĝas en la maldekstra parto de la derivo. Nun oni havas du: \begin_inset Formula $P\Rightarrow Q$ \end_inset kaj \begin_inset Formula $Q\Rightarrow R$ \end_inset . De tiuj oni devos konkludi \begin_inset Formula $P\Rightarrow Q\wedge R$ \end_inset . \layout Standard En ĉiu linio estas notata kion aĵon oni trovis certa, kaj dekstre oni klarigas kiel ĝi estas trovita. Tiuj simboloj dekstraj estas mallongigoj de nomoj el la 9 reguloj: \begin_inset Formula $E$ \end_inset estas pro la angla \begin_inset Quotes eld \end_inset \emph on elimination \emph default \begin_inset Quotes erd \end_inset kaj \begin_inset Formula $I$ \end_inset pro \begin_inset Quotes eld \end_inset \emph on introduction \emph default \begin_inset Quotes erd \end_inset (mi konservas tian notacion, komuna por plej lingvoj). En Esperanto, oni povas uzi \begin_inset Quotes eld \end_inset \emph on forigo \emph default \begin_inset Quotes erd \end_inset kaj \begin_inset Quotes eld \end_inset \emph on enigo \emph default \begin_inset Quotes erd \end_inset , aŭ prefiksojn \begin_inset Quotes eld \end_inset \emph on el- \emph default \begin_inset Quotes erd \end_inset kaj \begin_inset Quotes eld \end_inset \emph on kun- \emph default \begin_inset Quotes erd \end_inset (mi sekve klarigos tion). \layout Standard Ekzemple, kelkajn regulojn oni vidas tie estas \emph on elimplikaciigo \emph default ( \begin_inset Formula $E\Rightarrow$ \end_inset ), \emph on kunkajigo \emph default ( \begin_inset Formula $I\wedge$ \end_inset ), kaj \emph on kunimplikaciigo \emph default ( \begin_inset Formula $I\Rightarrow$ \end_inset ). Komprenu la vortojn: \emph on el-kaj-ig-o \emph default estas \emph on forigo de konjunkcio \emph default ( \emph on kaj-o \emph default ), \emph on kun-aŭ-ig-o \emph default estas \emph on enigo de disjunkcio \emph default ( \emph on aŭ-o \emph default ), \emph on el-neg-ig-o \emph default estas \emph on forigo de negacio \emph default ( \emph on neg-o \emph default ), ktp. La nomoj de la 9 derivreguloj estas do \emph on kunkajigo \emph default , \emph on elkajigo \emph default , \emph on kunaŭigo \emph default , \emph on elaŭigo \emph default , \emph on kunimplikaciigo \emph default , \emph on elimplikaciigo \emph default , \emph on kunnegigo \emph default , \emph on elnegigo \emph default , \emph on iteracio \emph default . Vi ankaŭ povas legi ilin longe, kvazaŭ la angla ( \begin_inset Quotes eld \end_inset \emph on implication elimination \emph default \begin_inset Quotes erd \end_inset , \begin_inset Quotes eld \end_inset \emph on disjunction introduction \emph default \begin_inset Quotes erd \end_inset , ktp.). \layout Standard La numeroj kunigantaj la nomojn de ĉiu regulo klarigas la loko el kie oni prenis la necesajn formulojn por apliki tiun regulon. Ili estas liniajn numerojn, do, por apliki regulon oni devas nur uzi informon el la jam verkitaj supraj linioj. \layout Standard Fine, tiu vertikala linieto kiu trairas de linio 3 al la 6 estas hipotezo (tial oni skribis \begin_inset Formula $H$ \end_inset dekstre). Ĉio kio estas enmetita tie ne estas ĉiam certa, sed nur kiam certas \begin_inset Formula $P$ \end_inset (la komenco de la hipotezo, ĉe linio 3). Tial, formuloj trovitaj ĉe la hipotezo oni ne uzu ekstere, ĉar ili ne estas ĉiam pravaj. \layout Standard La procedo finiĝas kiam oni eltrovas ke estas prava la formulo verkita dekstre de la derivsimbolo, jen \begin_inset Formula $P\Rightarrow Q\wedge R$ \end_inset (tio aperas ĉe la lasta linio). \layout Section La derivreguloj \layout Standard Jen estas esprimitaj kaj klarigitaj la naŭ bazaj reguloj kiujn oni uzas ĉe natura dedukto. Ilia celo estas montri kiam kaj kiel oni aldonu pli da certaj formuloj. \layout Standard Vi trovos ekzemplojn (eksplikitajn) ĉe la sekva sekcio. \layout Subsection Iteracio \layout Standard Tiu estas tre simpla regulo: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch*} \layout Standard n & A \backslash \backslash \layout Standard \backslash hline \layout Standard & A & IT n \layout Standard \backslash end{fitch*} \backslash ] \end_inset \layout Standard Nu, tiel verkite estas iom konfuza, sed ĉi tio estas ĝia formala difino, do estas la plej utila maniero skribi la regulon. Supra formulaĵo signifas ke se en linio numero \begin_inset Formula $n$ \end_inset estas verkata \begin_inset Formula $A$ \end_inset (ia ajn esprimo) tiam oni povas reskribi \begin_inset Formula $A$ \end_inset en la nuna linio, klarigante tiun aldonon per la noto \begin_inset Formula $IT\ n$ \end_inset verkita dekstre. \layout Standard Do kial oni volus tion? Ĝis la momento, por nenion, tamen, tio havos sian utilecon poste, kiam oni komencos uzi hipotezojn. Ĉar hipotezo estas \emph on ferma \emph default (malebligas eniron aŭ eliron de formuloj), ĉiuj reguloj devos uzi formulojn el ĉe la hipotezo. Se nia ŝatita formulo estas tuj ekstere de tiu hipotezo, oni povas enmeti ĝin uzante la \emph on iteracion \emph default . \layout Standard Iuj kredas ke ne estas necese elspezi linion tiel, sed ĝia uzado multe klarigas la skemojn. Sed io malpermesita estas uzi ĝin nur por \begin_inset Quotes eld \end_inset \emph on alproksimigi \emph default \begin_inset Quotes erd \end_inset formulon kiu estas kelkajn liniojn supre: estas malnecese reskribi linion kiu jam estas skribita supre en la nuna derivo. \layout Subsection Kunkajigo \layout Standard La kajon (aŭ konjunkcion) oni povas facile krei: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch*} \layout Standard m & A \backslash \backslash \layout Standard n & B \backslash \backslash \layout Standard \backslash hline \layout Standard & A \backslash wedge B & I$ \backslash wedge$ m,n \layout Standard \backslash end{fitch*} \backslash ] \end_inset \layout Standard Bone komprenu la funkciadon de figuroj kiel la supra. Kiam oni pentras longan horizontalan linion, normale ĝi estas por disigi la \emph on premisojn \emph default (supre) de la \emph on konkludo \emph default (malsupre). Premisoj estas kondiĉoj kiuj devas certiĝi por apliko de la regulo, kaj konkludo estas rezulto de tiu apliko. \layout Standard Tiu regulo diras ke se en linio veraĵo estas skribita, kaj en alia linio estas alia veraĵo, tiam oni povas skribi per nur unu linio ke ambaŭ aĵoj estas veraj. Oni devos noti dekstre la liniojn el kiu oni eltiris la unuan kaj la duan formulojn. \layout Standard Tio estas plej logike, ĉu ne? Se oni scias ke (vere) \emph on pluvas \emph default , kaj (tiel vere) \emph on estas sune \emph default , tiam sendube oni povas diri ke \emph on pluvas kaj estas sune \emph default (samtempe). Se io ŝajnas stranga, ne estas pro nia lerta rezonado; kulpigu al kiu asertis al ni ke \emph on pluvas \emph default aŭ \emph on estas sune \emph default . \layout Standard Rimarku ke prenante la liniojn turnite, oni povas atingi \begin_inset Formula $B\wedge A$ \end_inset , kaj prenante la saman linion eblas \begin_inset Formula $A\wedge A$ \end_inset kaj \begin_inset Formula $B\wedge B$ \end_inset , kiuj ankaŭ estas pravaj. \layout Subsection Elkajigo \layout Standard Tio estas operacio kontraŭa al la lasta. Ĝi havas du partojn. Unue: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch*} \layout Standard n & A \backslash wedge B \backslash \backslash \layout Standard \backslash hline \layout Standard & A & E$ \backslash wedge$ n \layout Standard \backslash end{fitch*} \backslash ] \end_inset \layout Standard Kaj la dua, por akiri \begin_inset Formula $B$ \end_inset : \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch*} \layout Standard n & A \backslash wedge B \backslash \backslash \layout Standard \backslash hline \layout Standard & B & E$ \backslash wedge$ n \layout Standard \backslash end{fitch*} \backslash ] \end_inset \layout Standard Do, oni povas disigi laŭ pluraj linioj la konjunkcierojn el konjunkcio. Tial, oni nomas tiun regulon \emph on forigo de la konjunkcio \emph default (aŭ \emph on elkajigo \emph default ): el linio kiu havas kaj-simboloj ( \begin_inset Formula $\wedge$ \end_inset ) oni atingas aliajn kiuj jam ne havas ilin; kompreneble, penante alproksimiĝi al nia celo (atingi iun formulon). \layout Subsection Kunimplikaciigo \layout Standard Tiu estas pli interesa, ĉar ĝi eblas uzi utile hipotezojn (tiujn subderivojn kiuj havas vertikalan linion maldekstre). Jen ĝi estas: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch*} \layout Standard m & \backslash fh A & H \backslash \backslash \layout Standard n & \backslash fa B \backslash \backslash \layout Standard \backslash hline \layout Standard & A \backslash Rightarrow B & I$ \backslash Rightarrow$ m,n \layout Standard \backslash end{fitch*} \backslash ] \end_inset \layout Standard Kion ĝi signifas estas ke se oni skribis ion (ĝin nomiĝu \begin_inset Formula $A$ \end_inset ), kaj poste eltrovis (per la derivreguloj) ke supozinte \begin_inset Formula $A$ \end_inset certigas \begin_inset Formula $B$ \end_inset (io ajn), tiam oni povas klare aldiri ion: ne eblas aserti ke \begin_inset Formula $B$ \end_inset estas ĉiam prava, sed jes ke \begin_inset Formula $A$ \end_inset entenas \begin_inset Formula $B$ \end_inset , kio estas skribita \begin_inset Formula $A\Rightarrow B$ \end_inset . \layout Standard Tio ebligas nin finigi subderivon kaj daŭrigi nian lastan taskon. Memoru ke natura dedukto ne devas esti haltita ĉe subderivo. \layout Subsection Elimplikaciigo \layout Standard Pli simpla ol la lasta ĉar ĝi ne temas pri supozoj sed pri faktoj: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch*} \layout Standard m & A \backslash Rightarrow B \backslash \backslash \layout Standard n & A \backslash \backslash \layout Standard \backslash hline \layout Standard & B & E$ \backslash Rightarrow$ m,n \layout Standard \backslash end{fitch*} \backslash ] \end_inset \layout Standard Simple, se oni estas dirita ke kiam okazas \begin_inset Formula $A$ \end_inset ankaŭ okazas \begin_inset Formula $B$ \end_inset (tio estas la signifo de \begin_inset Formula $A\Rightarrow B$ \end_inset ), kaj oni ankaŭ scias ke \begin_inset Formula $A$ \end_inset , do oni povas aserti ke \begin_inset Formula $B$ \end_inset . \layout Standard Tiu regulo estas ankaŭ nomata \emph on modus ponens \emph default . \layout Subsection Kunaŭigo \layout Standard La disjunkcio (la aŭo) estas tre facila sed ne memvidebla: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch*} \layout Standard n & A \backslash \backslash \layout Standard \backslash hline \layout Standard & A \backslash vee B & I$ \backslash vee$ n \layout Standard \backslash end{fitch*} \backslash ] \end_inset \layout Standard Nu, plej precize, mi diru ke ankaŭ ekzistas laŭ la alia ordo: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch*} \layout Standard n & A \backslash \backslash \layout Standard \backslash hline \layout Standard & B \backslash vee A & I$ \backslash vee$ n \layout Standard \backslash end{fitch*} \backslash ] \end_inset \layout Standard Mirinda, ĉu ne? Se oni scias ke \begin_inset Quotes eld \end_inset \emph on hodiaŭ estas ĵaŭdo \emph default \begin_inset Quotes erd \end_inset oni ankaŭ scias ke \begin_inset Quotes eld \end_inset \emph on hodiaŭ estas ĵaŭdo aŭ bovinoj flugas \emph default \begin_inset Quotes erd \end_inset , \begin_inset Quotes eld \end_inset \emph on hodiaŭ estas ĵaŭdo aŭ vendredo \emph default \begin_inset Quotes erd \end_inset , eĉ \begin_inset Quotes eld \end_inset \emph on hodiaŭ estas ĵaŭdo... aŭ ne \emph default \begin_inset Quotes erd \end_inset . Ĉiuj estas certaj. \layout Standard Memoru ke, parole, oni emas uzi \emph on ekskludan aŭon \emph default ( \emph on disaŭo \emph default , kaj \emph on XOR \emph default en la angla), kiu certas se unu el la disjunkcieroj estas vera sed ne kiam ambaŭ el ili estas veraj samtempe. Por logikisto, komuna frazo \begin_inset Quotes eld \end_inset \emph on hodiaŭ estas ĵaŭdo aŭ vendredo \emph default \begin_inset Quotes erd \end_inset certiĝas ĉe tri malsamaj okazoj: kiam \emph on hodiaŭ estas ĵaŭdo \emph default , kiam \emph on hodiaŭ estas vendredo \emph default , kaj kiam \emph on hodiaŭ estas ĵaŭdo kaj vendredo samtempe \emph default (iom malfacile ĉe la reala mondo, tamen, matematikistoj estas emaj supozi ion ajn...). \layout Subsection Elaŭigo \layout Standard Tiu estas la plej malfacila regulo, precipe ĉar donite de frazo kun \emph on aŭ \emph default , kiel \begin_inset Quotes eld \end_inset \emph on hodiaŭ estas ĵaŭdo aŭ vendredo \emph default \begin_inset Quotes erd \end_inset , kion do oni povas eltiri? Ĉu ke \emph on hodiaŭ estas ĵaŭdo \emph default ? Ne, eble estas vendredo. Ĉu ke \emph on hodiaŭ estas vendredo \emph default ? Ne, eble estas ĵaŭdo. Ĉu ke \emph on hodiaŭ estas ĵaŭdo aŭ vendredo \emph default ? Nu, jes, sed oni jam sciis tion... \layout Standard Jen la regulo (nun mi klarigos ĝin): \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch*} \layout Standard m & A \backslash vee B \backslash \backslash \layout Standard & \backslash fh A & H \backslash \backslash \layout Standard n & \backslash fa C \backslash \backslash \layout Standard & \backslash fh B & H \backslash \backslash \layout Standard p & \backslash fa C \backslash \backslash \layout Standard \backslash hline \layout Standard & C & E$ \backslash vee$ m,n,p \layout Standard \backslash end{fitch*} \backslash ] \end_inset \layout Standard Oni bezonas pli da informon, krome de \begin_inset Formula $A\vee B$ \end_inset . Se, bonŝance, oni scias ke \begin_inset Formula $A\Rightarrow C$ \end_inset , kaj ankaŭ \begin_inset Formula $B\Rightarrow C$ \end_inset , tio do eblas ja scii kio okazos kiam \begin_inset Formula $A\vee B$ \end_inset : ambaŭ unu elekto kaj la alia sekvigas \begin_inset Formula $C$ \end_inset , do \begin_inset Formula $C$ \end_inset estas prava. \layout Standard Tia okazo estas nur ebla en ekzercoj preparitaj por ke tiu \emph on forigo de disjunkcio \emph default aperu, aŭ kiam \begin_inset Formula $A$ \end_inset kaj \begin_inset Formula $B$ \end_inset multe similas (tiam, oni facile trovos ian \begin_inset Formula $C$ \end_inset tia ke ambaŭ entenu ĝin). \layout Standard Ekzemple: kiam mi kontraktis atingon al la Interreto per ADSL, tio estis per \emph on Telefónica \emph default aŭ \emph on Terra \emph default , sed mi tute ne certas pri kiu el ili aldonis al mi la servon (eĉ ili ne sciis). Sed ĉe mia lando (Hispanio), ĉiu elekto estis malrapida, multekosta, kaj plena da problemoj (nomu \begin_inset Formula $M$ \end_inset al tiuj malbonaĵoj), do, iu ajn kompanio estis \begin_inset Formula $M$ \end_inset . Konkrete, \begin_inset Formula $Telefonica\Rightarrow M$ \end_inset kaj \begin_inset Formula $Terra\Rightarrow M$ \end_inset , do sendube kvalito de mia ret-atingo estas klara: ĝi estis ankaŭ \begin_inset Formula $M$ \end_inset , sendepende de kiun el la du kompanioj mi uzis. Fakte, mi bezonis 9 monatoj por plene kontrakti la servon... Bonsorte ĉi tio okazis nur multaj jaroj antaŭ nune. \layout Standard Tiu regulo estas konata per \emph on provo per okazoj \emph default , ĉar oni devas provi ĉiun el la eblaj okazoj por certiĝi ke ĉiuj kondukas al sama konkludo. \layout Subsection Kunnegigo \layout Standard Ĉi tiu estas belega kaj interesa: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch*} \layout Standard m & \backslash fh A & H \backslash \backslash \layout Standard n & \backslash fa B \backslash \backslash \layout Standard p & \backslash fa \backslash neg B \backslash \backslash \layout Standard \backslash hline \layout Standard & \backslash neg A & I$ \backslash neg$ m,n,p \layout Standard \backslash end{fitch*} \backslash ] \end_inset \layout Standard Se supozinte \begin_inset Formula $A$ \end_inset , vi atingis la konkludon ke ambaŭ \begin_inset Formula $B$ \end_inset kaj \begin_inset Formula $\neg B$ \end_inset certiĝas samtempe, tio ankoraŭ ne estas fuŝita, ĉar vi ĵus ektrovis alian veraĵon: ke ne eblas ke \begin_inset Formula $A$ \end_inset certu, do, ke \begin_inset Formula $\neg A$ \end_inset certas. \layout Standard Ekzemple, mi konfesas ke \emph on se mi uzas Vindozon (Windows), mi ne profitas la tempon kiam mi uzas komputilon \emph default . Ekde kelkaj jaroj antaŭe, \emph on mi ja profitas ĝin \emph default , do la konkludo estas ke \emph on mi ne uzas Vindozon \emph default . Por atingi tiun konkludon, la vojon vi sekvus (eble senpense) estas precize kiun tiu regulo necesas: supozu ke \emph on mi ja uzas Vindozon \emph default , tiaokaze \emph on mi ne profitus mian komputilon \emph default . Tamen, mi diris ke \emph on mi ja profitas ĝin \emph default , do tiu supozo estu erara. \layout Standard Al tiu procedo oni nomas \emph on redukto al absurdo \emph default ( \emph on reductio ad absurdum \emph default ): supozi ion por atingi memkontraŭdiron kaj ebligi aserti ke tio supozita estas falsa. Tre utila se oni komencas supozante \emph on tion kontraŭan \emph default al kion oni volas pruvi: se oni atingas memkontraŭdiron, preskaŭ ĉio estas jam farita. \layout Standard Mi devas averti ke ĉi tio estas \emph on notacio trouzo \emph default : por ke logikaj teoremoj estu tute certaj, ĉiu subderivo devas sekvigi \emph on unu \emph default konkludon (ne du); kaj en la hipotezo ĉe la supra derivregulo, oni ne tute scias kiu estas la konkludo (ĉu \begin_inset Formula $B$ \end_inset aŭ ĉu \begin_inset Formula $\neg B$ \end_inset ?). La plej bona maniero skribi tion estus uzu \emph on kunkajigon \emph default por diri \begin_inset Formula $B\wedge\neg B$ \end_inset , kaj ĉi tiu estas la konkludo kiu montras la malverecon de la originala hipotezo. Sed miaj instruistoj evitigis tiun linion. \layout Subsection Elnegigo \layout Standard Tiu estas tre simpla, sed ĝin oni devas ankaŭ koni: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch*} \layout Standard n & \backslash neg \backslash neg A \backslash \backslash \layout Standard \backslash hline \layout Standard & A & E$ \backslash neg$ n \layout Standard \backslash end{fitch*} \backslash ] \end_inset \layout Standard Do, kiam oni vidas la negon de la nego de io, ni rajtas forigi tiujn du sinsekvajn negaciojn. \layout Standard Memoru ke la negacio de \begin_inset Quotes eld \end_inset \emph on ĉi tio estas blanka \emph default \begin_inset Quotes erd \end_inset ne estas \begin_inset Quotes eld \end_inset \emph on ĉi tio estas nigra \emph default \begin_inset Quotes erd \end_inset sed \begin_inset Quotes eld \end_inset \emph on ĉi tio ne estas blanka \emph default \begin_inset Quotes erd \end_inset . \layout Subsection Ne plu reguloj \layout Standard Ĝis tie ĉi la bazaj derivreguloj. Aliaj ekzistas por pli kompleksaj aferoj (temas pri \emph on kvantoroj \emph default kaj du pri \emph on vero \emph default kaj \emph on falso \emph default , kiujn mi klarigos poste), sed ĉi tiuj naŭ estas sufiĉaj por provi pruvi la validecon de iu ajn derivo en tiu dokumento (escepte tiuj pri kvantoroj...). \layout Standard Rememoru ke ne plu reguloj estas bezonataj: oni ne povas ŝanĝi de \begin_inset Formula $A\vee\neg A$ \end_inset al \begin_inset Formula $\blacksquare$ \end_inset ( \emph on vero \emph default ) direkte, nek de \begin_inset Formula $\neg(A\vee B)$ \end_inset al \begin_inset Formula $\neg A\wedge\neg B$ \end_inset , nek uzi asocian, distributan aŭ komutan regulon. Oni devas agi paŝon post paŝo; nek eĉ la simplaj ŝanĝoj estas permesataj (dume). Kial? Ĉar plej eble ili ne estas tiom simplaj kiom vi kredas: oni komprenos tion kiam estos pruvenda ke \begin_inset Formula $A\vee\neg A$ \end_inset estas ĉiam vera... (ĉe la sekva sekcio). \layout Section Klarigitaj ekzercoj \layout Standard Jen ekzercoj el pluraj niveloj, klarigitaj iom post iom. Se vi volas eĉ plu ekzemplojn (sed ne komentitajn), vidu la lastan sekcion. Kion mi penas rakonti ne estas la reguloj, sed la maniero pensi por ke oni divenos la magian ideon kiu solvas problemon. \layout Standard Ĉi tio estas kion mi plej bedaŭris kiam mi devis lerni naturan dedukton. \layout Subsection Iu tre simpla. \begin_inset Formula $P,\ P\Rightarrow Q\vdash P\wedge Q$ \end_inset \layout Standard La solvo al \begin_inset Formula $P,\ P\Rightarrow Q\vdash P\wedge Q$ \end_inset estas: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard P \backslash \backslash \layout Standard P \backslash Rightarrow Q \backslash \backslash \layout Standard Q & E$ \backslash Rightarrow$ 2,1 \backslash \backslash \layout Standard P \backslash wedge Q & I$ \backslash wedge$ 1,3 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Standard Jen oni ne devas tro pensadi, nur devas bone uzi la regulojn kaj iliajn klarigojn. \layout Standard Unue, komprenu kion ni estis demandita: oni diras ke nun okazas \emph on du \emph default aĵojn, la unua estas \begin_inset Formula $P$ \end_inset kaj la dua \begin_inset Formula $P\Rightarrow Q$ \end_inset (ili estas la du formulojn verkitajn maldekstre de la simbolo \begin_inset Formula $\vdash$ \end_inset ). Ĉi tiujn oni devas noti, unu po linio, ĉar ĉe tiu derivo, ili estos ĉiam certaj (tion ŝatante aŭ ne). \layout Standard La celo de tiu derivo estas sciiĝi ke \begin_inset Formula $P\wedge Q$ \end_inset ankaŭ certas, ĉar oni aldiris ke kiam \begin_inset Formula $P$ \end_inset kaj \begin_inset Formula $P\Rightarrow Q$ \end_inset estas certaj, tiam \begin_inset Formula $P\wedge Q$ \end_inset ankaŭ estas vera, kaj ni volas pruvi ke tio estas prava. Videble, oni fine atingis tion, ĉar en la lasta linio estas verkita formulo \begin_inset Formula $P\wedge Q$ \end_inset . \layout Standard Nu, kiel ni sekvos? Oni devas ekscii al kie oni volas aliri. Se \begin_inset Formula $P\wedge Q$ \end_inset devas certi, tiam ambaŭ \begin_inset Formula $P$ \end_inset kaj \begin_inset Formula $Q$ \end_inset devos certi; do oni okupu por pruvi ke ili ja certas. \layout Standard \begin_inset Formula $P$ \end_inset certas, ĉar estas fakto dirite al ni komence; ĝi estas skribita en linio 1. \layout Standard Sed neniu diris al ni ke \begin_inset Formula $Q$ \end_inset ankaŭ certu. Kion oni diris pri \begin_inset Formula $Q$ \end_inset ? Serĉinte ĝin en linioj 1 kaj 2, oni nur konas ke \begin_inset Formula $Q$ \end_inset certas kiam \begin_inset Formula $P$ \end_inset okazas (tion diras la linio 2). Sed \begin_inset Formula $P$ \end_inset ja estas vera, do oni povas uzi unu el la reguloj por dedukti \begin_inset Formula $Q$ \end_inset el \begin_inset Formula $P\Rightarrow Q$ \end_inset kaj \begin_inset Formula $P$ \end_inset . Rimarku la plej gravan ŝanĝon ĉe la transformo de \begin_inset Formula $P\Rightarrow Q$ \end_inset al \begin_inset Formula $Q$ \end_inset : ĉe la dua formulo, implikacion simbolon oni ne jam uzis; do regulo kiun oni bezonas estas la nomata \emph on forigo de implikacio \emph default , aŭ \emph on elimplikaciigo \emph default . \layout Standard Por uzi tiun derivregulon, oni konsultas ĝian difinon, kaj eltrovas ke en novan linion oni devas meti la \begin_inset Formula $Q$ \end_inset , kaj kiel klarigo \begin_inset Formula $E\Rightarrow\ 2,1$ \end_inset estu skribita dekstre. La \begin_inset Formula $E$ \end_inset estas pro la angla \emph on elimination \emph default (aŭ la esperanta \emph on el- \emph default ), la \begin_inset Formula $\Rightarrow$ \end_inset estas pro \emph on implikacio \emph default , la unua numero estas tiu el la linio kiu enhavas implikacion ( \begin_inset Formula $P\Rightarrow Q$ \end_inset ), kaj la dua numero, el la linio kiu diras la konatan veraĵon ( \begin_inset Formula $P$ \end_inset ). Estus malkorekte metu ilin turnite ( \begin_inset Formula $E\Rightarrow\ 1,2$ \end_inset ), ĉar la difino de la regulo esprimas ke linio kiu havas la implikacion estu citita unue. \layout Standard Jam aplikite la regulon, oni scias tri veraĵojn: ke \begin_inset Formula $P$ \end_inset , ke \begin_inset Formula $P\Rightarrow Q$ \end_inset , kaj ke \begin_inset Formula $Q$ \end_inset . Ĉiuj estas same certaj. Nun ni estas pli proksime al nia celo, \begin_inset Formula $P\wedge Q$ \end_inset , ĉar ni ja scias ke \begin_inset Formula $P$ \end_inset kaj \begin_inset Formula $Q$ \end_inset estas veraĵoj, do \begin_inset Formula $P\wedge Q$ \end_inset ankaŭ devas esti (memvideble). Ĉe la formulo ni serĉadas estas signo de konjunkcio ( \begin_inset Formula $\wedge$ \end_inset ) kiun oni mankas, do uzu \emph on kunkajigon \emph default (longe nomata \emph on enigo de konjunkcio \emph default ) por ebligi aserti ke \begin_inset Formula $P\wedge Q$ \end_inset pravas ĉar \begin_inset Formula $P$ \end_inset certas kaj \begin_inset Formula $Q$ \end_inset same. Kiel klarigo oni metas \begin_inset Formula $I\wedge\ 1,3$ \end_inset (linio kiu diras ke \begin_inset Formula $P$ \end_inset , kaj tiu kiu diras ke \begin_inset Formula $Q$ \end_inset ). Ne eblas meti \begin_inset Formula $I\wedge\ 3,1$ \end_inset ; tio estus por aserti \begin_inset Formula $Q\wedge P$ \end_inset , kio ne estas nia pruvenda formulo. \layout Standard Tiam jam scias 4 certajn aĵojn: \begin_inset Formula $P$ \end_inset , \begin_inset Formula $P\Rightarrow Q$ \end_inset , \begin_inset Formula $Q$ \end_inset , kaj \begin_inset Formula $P\wedge Q$ \end_inset . Eblas daŭrigi nian eltrovadon de veraĵoj, sed ni jam finiĝis, ĉar oni demandis al ni pruvi la verecon de \begin_inset Formula $P\wedge Q$ \end_inset , kaj oni jam atingis ĝin (ĉe linio 4). Do, tiu estos la lasta linio, kaj oni ne devas plu skribi. \layout Standard Ha, jen ĉi tiu ekzemplo pervorte: \begin_inset Quotes eld \end_inset \emph on ĉi tiam estas somero, kaj ĉe somero estas varma. Do, ĉi tiam estas somero kaj estas varma \emph default \begin_inset Quotes erd \end_inset . \layout Subsection Iomete pli kompleksa. \begin_inset Formula $P\wedge Q\Rightarrow R,\ Q\Rightarrow P,\ Q\vdash R$ \end_inset \layout Standard Provu vi mem solvi \begin_inset Formula $P\wedge Q\Rightarrow R,\ Q\Rightarrow P,\ Q\vdash R$ \end_inset . Poste vidu ĝian solvon: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard P \backslash wedge Q \backslash Rightarrow R \backslash \backslash \layout Standard Q \backslash Rightarrow P \backslash \backslash \layout Standard Q \backslash \backslash \layout Standard P & E$ \backslash Rightarrow$ 2,3 \backslash \backslash \layout Standard P \backslash wedge Q & I$ \backslash wedge$ 4,3 \backslash \backslash \layout Standard R & E$ \backslash Rightarrow$ 1,5 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Standard La nura rimedo por atingi \begin_inset Formula $R$ \end_inset estas uzante la unuan formulon, \begin_inset Formula $P\wedge Q\Rightarrow R$ \end_inset , sed oni nur povas uzi ĝin kiam \begin_inset Formula $P\wedge Q$ \end_inset certas, do klopodu pruvi ĝian certecon. \layout Standard Ni scias ke \begin_inset Formula $Q\Rightarrow P$ \end_inset (linio 2) kaj ke \begin_inset Formula $Q$ \end_inset (linio 3), do ni deduktas ke \begin_inset Formula $P$ \end_inset . Ĉar nun \begin_inset Formula $P$ \end_inset certas kaj ankaŭ \begin_inset Formula $Q$ \end_inset , do ankaŭ \begin_inset Formula $P\wedge Q$ \end_inset . Ĝis nun tio similas al la antaŭa ekzerco. \layout Standard Laste, ni havas \begin_inset Formula $P\wedge Q\Rightarrow R$ \end_inset , kaj scias ke \begin_inset Formula $P\wedge Q$ \end_inset , do eblas diri (fine) ke \begin_inset Formula $R$ \end_inset . \layout Subsection Jam supozante aĵojn. \begin_inset Formula $P\Rightarrow Q,\ Q\Rightarrow R\vdash P\Rightarrow Q\wedge R$ \end_inset \layout Standard Ĉi tiu, \begin_inset Formula $P\Rightarrow Q,\ Q\Rightarrow R\vdash P\Rightarrow Q\wedge R$ \end_inset , estas pli interesa: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard P \backslash Rightarrow Q \backslash \backslash \layout Standard Q \backslash Rightarrow R \backslash \backslash \layout Standard \backslash fh P & H \backslash \backslash \layout Standard \backslash fa Q & E$ \backslash Rightarrow$ 1,3 \backslash \backslash \layout Standard \backslash fa R & E$ \backslash Rightarrow$ 2,4 \backslash \backslash \layout Standard \backslash fa Q \backslash wedge R & I$ \backslash wedge$ 4,5 \backslash \backslash \layout Standard P \backslash Rightarrow Q \backslash wedge R & I$ \backslash Rightarrow$ 3,6 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Standard Notu la jenajn detalojn: \layout Itemize Ni havas nenian informon pri io ajn kio certas nun (ni mankas formulojn kiajn \begin_inset Formula $P$ \end_inset , aŭ \begin_inset Formula $Q\wedge R$ \end_inset , ktp.). Oni nur aldiras al ni ideojn kiajn ke \emph on se okazus \begin_inset Formula $P$ \end_inset , tiam ankaŭ okazus \begin_inset Formula $Q$ \end_inset \emph default . \layout Itemize Simile, kio ni devas pruvi ne estas ke \emph on ĵus nun io okazas \emph default , sed ke \emph on se okazus \begin_inset Formula $P$ \end_inset , tiam \begin_inset Formula $Q$ \end_inset kaj \begin_inset Formula $R$ \end_inset estus certaj \emph default . \layout Itemize \begin_inset Formula $P\Rightarrow Q\wedge R$ \end_inset estas implikacio ( \emph on io entenas ion \emph default ), ĉar operatoro \begin_inset Formula $\Rightarrow$ \end_inset havas malpli prioritaton ol \begin_inset Formula $\wedge$ \end_inset . Estas grava eraro interpreti tiun formulon kvazaŭ \begin_inset Formula $(P\Rightarrow Q)\wedge R$ \end_inset . \layout Standard Ĉar la formulon ni serĉas estas implikacio ( \begin_inset Formula $P\Rightarrow Q\wedge R$ \end_inset ), ni devos uzi la \emph on kunimplikaciigon \emph default , sed tiu regulo necesas subderivon (vidu ĝian difinon). \layout Standard Kompreni kial, ne estas malfacile: \begin_inset Formula $P\Rightarrow Q\wedge R$ \end_inset diras ke \emph on se \begin_inset Formula $P$ \end_inset okazas, tiam okazas \begin_inset Formula $Q\wedge R$ \end_inset \emph default , do unue oni devos supozi ke ja okazas \begin_inset Formula $P$ \end_inset . Tiam oni klopodu ke, ĉe la okazo kiam \begin_inset Formula $P$ \end_inset certas, ankaŭ certas \begin_inset Formula $Q\wedge R$ \end_inset . Tion atingite, oni aplikas la regulon por restigi ĉion bone skribite: \begin_inset Formula $P\Rightarrow Q\wedge R$ \end_inset . \layout Standard Tial, ĉe linio 3 oni faras hipotezon (klarigita per la dekstra \begin_inset Formula $H$ \end_inset ): supozu ke \begin_inset Formula $P$ \end_inset certas. Nun komencas subderivon, ĉe kie oni povas uzi ĉiun veraĵon el la patra derivo (linioj 1 kaj 2 ĉe tiu okazo), kaj ankaŭ povas uzi \begin_inset Formula $P$ \end_inset kvazaŭ ĝi estus certa. \layout Standard Oni faris tiun hipotezon celante scii ke \begin_inset Formula $Q\wedge R$ \end_inset , do oni deduktas ĝin simile al la antaŭaj ekzemploj. Notu la uzadon de veraĵojn el ene kaj ekstere de la subderivo, kaj ankaŭ ke, ĝis fino de la subderivo, tiu vertikala maldekstra linio devas esti metita. \layout Standard Ĉe linio 6 oni jam havas \begin_inset Formula $Q\wedge R$ \end_inset , kion ni volis. Uzante la derivregulon de \emph on kunimplikaciigo \emph default , oni eliras el tiu subderivo, asertante ke \emph on se la hipotezo estas certa, tiam ankaŭ certas io kion ni deduktis el ĝi \emph default . Oni malmetas la vertikalan linion, ĉar \begin_inset Formula $P\Rightarrow Q\wedge R$ \end_inset estas ĉiam certa (sendepende je ĉu \begin_inset Formula $P$ \end_inset estas vera aŭ ne). La uzata klarigo, \begin_inset Formula $I\Rightarrow\ 3,6$ \end_inset , diras ke estas linio 3 kie oni faris la supozon, kaj 6 la linio kie oni divenis ion interesan kio okazas farinte tiun supozon. \layout Standard \begin_inset Formula $P\Rightarrow Q\wedge R$ \end_inset estas kion ni serĉis, do oni jam finis. La fino estas same kiel antaŭe, ĉar oni ja estas ekstere de subderivo. \layout Subsection Uzante iteracion. \begin_inset Formula $P\vdash Q\Rightarrow P$ \end_inset \layout Standard Tiu ĉi estas tre mallonga: \begin_inset Formula $P\vdash Q\Rightarrow P$ \end_inset . Jen solvo: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard P \backslash \backslash \layout Standard \backslash fh Q & H \backslash \backslash \layout Standard \backslash fa P & IT 1 \backslash \backslash \layout Standard Q \backslash Rightarrow P & I$ \backslash Rightarrow$ 2,3 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Standard La vojo estas direkta: oni supozu \begin_inset Formula $Q$ \end_inset , kaj vidu ke, tiuokaze, estas prava \begin_inset Formula $P$ \end_inset . Jen sekreteto: \begin_inset Formula $P$ \end_inset ĉiam certas, ĉu supozinte \begin_inset Formula $Q$ \end_inset aŭ ĉu ne. \layout Standard Oni devos uzi \emph on kunimplikaciigon \emph default , sed tio necesas hipotezon, kaj, kelkaj linioj sube, la rezulton supozi tion. Nur tiam oni povos fermi la subderivon. \layout Standard Post ĝia malfermo (linio 2), oni faru ion por restigi skribe ke \begin_inset Formula $P$ \end_inset . Ĉar ni jam havas ĝin verkita en linio 1, simple metu \begin_inset Formula $P$ \end_inset denove kaj klarigu per \begin_inset Formula $IT\ 1$ \end_inset , kio signifas \begin_inset Quotes eld \end_inset \emph on ĉi tion mi kopiis de linio 1 \emph default \begin_inset Quotes erd \end_inset . La \begin_inset Formula $IT$ \end_inset estas pro \emph on iteracio \emph default . \layout Standard Jam oni plenumas la kondiĉojn por apliki la derivregulon, do oni apliku ĝin, eliru el subderivo, kaj jam estas finita. \layout Subsection Redukto al absurdo. \begin_inset Formula $P\Rightarrow Q,\ \neg Q\vdash\neg P$ \end_inset \layout Standard Tiu estas utilega tekniko. La validecon de \begin_inset Formula $P\Rightarrow Q,\ \neg Q\vdash\neg P$ \end_inset oni pruvu per: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard P \backslash Rightarrow Q \backslash \backslash \layout Standard \backslash neg Q \backslash \backslash \layout Standard \backslash fh P & H \backslash \backslash \layout Standard \backslash fa Q & E$ \backslash Rightarrow$ 1,3 \backslash \backslash \layout Standard \backslash fa \backslash neg Q & IT 2 \backslash \backslash \layout Standard \backslash neg P & I$ \backslash neg$ 3,4,5 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Standard Atingenda estas \begin_inset Formula $\neg P$ \end_inset , kiu estas \emph on la nego de io \emph default , tial oni devos uzi la regulon de \emph on kunnegigo \emph default , konata per \emph on redukto al absurdo \emph default (kaj ankaŭ \emph on enigo de negacio \emph default ). \layout Standard La maniero fari tion estos supozi tion kontraŭan al \begin_inset Formula $\neg P$ \end_inset (kio estas \begin_inset Formula $P$ \end_inset ) kaj atingi memkontraŭdiron. Supozante \begin_inset Formula $P$ \end_inset oni atingas \begin_inset Formula $Q$ \end_inset (per \emph on elimplikaciigo \emph default ), kaj, ĉar oni ankaŭ havas \begin_inset Formula $\neg Q$ \end_inset , eblas apliki la regulon. Tiu \begin_inset Formula $\neg Q$ \end_inset devos esti metita en la subderivon per \emph on iteracio \emph default , por ke ĝi estu kun la \begin_inset Formula $Q$ \end_inset kaj \emph on en \emph default la subderivo. Ĉio kio estas interne de la subderivo estas sekvo de \begin_inset Formula $P$ \end_inset , do estas grava rimarki ke tiel \begin_inset Formula $Q$ \end_inset kiel \begin_inset Formula $\neg Q$ \end_inset ambaŭ estas ĝia sekvo. \layout Standard Pri la \emph on kunnegigo \emph default , la maniero klarigi la regulon estas metante la linionumeron kie komencas la supozo (malprava), kaj la numerojn el la du linioj kie oni vidis la kontraŭdiron. La konkludo de ĉi tiu regulo estas tio kontraŭa al kio oni supozis, tiuokaze \begin_inset Formula $\neg P$ \end_inset , do la procedo jen finiĝas. \layout Standard Tiu rezonado verŝajne oni faras senpense. Pervorte, ĝi estus kiel: \begin_inset Quotes eld \end_inset \emph on kompreneble ke \begin_inset Formula $\neg P$ \end_inset , ĉar se estus \begin_inset Formula $P$ \end_inset , do \begin_inset Formula $Q$ \end_inset , kaj vi diris ke \begin_inset Formula $\neg Q$ \end_inset , do ne eblas ke \begin_inset Formula $P$ \end_inset \emph default \begin_inset Quotes erd \end_inset . \layout Subsection Kun subderivoj. \begin_inset Formula $P\Rightarrow(Q\Rightarrow R)\vdash Q\Rightarrow(P\Rightarrow R)$ \end_inset \layout Standard La afero malfaciliĝas. Jen la solvo de \begin_inset Formula $P\Rightarrow(Q\Rightarrow R)\vdash Q\Rightarrow(P\Rightarrow R)$ \end_inset : \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard P \backslash Rightarrow (Q \backslash Rightarrow R) \backslash \backslash \layout Standard \backslash fh Q & H \backslash \backslash \layout Standard \backslash fa \backslash fh P & H \backslash \backslash \layout Standard \backslash fa \backslash fa Q \backslash Rightarrow R & E$ \backslash Rightarrow$ 1,3 \backslash \backslash \layout Standard \backslash fa \backslash fa R & E$ \backslash Rightarrow$ 4,2 \backslash \backslash \layout Standard \backslash fa P \backslash Rightarrow R & I$ \backslash Rightarrow$ 3,5 \backslash \backslash \layout Standard Q \backslash Rightarrow (P \backslash Rightarrow R) & I$ \backslash Rightarrow$ 2,6 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Standard Unue: ĉi tie oni nur uzos la du derivregulojn kiuj helpas enigi kaj forigi implikaciojn, ĉar ĝi estas la sola operatoro kiun oni havas. \layout Standard Oni volas atingi \begin_inset Formula $Q\Rightarrow(P\Rightarrow R)$ \end_inset , do oni devos fari hipotezon \begin_inset Formula $Q$ \end_inset ĉe kie oni devos montri ke \begin_inset Formula $P\Rightarrow R$ \end_inset . Faru tion nun por faciligi la problemon: oni malfermas la subderivon en linio 2. Oni ne fermos ĝin ĝis kiam oni scias ke \begin_inset Formula $P\Rightarrow R$ \end_inset estas certa. \layout Standard Nun la problemo estas iom pli facila. Oni bezonas pruvi \begin_inset Formula $P\Rightarrow R$ \end_inset , kaj havas du liniojn kun du veraĵoj: la unua diras \begin_inset Formula $P\Rightarrow(Q\Rightarrow R)$ \end_inset , kaj la dua \begin_inset Formula $Q$ \end_inset . \layout Standard Kiel povas oni alproksimiĝi al \begin_inset Formula $P\Rightarrow R$ \end_inset ? Nu, same kiel iam ajn: ni devas supozi ke \begin_inset Formula $P$ \end_inset , kaj eltrovi ke \begin_inset Formula $R$ \end_inset , iel. Eĉ se tio ne ŝajnas facila, estas kion oni faru, ĉar la \emph on kunimplikaciigo \emph default tiel funkcias. Do, malfermu alian hipotezon, nun supozante ke \begin_inset Formula $P$ \end_inset , kaj eble oni atingos \begin_inset Formula $R$ \end_inset . Ĉi tiu estas hipotezo en hipotezo, tamen tio estas nenia problemo. \layout Standard Skribinte la linio 3, kaj, metite en \emph on subsubderivo \emph default , oni disponas de tri scioj: ke \begin_inset Formula $P\Rightarrow(Q\Rightarrow R)$ \end_inset , ke \begin_inset Formula $Q$ \end_inset , kaj ke \begin_inset Formula $P$ \end_inset . Oni devas pruvi ke \begin_inset Formula $R$ \end_inset . Ne estas tiom malfacile, ĉu? Se oni scias ke \begin_inset Formula $P$ \end_inset , uzante \emph on elimplikaciigon \emph default kun linio 1 oni ricevos la certan formulon \begin_inset Formula $Q\Rightarrow R$ \end_inset . Ĉar \begin_inset Formula $Q$ \end_inset ankaŭ certas (linio 2), oni povas reapliki tiun regulon por ekscii ke \begin_inset Formula $R$ \end_inset . \layout Standard Videble, supozinte \begin_inset Formula $P$ \end_inset oni atingis la konkludon \begin_inset Formula $R$ \end_inset , do eblas skribi en nova linio ke \begin_inset Formula $P\Rightarrow R$ \end_inset , kion ni serĉadis. Nun jam eliris el la subsubderivo, kaj nur estas sub la supozo ke \begin_inset Formula $Q$ \end_inset certas. Ĉar oni vidas ke tiu supozo entenas la certecon de la formulo \begin_inset Formula $P\Rightarrow R$ \end_inset , oni povas eliri tiun subderivon konkludante ke \begin_inset Formula $Q\Rightarrow(P\Rightarrow R)$ \end_inset . \layout Standard \begin_inset Formula $Q\Rightarrow(P\Rightarrow R)$ \end_inset estis precipe kion oni volis pruvi, do jam estas finata la derivo. \layout Subsection Iu kun provo per okazoj. \begin_inset Formula $P\vee(Q\wedge R)\vdash P\vee Q$ \end_inset \layout Standard Oni uzu la plej malfacilan derivregulon, \emph on elaŭigon \emph default . \begin_inset Formula $P\vee(Q\wedge R)\vdash P\vee Q$ \end_inset solvita: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard P \backslash vee (Q \backslash wedge R) \backslash \backslash \layout Standard \backslash fh P & H \backslash \backslash \layout Standard \backslash fa P \backslash vee Q & I$ \backslash vee$ 2 \backslash \backslash \layout Standard \backslash fh Q \backslash wedge R & H \backslash \backslash \layout Standard \backslash fa Q & E$ \backslash wedge$ 4 \backslash \backslash \layout Standard \backslash fa P \backslash vee Q & I$ \backslash vee$ 5 \backslash \backslash \layout Standard P \backslash vee Q & E$ \backslash vee$ 1,3,6 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Standard Vi jam scias la regulojn, do mi klarigas la manieron pensi de iu homo, kiu eble ne komprenas naturan dedukton, sed estas iom pensema: \layout Standard Oni devas pruvi ke \begin_inset Formula $P\vee Q$ \end_inset ĉiam certas. La maldekstra esprimo, \begin_inset Formula $P\vee(Q\wedge R)$ \end_inset , povas certiĝi pro du motivoj: \layout Itemize se ĝi certas pro la vero de \begin_inset Formula $P$ \end_inset , tiam \begin_inset Formula $P\vee Q$ \end_inset ja estas certa. \layout Itemize se ĝi certas pro la vero de \begin_inset Formula $Q\wedge R$ \end_inset , tiam \begin_inset Formula $Q$ \end_inset kaj \begin_inset Formula $R$ \end_inset estas ambaŭ certaj, do \begin_inset Formula $P\vee Q$ \end_inset certas per \begin_inset Formula $Q$ \end_inset . \layout Standard Do, ĉiel, \begin_inset Formula $P\vee Q$ \end_inset estas vera. \layout Standard Nun, la cetero estas traduki tion al logika lingvo, sekvante la saman ordon kiel antaŭe, kaj iom post iom. \layout Standard Oni komencas pruvante unu vojo, poste, la alian, kaj fine oni aplikas \emph on elaŭigon \emph default . Por klarigi la regulon oni devas skribi la linion kiu enhavas la disjunkcion, kaj la du liniojn el ene de ĉiu subderivo kie montriĝas ke, supozante iun aĵon aŭ la alian, la rezulto estas la samo. \layout Standard Rimarku ke, eĉ se oni eltrovis ke \begin_inset Formula $P\Rightarrow P\vee Q$ \end_inset kaj ke \begin_inset Formula $Q\wedge R\Rightarrow P\vee Q$ \end_inset , ne estas necese uzi \emph on kunimplikaciigon \emph default por restigi skribe tion. \layout Standard La plej malfacilo el la \emph on provo per okazoj \emph default normale estas decidi, kiun esprimon oni provos pruvi en ambaŭ okazoj. Ĝi estu la sama en ambaŭ okazoj! \layout Subsection Iu por pensi. \begin_inset Formula $L\wedge M\Rightarrow\neg P,\ I\Rightarrow P,\ M,\ I\vdash\neg L$ \end_inset \layout Standard Provu pripensi \begin_inset Formula $L\wedge M\Rightarrow\neg P,\ I\Rightarrow P,\ M,\ I\vdash\neg L$ \end_inset ; poste skribu ĝin en papero. Ĝi restas: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard L \backslash wedge M \backslash Rightarrow \backslash neg P \backslash \backslash \layout Standard I \backslash Rightarrow P \backslash \backslash \layout Standard M \backslash \backslash \layout Standard I \backslash \backslash \layout Standard \backslash fh L & H \backslash \backslash \layout Standard \backslash fa L \backslash wedge M & I$ \backslash wedge$ 5,3 \backslash \backslash \layout Standard \backslash fa \backslash neg P & E$ \backslash Rightarrow$ 1,6 \backslash \backslash \layout Standard \backslash fa P & E$ \backslash Rightarrow$ 2,4 \backslash \backslash \layout Standard \backslash neg L & I$ \backslash neg$ 5,7,8 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Standard Pervorte: \begin_inset Quotes eld \end_inset \emph on se vi uzas Linukson (Linux) kaj Mozilon (Mozilla) kiel foliumilo, vi evitas problemojn. Tamen, se vi uzas 'Internet Explorer' vi havos problemojn. Nun vi uzas Mozilon, sed iam ankaŭ 'Internet Explorer'. Do, mi scias ke vi ne uzas Linukson \emph default \begin_inset Quotes erd \end_inset . \layout Standard Eble tio ŝajnas al vi evidenta: \begin_inset Quotes eld \end_inset \emph on kompreneble, ĉar IE ne estas ĉe Linukso \emph default \begin_inset Quotes erd \end_inset , sed notu ke mi neniam diris tion. La \begin_inset Formula $I\Rightarrow\neg L$ \end_inset estas nenie. \layout Standard La rimedon kiun vi devos sekvi dum vi pripensas la ekzercon estas: \layout Enumerate Mi bezonas pruvi \begin_inset Formula $\neg L$ \end_inset , kio estas nego de io. Estas videbla nenia regulo kiel \emph on io entenas \begin_inset Formula $\neg L$ \end_inset , \emph default kiu ebligas min atingi ĝin direkte. Oni devos uzi alian metodon, ekzemple \emph on kunnegigo \emph default ( \emph on redukto al absurdo \emph default ): supozu ke mi ja uzas Linukson. \layout Enumerate Ĉe la okazo kiam mi uzas Linukson, mi uzus ambaŭ Linukson kaj Mozilon, ĉar mi jam uzis Mozilon antaŭe (tiu estas la tria veraĵo skribita en la problema esprimo). \layout Enumerate Uzante Linukson kaj Mozilon, mi ne havos komputikajn problemojn, ĉar \begin_inset Formula $L\wedge M\Rightarrow\neg P$ \end_inset . \layout Enumerate Sed mi ankaŭ uzis Internet Explorer (kvara veraĵo), kaj, ĉar IE kunportas problemojn, mi havos problemojn. \begin_inset Formula $P$ \end_inset . \layout Enumerate Mi atingis memkontraŭdiron: \begin_inset Formula $\neg P$ \end_inset kaj \begin_inset Formula $P$ \end_inset . Do, kio vere okazas estas ke mia supozo pri uzado de Linukso estas malkorekta: prave \begin_inset Formula $\neg L$ \end_inset . \layout Standard Nun vi nur devas sekvi la saman procedon, sed skribante ĝin paŝon post paŝo, kaj uzante la regulojn. Kion vi ricevos estos kiel la supran figuron, kiu havas precipe 5 procedajn liniojn (ĉar la unuaj 4 estas por kopii la veraĵojn). Ĉiu linio rilatas al ĉiu paŝo kiun mi klarigis tie. \layout Subsection Malplena maldekstra parto. \begin_inset Formula $\vdash P\Rightarrow P$ \end_inset \layout Standard Pruvi \begin_inset Formula $\vdash P\Rightarrow P$ \end_inset estas tre facila kaj mallonga: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard \backslash fh P & H \backslash \backslash \layout Standard \backslash fa P & IT 1 \backslash \backslash \layout Standard P \backslash Rightarrow P & I$ \backslash Rightarrow$ 1,2 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Standard Tia ekzerco ankoraŭ ne aperis: videble, la maldekstra parto de la derivo estas malplena. Tio signifas ke oni estas dirita nenia veraĵo kiun oni povas uzi por pruvi \begin_inset Formula $P\Rightarrow P$ \end_inset . Kial? Nu, ĉar \begin_inset Formula $P\Rightarrow P$ \end_inset estas ĉiam certa, sendepende de la valoro de \begin_inset Formula $P$ \end_inset aŭ la aliaj formuloj. \layout Standard Estas plej komode kaj facile solvi tiajn derivojn, ĉar oni komencas la laboron direkte kun la formulon oni volas atingi. Sed atentu, ĉar kelkaj \emph on absolutaj veroj \emph default (kiaj ĉiam estas pravaj) estas ege malfacile kaj bezonas longajn pruvojn. \layout Standard Notu: ĉiam kiam la maldekstra parto estas malplena, oni devas komenci per hipotezo (kion alian oni povus fari?). \layout Standard Por atingi la pruvon de \begin_inset Formula $P\Rightarrow P$ \end_inset oni agas kiel antaŭe: supozu \begin_inset Formula $P$ \end_inset kaj provu atingi la veron de \begin_inset Formula $P$ \end_inset . Ĉar oni ĵus supozis ĝin ĉe la unua linio, oni nur devas uzi la regulon de \emph on iteracio \emph default por kopii ĝin al interne, kaj finu la subderivon per \emph on kunimplikaciigo \emph default . Jam estas ĉio farita, per tri linioj. \layout Standard Rimarku ke \begin_inset Formula $P\Rightarrow P$ \end_inset estas certa ĉar \begin_inset Formula $\blacksquare\Rightarrow\blacksquare$ \end_inset kaj \begin_inset Formula $\square\Rightarrow\square$ \end_inset . Mi profitas por memorigi ke ankaŭ \begin_inset Formula $\square\Rightarrow\blacksquare$ \end_inset , sed \begin_inset Formula $\blacksquare\nRightarrow\square$ \end_inset . \layout Subsection Supozu tion kontraŭan. \begin_inset Formula $\vdash\neg(P\wedge\neg P)$ \end_inset \layout Standard Jen iu ankaŭ facila, \begin_inset Formula $\vdash\neg(P\wedge\neg P)$ \end_inset . Oni agas tiel: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard \backslash fh P \backslash wedge \backslash neg P & H \backslash \backslash \layout Standard \backslash fa P & E$ \backslash wedge$ 1 \backslash \backslash \layout Standard \backslash fa \backslash neg P & E$ \backslash wedge$ 1 \backslash \backslash \layout Standard \backslash neg (P \backslash wedge \backslash neg P) & I$ \backslash neg$ 1,2 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Standard Ĉiuj el ni scias ke ne eblas okazi du kontraŭajn aĵojn samtempe, sed, kial oni povas pruvi tion? Per \emph on redukto al absurdo \emph default : \layout Standard Supozu ke ja okazas \begin_inset Formula $P\wedge\neg P$ \end_inset . Tiam okazas \begin_inset Formula $P$ \end_inset kaj \begin_inset Formula $\neg P$ \end_inset , ambaŭ samtempe, kio estas memkontraŭdiron. Do, nian supozon ne eblas certu, do estas falsa. Tiel oni pruvas \begin_inset Formula $\neg(P\wedge\neg P)$ \end_inset . \layout Standard Vidante ion tiom \emph on klara \emph default kaj \emph on memkomprenebla \emph default kiom \begin_inset Formula $\neg(P\wedge\neg P)$ \end_inset , tiam tio kontraŭa estos \emph on klare \emph default falsa kaj absurda. Do vi facile eblos pruvi ke tio ne sin tenas kaj memkontraŭdiras. Poste, oni povos certigi ke originala formulo estas certa ĉar ĝia kontraŭa estas falsa. \layout Subsection Tiu ŝajnas facila. \begin_inset Formula $\vdash P\vee\neg P$ \end_inset \layout Standard Ĉu \begin_inset Formula $\vdash P\vee\neg P$ \end_inset estas tiom facila? \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard \backslash fh \backslash neg (P \backslash vee \backslash neg P) & H \backslash \backslash \layout Standard \backslash fa \backslash fh P & H \backslash \backslash \layout Standard \backslash fa \backslash fa P \backslash vee \backslash neg P & I$ \backslash vee$ 2 \backslash \backslash \layout Standard \backslash fa \backslash fa \backslash neg (P \backslash vee \backslash neg P) & IT 1 \backslash \backslash \layout Standard \backslash fa \backslash neg P & I$ \backslash neg$ 2,3,4 \backslash \backslash \layout Standard \backslash fa \backslash fh \backslash neg P & H \backslash \backslash \layout Standard \backslash fa \backslash fa P \backslash vee \backslash neg P & I$ \backslash vee$ 6 \backslash \backslash \layout Standard \backslash fa \backslash fa \backslash neg (P \backslash vee \backslash neg P) & IT 1 \backslash \backslash \layout Standard \backslash fa \backslash neg \backslash neg P & I$ \backslash neg$ 6,7,8 \backslash \backslash \layout Standard \backslash fa P & E$ \backslash neg$ 9 \backslash \backslash \layout Standard \backslash neg \backslash neg (P \backslash vee \backslash neg P) & I$ \backslash neg$ 1,5,10 \backslash \backslash \layout Standard P \backslash vee \backslash neg P & E$ \backslash neg$ 11 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Standard Unu el la plej simplaj kaj longaj kiuj mi trovis. Ŝajnas eĉ ne necese pruvadi tion, ĉar iu ajn scias ke el la du aĵojn \begin_inset Quotes eld \end_inset \emph on hodiaŭ estas ĵaŭdo \emph default \begin_inset Quotes erd \end_inset kaj \begin_inset Quotes eld \end_inset \emph on hodiaŭ ne estas ĵaŭdo \emph default \begin_inset Quotes erd \end_inset , unu el ili estas certa (ne eblas ke ambaŭ estu falsaj samtempe). \layout Standard Oni povus unue pensi en la rimedon de \emph on provo per okazoj \emph default , ĉar el \begin_inset Formula $P$ \end_inset eblas eltiri \begin_inset Formula $P\vee\neg P$ \end_inset , kaj el \begin_inset Formula $\neg P$ \end_inset eltiri \begin_inset Formula $P\vee\neg P$ \end_inset , do, la saman formulon. Sed tio malutilas, ĉar derivregulo de \emph on provo per okazoj \emph default estas \emph on elaŭigo \emph default kaj oni mankas iun aŭon por eligi; fakte, oni nek havas la certan formulon \begin_inset Formula $A\vee B$ \end_inset tiel ke \begin_inset Formula $A\Rightarrow C$ \end_inset kaj \begin_inset Formula $B\Rightarrow C$ \end_inset , kiel la regulo bezonas. Plej fakte, oni havas neniun formulon kies certecon oni povas aserti (la maldekstra parto de la derivo estas malplena). \layout Standard Oni scias ke ĉe la komenco, hipotezon devas fari (ĉar ne estas alia vojo). Estas \begin_inset Quotes eld \end_inset \emph on sufiĉe \emph default \begin_inset Quotes erd \end_inset klara por ni ke \begin_inset Formula $P\vee\neg P$ \end_inset certas, do verŝajne ĝian kontraŭan, \begin_inset Formula $\neg(P\vee\neg P)$ \end_inset , estos facile pruvebla falsa. Do oni uzos \emph on redukton al absurdo \emph default : supozinte tion ĉe linio 1, oni devas atingi memkontraŭdiron, iu ajn. \layout Standard Mi celis atingi kontraŭdiron \begin_inset Formula $\neg P$ \end_inset kaj \begin_inset Formula $P$ \end_inset . Tamen, oni mankas tiujn formulojn; kie ni trovigos ilin? Nu, eblas refari \emph on redukton al absurdo \emph default : por ekvidi \begin_inset Formula $\neg P$ \end_inset , supozu \begin_inset Formula $P$ \end_inset por atingi memkontraŭdiron. Kiel antaŭe, estas utilege profiti eblojn de \emph on kunaŭigo \emph default : supozinte \begin_inset Formula $P$ \end_inset , oni povas ŝanĝigi ĝin al \begin_inset Formula $P\vee\neg P$ \end_inset por serĉi kontraŭdiron. Ĉar oni havas la \begin_inset Formula $\neg(P\vee\neg P)$ \end_inset tute supre, oni rajtas uzi ĝin por fine pruvi \begin_inset Formula $\neg P$ \end_inset . Same oni faras por atingi \begin_inset Formula $P$ \end_inset , sed tiuokaze supozante \begin_inset Formula $\neg P$ \end_inset . \layout Standard Ricevite \begin_inset Formula $P$ \end_inset kaj \begin_inset Formula $\neg P$ \end_inset post la supozado de \begin_inset Formula $\neg(P\vee\neg P)$ \end_inset , oni vidas ke tiu formulo maleblas certi, do ĝia nego, \begin_inset Formula $\neg\neg(P\vee\neg P)$ \end_inset , ja certas. Per \emph on elnegigo \emph default , fine estas trovita serĉatan formulon: \begin_inset Formula $P\vee\neg P$ \end_inset . \layout Standard Mi agis tiel por igi la skemon iom simetria, sed oni ja povas solvi la problemon per malpliaj paŝoj serĉante alian memkontraŭdiron, ekzemple \begin_inset Formula $P\vee\neg P$ \end_inset kaj \begin_inset Formula $\neg(P\vee\neg P)$ \end_inset . Tiel ĝi restus: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard \backslash fh \backslash neg (P \backslash vee \backslash neg P) & H \backslash \backslash \layout Standard \backslash fa \backslash fh P & H \backslash \backslash \layout Standard \backslash fa \backslash fa P \backslash vee \backslash neg P & I$ \backslash vee$ 2 \backslash \backslash \layout Standard \backslash fa \backslash fa \backslash neg (P \backslash vee \backslash neg P) & IT 1 \backslash \backslash \layout Standard \backslash fa \backslash neg P & I$ \backslash neg$ 2,3,4 \backslash \backslash \layout Standard \backslash fa P \backslash vee \backslash neg P & I$ \backslash vee$ 5 \backslash \backslash \layout Standard \backslash fa \backslash neg (P \backslash vee \backslash neg P) & IT 1 \backslash \backslash \layout Standard \backslash neg \backslash neg (P \backslash vee \backslash neg P) & I$ \backslash neg$ 1,6,7 \backslash \backslash \layout Standard P \backslash vee \backslash neg P & E$ \backslash neg$ 8 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Subsection Iu interesa. \begin_inset Formula $P\vee Q,\ \neg P\vdash Q$ \end_inset \layout Standard Ankaŭ ŝajnas facila: \begin_inset Formula $P\vee Q,\ \neg P\vdash Q$ \end_inset . Jen: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard P \backslash vee Q \backslash \backslash \layout Standard \backslash neg P \backslash \backslash \layout Standard \backslash fh P & H \backslash \backslash \layout Standard \backslash fa \backslash fh \backslash neg Q & H \backslash \backslash \layout Standard \backslash fa \backslash fa \backslash neg P & IT 2 \backslash \backslash \layout Standard \backslash fa \backslash fa P & IT 3 \backslash \backslash \layout Standard \backslash fa \backslash neg \backslash neg Q & I$ \backslash neg$ 4,5,6 \backslash \backslash \layout Standard \backslash fa Q & E$ \backslash neg$ 7 \backslash \backslash \layout Standard \backslash fh Q & H \backslash \backslash \layout Standard \backslash fa Q & IT 9 \backslash \backslash \layout Standard Q & E$ \backslash vee$ 1,8,10 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Standard Estas facilege kompreneble por iu ajn: certas \begin_inset Formula $P\vee Q$ \end_inset , sed \begin_inset Formula $P$ \end_inset estas falsa, do la vero estas \begin_inset Formula $Q$ \end_inset . \layout Standard Diversaj metodoj ekzistas, sed iam oni devos uzi \emph on elaŭigon \emph default por ion fari kun \begin_inset Formula $P\vee Q$ \end_inset . Provu pruvi ke ambaŭ \begin_inset Formula $P$ \end_inset kaj \begin_inset Formula $Q$ \end_inset kondukas al la sama loko, kiu estos nian celan formulon \begin_inset Formula $Q$ \end_inset (ĉar eblas iri direkte al \begin_inset Formula $Q$ \end_inset , do profitu). \layout Standard Do oni malfermas subderivon supozante \begin_inset Formula $P$ \end_inset , kaj celas eltrovi ke \begin_inset Formula $Q$ \end_inset . Ne estas tre kompleksa, ĉar oni havas la \begin_inset Formula $\neg P$ \end_inset en linio 2; tio helpas kontraŭdiri ion ajn. Oni serĉas \begin_inset Formula $Q$ \end_inset , do supozu \begin_inset Formula $\neg Q$ \end_inset kaj per \emph on kunnegigo \emph default ricevu \begin_inset Formula $\neg\neg Q$ \end_inset , kiu estas \begin_inset Formula $Q$ \end_inset . \layout Standard La alian vojon, supozinte \begin_inset Formula $Q$ \end_inset certa, kondukas direkte al \begin_inset Formula $Q$ \end_inset . \layout Standard Do, ambaŭ vojoj iras al \begin_inset Formula $Q$ \end_inset kaj per \emph on elaŭigo \emph default oni pruvas ke \begin_inset Formula $Q$ \end_inset ĉiam certas. \layout Subsection Tiu aperis en mia ekzameno. \begin_inset Formula $A\vee B,\ A\Rightarrow C,\ \neg D\Rightarrow\neg B\vdash C\vee D$ \end_inset \layout Standard Ĉe la fina ekzameno de \emph on ILO \emph default oni demandis al mi \begin_inset Formula $A\vee B,\ A\Rightarrow C,\ \neg D\Rightarrow\neg B\vdash C\vee D$ \end_inset , kaj mi pasigis multan, multan tempon ĝis mi fine sukcesis: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard A \backslash vee B \backslash \backslash \layout Standard A \backslash Rightarrow C \backslash \backslash \layout Standard \backslash neg D \backslash Rightarrow \backslash neg B \backslash \backslash \layout Standard \backslash fh A & H \backslash \backslash \layout Standard \backslash fa C & E$ \backslash Rightarrow$ 2,4 \backslash \backslash \layout Standard \backslash fa C \backslash vee D & I$ \backslash vee$ 5 \backslash \backslash \layout Standard \backslash fh B & H \backslash \backslash \layout Standard \backslash fa \backslash fh \backslash neg D & H \backslash \backslash \layout Standard \backslash fa \backslash fa \backslash neg B & E$ \backslash Rightarrow$ 3,8 \backslash \backslash \layout Standard \backslash fa \backslash fa B & IT 7 \backslash \backslash \layout Standard \backslash fa \backslash neg \backslash neg D & I$ \backslash neg$ 8,9,10 \backslash \backslash \layout Standard \backslash fa D & E$ \backslash neg$ 11 \backslash \backslash \layout Standard \backslash fa C \backslash vee D & I$ \backslash vee$ 12 \backslash \backslash \layout Standard C \backslash vee D & E$ \backslash vee$ 1,6,13 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Standard Rimarku ke la rezulton ni serĉas, \begin_inset Formula $C\vee D$ \end_inset , estas aŭo. Ĉar vi jam konas \emph on kunaŭigon \emph default , vi povus simple serĉi \begin_inset Formula $C$ \end_inset , kaj poste uzi tiun regulon por eltrovi \begin_inset Formula $C\vee D$ \end_inset . Se vi ne trovus ke \begin_inset Formula $C$ \end_inset certas, vi eblus provi kun \begin_inset Formula $D$ \end_inset , ĉar se \begin_inset Formula $D$ \end_inset certas, tiam \begin_inset Formula $C\vee D$ \end_inset ankaŭ estas, kaj oni finas tie. \layout Standard Bedaŭrinde, \begin_inset Formula $C$ \end_inset ne estas ĉiam certa, nek \begin_inset Formula $D$ \end_inset estas ĉiam certa (tamen, \begin_inset Formula $C\vee D$ \end_inset ja ĉiam certas, kaj tio estas kion oni volas pruvi). Tion komprenite, oni devos serĉi alian rimedon kiu prilaboras kun ambaŭ formulojn, \begin_inset Formula $C$ \end_inset kaj \begin_inset Formula $D$ \end_inset , samtempe, ĉar ŝajne se oni prenas unu solan sen uzi la alian, ĝi ne aldonas multon da informo. \layout Standard Por uzi \begin_inset Formula $A\vee B$ \end_inset oni aplikos \emph on provon per okazoj \emph default . Oni provos ekscii ke tiel \begin_inset Formula $A$ \end_inset kiel \begin_inset Formula $B$ \end_inset kondukas al \begin_inset Formula $C\vee D$ \end_inset , ĉar se oni tion atingas, ne plua laboro restas. \layout Standard \begin_inset Formula $A$ \end_inset entenas \begin_inset Formula $C$ \end_inset , kaj se \begin_inset Formula $C$ \end_inset estas vera, tiam ankaŭ veras \begin_inset Formula $C\vee D$ \end_inset , do \begin_inset Formula $A$ \end_inset entenas \begin_inset Formula $C\vee D$ \end_inset . \layout Standard Por \begin_inset Formula $B$ \end_inset , kion ni scias ne rilatas ĝin al \begin_inset Formula $C$ \end_inset sed al \begin_inset Formula $D$ \end_inset . Oni volas \begin_inset Formula $C\vee D$ \end_inset . Ŝajnas malfacilege ke \begin_inset Formula $C\vee D$ \end_inset certas pro \begin_inset Formula $C$ \end_inset , do oni provos certigi nur \begin_inset Formula $D$ \end_inset . Por tio, oni uzu \emph on redukton al absurdo \emph default : supozu \begin_inset Formula $D$ \end_inset falsa, tiam certas \begin_inset Formula $\neg B$ \end_inset pro formulo el linio 3. Sed oni estas supozinte la certecon de \begin_inset Formula $B$ \end_inset , do nia hipotezo \begin_inset Formula $\neg D$ \end_inset ne estu certa. Do \begin_inset Formula $D$ \end_inset ja certas, kaj konsekvence ankaŭ \begin_inset Formula $C\vee D$ \end_inset . \layout Standard Ĉar \begin_inset Formula $A\vee B$ \end_inset ja certas, kaj ambaŭ vojoj kondukas al \begin_inset Formula $C\vee D$ \end_inset , oni fine vidas ke \begin_inset Formula $C\vee D$ \end_inset ĉiam estas certa. \layout Standard Se vi estas lerta laboristo de logikaj formuloj, eble vi eksciiĝis ke \begin_inset Formula $\neg D\Rightarrow\neg B$ \end_inset estas \begin_inset Formula $B\Rightarrow D$ \end_inset . Tio tre simpligas la problemon kaj helpas ĝin kompreni pli frue. Tamen, vi ne rajtas ŝanĝi \begin_inset Formula $\neg D\Rightarrow\neg B$ \end_inset per \begin_inset Formula $B\Rightarrow D$ \end_inset direkte; vi faru tion paŝon post paŝo por pli ĝui la logikon. \layout Subsection Iu \begin_inset Quotes eld \end_inset mallonga \begin_inset Quotes erd \end_inset . \begin_inset Formula $A\Longleftrightarrow B\vdash(A\wedge B)\vee(\neg A\wedge\neg B)$ \end_inset \layout Standard Ŝajnas facila: se du esprimoj estas ekvivalentaj, tio estas ĉar ambaŭ certas, aŭ ambaŭ falsas. Mi sukcesis pruvi la validecon de \begin_inset Formula $A\Longleftrightarrow B\vdash(A\wedge B)\vee(\neg A\wedge\neg B)$ \end_inset tiel: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard (A \backslash Rightarrow B) \backslash wedge (B \backslash Rightarrow A) \backslash \backslash \layout Standard \backslash fh \backslash neg (A \backslash vee \backslash neg A) & H \backslash \backslash \layout Standard \backslash fa \backslash fh A & H \backslash \backslash \layout Standard \backslash fa \backslash fa A \backslash vee \backslash neg A & I$ \backslash vee$ 3 \backslash \backslash \layout Standard \backslash fa \backslash fa \backslash neg (A \backslash vee \backslash neg A) & IT 2 \backslash \backslash \layout Standard \backslash fa \backslash neg A & I$ \backslash neg$ 3,4,5 \backslash \backslash \layout Standard \backslash fa A \backslash vee \backslash neg A & I$ \backslash vee$ 6 \backslash \backslash \layout Standard \backslash fa \backslash neg (A \backslash vee \backslash neg A) & IT 2 \backslash \backslash \layout Standard \backslash neg \backslash neg (A \backslash vee \backslash neg A) & I$ \backslash neg$ 2,7,8 \backslash \backslash \layout Standard A \backslash vee \backslash neg A & E$ \backslash neg$ 9 \backslash \backslash \layout Standard \backslash fh A & H \backslash \backslash \layout Standard \backslash fa A \backslash Rightarrow B & E$ \backslash wedge$ 1 \backslash \backslash \layout Standard \backslash fa B & E$ \backslash Rightarrow$ 12,11 \backslash \backslash \layout Standard \backslash fa A \backslash wedge B & I$ \backslash wedge$ 11,13 \backslash \backslash \layout Standard \backslash fa (A \backslash wedge B) \backslash vee ( \backslash neg A \backslash wedge \backslash neg B) & I$ \backslash vee$ 14 \backslash \backslash \layout Standard \backslash fh \backslash neg A & H \backslash \backslash \layout Standard \backslash fa \backslash fh B & H \backslash \backslash \layout Standard \backslash fa \backslash fa B \backslash Rightarrow A & E$ \backslash wedge$ 1 \backslash \backslash \layout Standard \backslash fa \backslash fa A & E$ \backslash Rightarrow$ 18,17 \backslash \backslash \layout Standard \backslash fa \backslash fa \backslash neg A & IT 16 \backslash \backslash \layout Standard \backslash fa \backslash neg B & I$ \backslash neg$ 17,19,20 \backslash \backslash \layout Standard \backslash fa \backslash neg A \backslash wedge \backslash neg B & I$ \backslash wedge$ 16,21 \backslash \backslash \layout Standard \backslash fa (A \backslash wedge B) \backslash vee ( \backslash neg A \backslash wedge \backslash neg B) & I$ \backslash vee$ 22 \backslash \backslash \layout Standard (A \backslash wedge B) \backslash vee ( \backslash neg A \backslash wedge \backslash neg B) & E$ \backslash vee$ 10,15,23 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Standard Unue: oni ne metu \begin_inset Formula $A\Longleftrightarrow B$ \end_inset ĉar ne havas derivregulojn por la \begin_inset Formula $\Longleftrightarrow$ \end_inset . Sed ĝi estas malplej uzata, do kiam \begin_inset Formula $\Longleftrightarrow$ \end_inset aperas, oni rajtas ŝanĝi ĝin per \begin_inset Formula $(A\Rightarrow B)\wedge(B\Rightarrow A)$ \end_inset , kiu estas la samo. \layout Standard Nu, tio estas la sola ideo mi ekpensis... Mi lasas al vi ekzercon serĉi pli mallongan formon (se ĝi ekzistas). Kion mi faris estas restigi skribe ke \begin_inset Formula $A\vee\neg A$ \end_inset ĉiam certas (tiu ekzerco jam aperis, jen mi ripetis la samajn paŝojn). Jam konante \begin_inset Formula $A\vee\neg A$ \end_inset , mi pruvas ke tiel okazo \begin_inset Formula $A$ \end_inset kiel okazo \begin_inset Formula $\neg A$ \end_inset alportas al la sama formulo, kiu estas la solvo. \layout Section Malkorektaĵoj \layout Standard Jen komunaj eraroj kiujn vi ne faru. Memoru ke logika instruisto korektos viajn ekzercojn per \emph on certo \emph default aŭ \emph on falso \emph default , do lernu faradi ĉion perfekte. \layout Subsection Enigo kaj forigo de \emph on \begin_inset Quotes eld \end_inset tio kio plej plaĉas min \begin_inset Quotes erd \end_inset \layout Standard La derivreguloj de \emph on enigo \emph default kaj \emph on forigo \emph default ne eblas verki kion vi plej ŝatas, ĉar ilia celo estas nur helpigi uzi aŭ generi formulon kun konkreta operatoro. \layout Standard Tial, se vi havas \begin_inset Formula $P$ \end_inset , ne diru \begin_inset Quotes eld \end_inset \emph on mi nun faras \emph default kunnegigon \emph on kaj eltrovas \begin_inset Formula $\neg P$ \end_inset , kiun mi ĵus bezonis \emph default \begin_inset Quotes erd \end_inset . Ekzistas kelkaj kondiĉoj por ĉiu regulo, kaj se ili ne estas plenumitaj, vi ne povas apliki la regulon. \layout Standard Jen ekzemplo (pardonu se bildoj havas hispanajn notojn): la derivregulo \emph on elimplikaciigo \emph default ne ebligas atingi formulon el la unua linio. \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard P \backslash Rightarrow Q \backslash wedge R \backslash \backslash \layout Standard Q \backslash wedge R & E$ \backslash Rightarrow$ 1,1 \layout Standard \backslash end{fitch} { \backslash textcolor{red}{ \backslash bigotimes INCORRECTO \backslash bigotimes}} \backslash ] \end_inset \layout Standard Tio estus permesita, se oni vere scius ke ĉiam certas \begin_inset Formula $P$ \end_inset ; tial oni povus apliki la regulon, bone skribinte liniajn numerojn. \layout Subsection Ion kopii el malatingebla subderivo \layout Standard Interne de la ĉefa pruvo (kiu trairas de la unua ĝis la lasta linio) oni povas malfermi \emph on filajn derivojn \emph default ( \emph on subderivojn \emph default ). Interne de subderivo oni ankaŭ povas havi \emph on subsubderivon \emph default , kiu havus kiel patro la subderivo kaj kiel avo la ĉefa derivo. \layout Standard Por ekzempli, jen la solvon de \begin_inset Formula $A\vee B,\ A\Rightarrow C,\ \neg D\Rightarrow\neg B\vdash C\vee D$ \end_inset : \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard A \backslash vee B \backslash \backslash \layout Standard A \backslash Rightarrow C \backslash \backslash \layout Standard \backslash neg D \backslash Rightarrow \backslash neg B \backslash \backslash \layout Standard \backslash fh A & H \backslash \backslash \layout Standard \backslash fa C & E$ \backslash Rightarrow$ 2,4 \backslash \backslash \layout Standard \backslash fa C \backslash vee D & I$ \backslash vee$ 5 \backslash \backslash \layout Standard \backslash fh B & H \backslash \backslash \layout Standard \backslash fa \backslash fh \backslash neg D & H \backslash \backslash \layout Standard \backslash fa \backslash fa \backslash neg B & E$ \backslash Rightarrow$ 3,8 \backslash \backslash \layout Standard \backslash fa \backslash fa B & IT 7 \backslash \backslash \layout Standard \backslash fa \backslash neg \backslash neg D & I$ \backslash neg$ 8,9,10 \backslash \backslash \layout Standard \backslash fa D & E$ \backslash neg$ 11 \backslash \backslash \layout Standard \backslash fa C \backslash vee D & I$ \backslash vee$ 12 \backslash \backslash \layout Standard C \backslash vee D & E$ \backslash vee$ 1,6,13 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Standard Nu, iu ajn derivo nur povas atingi formulojn el ene de si mem, el ĝia patro, el la patro de ĝia patro, el la patro de la patro de ĝia patro, ... Oni eble konas ĉi tiujn ulojn per \emph on prapatroj \emph default , do \emph on derivo povas atingi sin mem kaj siajn prapatrojn \emph default . \layout Standard Ekzemple, estante ĉe linio 10, la reguloj povas uzi formulojn el la jenaj lokoj: \layout Itemize el la nuna derivo (linioj 8 kaj 9, ĝisnune). \layout Itemize el la derivo patra de la 8-10, tiu estas, la linio 7. \layout Itemize el la derivo patra de kiu komencas en linio 7, do, linioj 1 al 3. \layout Standard Neniel oni povas uzi la formulojn el la linioj 4 ĝis 6, kiu estas la derivo onkla de la nuna (frato de la patro), ĉar ĉi tiu tuta derivo estas bazita en la hipotezo ke \begin_inset Formula $A$ \end_inset (linio 4), kaj oni jam finis fariĝi tiun supozon. \layout Standard Ĉe logika lingvo, oni diras ke formulo \begin_inset Formula $A$ \end_inset estas \emph on aktuala \emph default en formulo \begin_inset Formula $B$ \end_inset se estante en \begin_inset Formula $B$ \end_inset oni povas uzi \begin_inset Formula $A$ \end_inset . Por ke ĉi tio pravu, \begin_inset Formula $A$ \end_inset devas esti verkita antaŭ ol \begin_inset Formula $B$ \end_inset , kaj iu prapatro el \begin_inset Formula $B$ \end_inset devas esti patro de \begin_inset Formula $A$ \end_inset . \layout Standard Do, por pruvi \begin_inset Formula $P\wedge Q$ \end_inset vi ne rajtas fari ĉi tiel: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard \backslash fh P & H \backslash \backslash \layout Standard \backslash fa \backslash fh Q & H \backslash \backslash \layout Standard \backslash fa \backslash fa P \backslash wedge Q & I$ \backslash wedge$ 1,2 \backslash \backslash \layout Standard P \backslash wedge Q & IT 3 \layout Standard \backslash end{fitch} { \backslash textcolor{red}{ \backslash bigotimes INCORRECTO \backslash bigotimes}} \backslash ] \end_inset \layout Subsection Mismeti la krampojn \layout Standard Kiam mi verkis la regulajn difinojn, mi uzis literojn \begin_inset Formula $A$ \end_inset kaj \begin_inset Formula $B$ \end_inset , sed tiuj ja povas reprezenti ian ajn esprimon. \layout Standard Ekzemple, jen oni faras \emph on kunnegigon \emph default , kie -laŭ la regulo- oni supozas formulon \begin_inset Formula $A$ \end_inset , atingas memkontraŭdiron, kaj konkludas ke \begin_inset Formula $\neg A$ \end_inset , tio estas, la originalan formulon, sed negigitan. Oni vidu: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch*} \layout Standard 1 & \backslash fh P \backslash Rightarrow Q & H \backslash \backslash \layout Standard \backslash ldots & \backslash fa \backslash ldots \backslash \backslash \layout Standard 7 & \backslash neg P \backslash Rightarrow Q & I$ \backslash neg$ 1, \backslash ldots \layout Standard \backslash end{fitch*} { \backslash textcolor{red}{ \backslash bigotimes INCORRECTO \backslash bigotimes}} \backslash ] \end_inset \layout Standard Plej eble estas klare ke la \begin_inset Formula $A$ \end_inset ĉe tiu regulo reprezentas al \begin_inset Formula $P\Rightarrow Q$ \end_inset en ĉi tiu ekzemplo. Problemo aperas farante \begin_inset Formula $\neg A$ \end_inset . La nego de \begin_inset Formula $P\Rightarrow Q$ \end_inset ne estas \begin_inset Formula $\neg P\Rightarrow Q$ \end_inset , sed \begin_inset Formula $\neg(P\Rightarrow Q)$ \end_inset . Estas nepre necesaj la krampoj ĉar, se oni ne metas ilin, la nego nur modifas \begin_inset Formula $P$ \end_inset . \layout Standard Se vi ne scias kiam metu krampojn, ilin metu ĉiam kaj poste forviŝu tiujn malnecesajn. Ekzemple, por skribi ke \begin_inset Formula $\neg P\vee R$ \end_inset entenas \begin_inset Formula $R\wedge Q$ \end_inset , ĉirkaŭigu ĉiun esprimon per krampoj kaj do skribu \begin_inset Formula $(\neg P\vee R)\Rightarrow(R\wedge Q)$ \end_inset . Tiel, vi certe maleraras. Nun lernu kiam eblas forigi krampojn, kaj forviŝu ĉiujn eblajn. Ĉe tiu okazo, la du estas sennecesaj kaj restas \begin_inset Formula $\neg P\vee R\Rightarrow R\wedge Q$ \end_inset . \layout Subsection Fini en subderivo \layout Standard Oni ne rajtas fini dedukton ene de subderivo. La lasta linio malhavos tiun vertikalan maldekstran linieton. \layout Standard La kialo estas ke ĉio el ene de subderivo estas vera nur kiam la supozo certas, kaj la originala problemo demandis pruvi ke tio el dekstre de la \begin_inset Formula $\vdash$ \end_inset \emph on ĉiam \emph default pravas. \layout Standard Jen malekzemplo de iu aŭdaca kiu volas pruvi \begin_inset Formula $P\wedge Q$ \end_inset : \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard \backslash fh P & H \backslash \backslash \layout Standard \backslash fa \backslash fh Q & H \backslash \backslash \layout Standard \backslash fa \backslash fa P \backslash wedge Q & I$ \backslash wedge$ 1,2 \layout Standard \backslash end{fitch} { \backslash textcolor{red}{ \backslash bigotimes INCORRECTO \backslash bigotimes}} \backslash ] \end_inset \layout Standard Oni supozis \begin_inset Formula $P$ \end_inset , kaj poste \begin_inset Formula $Q$ \end_inset . Tiuokaze, kompreneble estas certa \begin_inset Formula $P\wedge Q$ \end_inset , sed \emph on nur ĉe tiu okazo \emph default . Ne eblas aserti ke \begin_inset Formula $P\wedge Q$ \end_inset ĉiam estas certa. Tial, oni devas fermadi la du derivojn (unue la interna, kaj poste la ekstera) por eltrovi iun konkludon kiu ĉiaokaze certas. \layout Standard Nek eblus apliki tiun regulon nomatan \emph on iteracion \emph default ĉe linio 4. Mi jam klarigis tion antaŭe. \layout Subsection Malfari paŝojn \layout Standard Eĉ se vi konas ekvivalentojn inter formulojn, estas plej bone se vi ne uzas ilin. Ekzemple, se vi skribu la negon de \begin_inset Formula $\neg P$ \end_inset , ne skribu \begin_inset Formula $P$ \end_inset direkte, sed metu \begin_inset Formula $\neg\neg P$ \end_inset . \layout Standard Pensu ke nenio estas tiom memvidebla, kaj ke oni povas demandi al vi pruvi derivojn kiajn \begin_inset Formula $P\vdash\neg\neg P$ \end_inset , kie se vi povus uzi la simpligojn, vi preskaŭ ne laborus. \layout Standard Ekzemple, havante \begin_inset Formula $\neg(A\vee B)$ \end_inset en linio, la paso al \begin_inset Formula $\neg A\wedge\neg B$ \end_inset ĉe la sekva estas klarigita per neniu el la 9 reguloj. Tamen, se vi sukcesas pruvi kaj kompreni ke \begin_inset Formula $\neg(A\vee B)\vdash\neg A\wedge\neg B$ \end_inset , vi eble ŝatus aldoni ĝin kiel nova regulo por uzi ĝin ĉe postaj derivoj. Mi aldonos kelkajn el tiaj ĉe sekva sekcio. \layout Section Iom pli kompleksa \layout Standard Jen mi finos klarigojn de ĉio kion mi estis instruita (eĉ se oni ne tre uzis tion). Tio pri kvantoroj gravas, sed estas pli konfuza. \layout Subsection Reguloj pri vero kaj falso \layout Standard Oni povas direkte uzi valorojn \begin_inset Formula $\blacksquare$ \end_inset ( \emph on vero \emph default ) kaj \begin_inset Formula $\square$ \end_inset ( \emph on falso \emph default ), kaj ankaŭ enigi aŭ forigi ilin ĉe nia derivo per simplaj reguloj. \layout Subsubsection Enigo de vero \layout Standard Estas la plej facila: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch*} \layout Standard \backslash hline \layout Standard & \backslash blacksquare & I$ \backslash blacksquare$ \layout Standard \backslash end{fitch*} \backslash ] \end_inset \layout Standard Do, ĉiam, kaj laŭ neniaj kondiĉoj, oni rajtas skribi ke \begin_inset Formula $\blacksquare$ \end_inset estas certa, ĉar ĝi ja estas. \layout Subsubsection Forigo de falso \layout Standard Iu amuzanta: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch*} \layout Standard n & \backslash square \backslash \backslash \layout Standard \backslash hline \layout Standard & A & E$ \backslash square$ n \layout Standard \backslash end{fitch*} \backslash ] \end_inset \layout Standard Klarigo: se oni atingis la konkludon ke \begin_inset Formula $\square$ \end_inset estas certa, oni jam atingis situacion kie oni povas elpensi ion ajn kaj aserti ke ĝi estas certa; almenaŭ tiom certa kiom la certeco de \begin_inset Formula $\square$ \end_inset ( \emph on falso \emph default ). \layout Standard Al tiu regulo oni nomas \emph on ex falso quodlibet sequitur \emph default , kaj tio signifas ke \begin_inset Quotes eld \end_inset \emph on el falso oni povas eltrovi ion ajn \emph default \begin_inset Quotes erd \end_inset . \layout Subsection Reguloj pri kvantoroj \layout Standard Oni estas tro limigitaj se nur povas uzi \begin_inset Formula $P$ \end_inset , \begin_inset Formula $Q$ \end_inset , \begin_inset Formula $R$ \end_inset , ... por traduki frazojn al la logika lingvo. Kvantoroj ebligos nin uzi plurajn aliajn rimedojn. \layout Subsubsection Kio tio estas \layout Standard Mi ne ĉion povas klarigi, ĉar estas necesaj multaj aliaj konceptoj, sed mi iom klarigetos. Unue, kelkaj ŝanĝoj: \layout Standard Nun oni ne nur parolos pri ĝeneralaj okazoj ( \emph on pluvas \emph default , \emph on estas varma \emph default , ktp.), sed oni havos \emph on domajnon \emph default de konataj aĵoj, kaj diros kiu propreco estas vera por ĉiu elemento. \layout Standard Ekzemple: oni havas domajnon \begin_inset Formula $\{ p,\ t,\ r\}$ \end_inset , kiu rilatas respektive al \emph on PROLOG \emph default (logika programlingvo), al \emph on terminalo \emph default (ekrano kaj klavaro por uzi foran komputilon), kaj al \emph on retkarto \emph default (ilo por retigi komputilojn). \emph on p \emph default , \emph on t \emph default , \emph on r \emph default . \layout Standard Oni aldonas \emph on predikatan literon \emph default (ili ne plu estas nomataj \emph on propoziciaj literoj \emph default ) \begin_inset Formula $E$ \end_inset , tiel ke esprimo \begin_inset Formula $Ex$ \end_inset (legata \begin_inset Quotes eld \end_inset \emph on \begin_inset Formula $E$ \end_inset de \begin_inset Formula $x$ \end_inset \emph default (ikso) \begin_inset Quotes erd \end_inset , skribita kune) signifas ke \emph on \begin_inset Formula $x$ \end_inset estas ia ekipaĵo (komputila) \emph default . Ankaŭ oni havos \begin_inset Formula $Sx$ \end_inset por esprimi ke \emph on \begin_inset Formula $x$ \end_inset estas ia softvaro \emph default , kaj \begin_inset Formula $Tx$ \end_inset kiu signifos \emph on \begin_inset Formula $x$ \end_inset estas teksto-tradukilo \emph default (softvaro por aŭtomate traduki tekstojn). \layout Standard Nun oni scias ke certas \begin_inset Formula $Et$ \end_inset , \begin_inset Formula $Er$ \end_inset , \begin_inset Formula $Sp$ \end_inset kaj neniu alia. \layout Standard Kvantoroj ebligos nin skribi veraĵojn kiuj priparolas pri kelkaj elementoj el domajno. Estas du kvantoroj: \layout Itemize Universala kvantoro: \begin_inset Formula $\forall$ \end_inset . Kiam oni metas \begin_inset Formula $\forall xPx$ \end_inset ( \begin_inset Quotes eld \end_inset \emph on por ĉiu \begin_inset Formula $x$ \end_inset , \begin_inset Formula $P$ \end_inset de \begin_inset Formula $x$ \end_inset \emph default \begin_inset Quotes erd \end_inset ), oni volas esprimi ke ĉiuj elementoj el domajno certigas la proprecon \begin_inset Formula $P$ \end_inset . \layout Itemize Ekzistokvantoro: \begin_inset Formula $\exists$ \end_inset . \begin_inset Formula $\exists xPx$ \end_inset ( \begin_inset Quotes eld \end_inset \emph on ekzistas \begin_inset Formula $x$ \end_inset kia \begin_inset Formula $P$ \end_inset de \begin_inset Formula $x$ \end_inset \emph default \begin_inset Quotes erd \end_inset ) signifas ke almenaŭ unu elemento el domajno certigas la proprecon \begin_inset Formula $P$ \end_inset . \layout Standard Ekzemple, ĉi tie estas certaj la jenaj formuloj: \begin_inset Formula $\forall x(Ex\vee Sx)$ \end_inset , \begin_inset Formula $\neg\exists xTx$ \end_inset , \begin_inset Formula $\forall x(Tx\Rightarrow\neg Ex)$ \end_inset , \begin_inset Formula $\exists xEx\wedge\exists xSx$ \end_inset kaj multaj aliaj. Kvantoroj havas saman prioritaton ol la \begin_inset Formula $\neg$ \end_inset . \layout Standard Reguloj tie klarigitaj prilaboros nur kun \emph on liberaj anstataŭigoj \emph default . Pardonu min pro ne klarigi kion tio signifas, sed mi ne volas devojiĝi de la temo. \layout Subsubsection Enigo de ekzistokvantoro \layout Standard Se oni vidas pruvon de ekzisto, oni rajtas diri ke iu propreco certas pro almenaŭ unu elemento: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch*} \layout Standard n & A \backslash {t/x \backslash } \backslash \backslash \layout Standard \backslash hline \layout Standard & \backslash exists x A & I$ \backslash exists$ n,t \layout Standard \backslash end{fitch*} \backslash ] \end_inset \layout Standard Tio \begin_inset Formula $A\{ t/x\}$ \end_inset estas \emph on anstataŭigo \emph default (legata \begin_inset Quotes eld \end_inset \emph on \begin_inset Formula $t$ \end_inset super \begin_inset Formula $x$ \end_inset \emph default \begin_inset Quotes erd \end_inset , temas pri ŝanĝi \begin_inset Formula $x$ \end_inset al \begin_inset Formula $t$ \end_inset ). \layout Standard Tiu regulo esprimas ke se oni vidas \begin_inset Formula $At$ \end_inset , kie \begin_inset Formula $t$ \end_inset estas elemento, oni povas aserti ke \begin_inset Formula $\exists xAx$ \end_inset , ĉar kiam \begin_inset Formula $x$ \end_inset estas \begin_inset Formula $t$ \end_inset ja certas la propreco. \layout Subsubsection Forigo de ekzistokvantoro \layout Standard Eltiri ion certan el \begin_inset Formula $\exists xPx$ \end_inset iom kostas, sed oni agas tiel: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch*} \layout Standard m & \backslash exists x A \backslash \backslash \layout Standard n & \backslash fh A \backslash {a/x \backslash } & H \backslash \backslash \layout Standard p & \backslash fa B \backslash \backslash \layout Standard \backslash hline \layout Standard & B & E$ \backslash exists$ m,n,p,a \layout Standard \backslash end{fitch*} \backslash ] \end_inset \layout Standard Do, se unu el la pluraj \begin_inset Formula $A$ \end_inset entenas \begin_inset Formula $B$ \end_inset , tiam oni scias ke \begin_inset Formula $B$ \end_inset , ĉar ja konas ke unu el la \begin_inset Formula $A$ \end_inset certas. Laŭ teknikaj teorioj, ne rajtas aperi iun \begin_inset Formula $a$ \end_inset ĉe \begin_inset Formula $B$ \end_inset nek ĉe iu atingebla hipotezo. \layout Subsubsection Enigo de universala kvantoro \layout Standard Tiu ja estas facila: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch*} \layout Standard n & A \backslash \backslash \layout Standard \backslash hline \layout Standard & \backslash forall x A & I$ \backslash forall$ n \layout Standard \backslash end{fitch*} \backslash ] \end_inset \layout Standard Do, se \begin_inset Formula $A$ \end_inset ĉiam certas, tiam certas por ajna valoro de \begin_inset Formula $x$ \end_inset . Neniu \emph on libera \emph default \begin_inset Formula $x$ \end_inset aperu en atingebla hipotezo (pardonu tiajn \begin_inset Quotes eld \end_inset kriptajn \begin_inset Quotes erd \end_inset frazojn, sed ili estas parto de teorio). \layout Subsubsection Forigo de universala kvantoro \layout Standard Ankaŭ facile komprenebla: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch*} \layout Standard n & \backslash forall x A \backslash \backslash \layout Standard \backslash hline \layout Standard & A \backslash {t/x \backslash } & E$ \backslash forall$ n,t \layout Standard \backslash end{fitch*} \backslash ] \end_inset \layout Standard Se oni scias ke \begin_inset Formula $A$ \end_inset certas por ĉiuj elementoj, tiam oni povas elekti iun ajn elementon kaj scios ke \begin_inset Formula $A$ \end_inset certas en tiu elemento. \layout Subsubsection Ekzemploj \layout Standard Ĉe la lasta sekcio estas kelkaj ekzemploj kun kvantoroj, sed ne klarigitaj. Plej eble vi devos konsulti ian logikan libron se vi celas kompreni ilin. \layout Subsection Malbazaj reguloj \layout Standard Ĉe multaj libroj kaj kursetoj oni havas plurajn derivregulojn (alie al la 9 bazaj) kiuj ebligas pli rapide labori kun formuloj. Ili prezentas abstrakton: forlasi pensi en detalojn por dediĉiĝi al pli kompleksajn problemojn (kiel ĉe la \emph on altnivelajn \emph default programlingvojn). \layout Standard Se vi decidas uzi ilin, vi malhavis plurajn farendaĵojn, sed vi pli frue finos. Mia konsilo estas uzu regulon nur se vi eblas pruvi ĝian validecon per la 9 bazaj reguloj. \layout Standard Iuj kiuj mi trovis ie estas: \layout Itemize \emph on Duobla nego \emph default : ebligas ŝanĝi \begin_inset Formula $A$ \end_inset al \begin_inset Formula $\neg\neg A$ \end_inset kaj reciproke. \layout Itemize \emph on Modus Tollens \emph default : havante \begin_inset Formula $A\Rightarrow B$ \end_inset kaj \begin_inset Formula $\neg B$ \end_inset , tiam \begin_inset Formula $\neg A$ \end_inset . \layout Itemize \emph on Silogismo disjunkcia \emph default : se \begin_inset Formula $A\vee B$ \end_inset kaj \begin_inset Formula $\neg A$ \end_inset , do \begin_inset Formula $B$ \end_inset . Kaj se \begin_inset Formula $A\vee B$ \end_inset kaj \begin_inset Formula $\neg B$ \end_inset , tiam do \begin_inset Formula $A$ \end_inset . \layout Itemize \emph on Forigo de \begin_inset Formula $\neg$ \end_inset \begin_inset Formula $\Rightarrow$ \end_inset \emph default : se oni havas \begin_inset Formula $\neg(A\Rightarrow B)$ \end_inset , tiam ankaŭ \begin_inset Formula $A$ \end_inset kaj \begin_inset Formula $\neg B$ \end_inset okazas. \layout Itemize \emph on Forigo de \begin_inset Formula $\neg$ \end_inset \begin_inset Formula $\vee$ \end_inset \emph default : se oni havas \begin_inset Formula $\neg(A\vee B)$ \end_inset , tiam \begin_inset Formula $\neg A$ \end_inset , kaj ankaŭ \begin_inset Formula $\neg B$ \end_inset . \layout Itemize \emph on Forigo de \begin_inset Formula $\neg\wedge$ \end_inset \emph default : se oni havas \begin_inset Formula $\neg(A\wedge B)$ \end_inset , tiam \begin_inset Formula $\neg A\vee\neg B$ \end_inset . \layout Itemize \emph on Aliaj teoremoj \emph default : \begin_inset Formula $A\Rightarrow A$ \end_inset , \begin_inset Formula $A\vee\neg A$ \end_inset , \begin_inset Formula $\neg(A\wedge\neg A)$ \end_inset kaj aliaj. \layout Itemize \emph on Anstataŭigo de ekvivalentaj formuloj \emph default : se \begin_inset Formula $A\Longleftrightarrow B$ \end_inset , tiam kie diras \begin_inset Formula $A$ \end_inset oni povas meti \begin_inset Formula $B$ \end_inset kaj reciproke. \layout Standard Kvankam aliaj ekzistas, se oni demandas ekzercon al vi, oni jam diros kiuj reguloj estas permesitaj kaj kiuj ne (ekzemple, al ni oni permesis uzi nur la bazajn). \layout Section Ekstra \layout Standard Se vi jam konis ĉion kion mi aldiris, aŭ dubas pri temoj aliaj al la agmaniero de natura dedukto, restu ĉe tiu sekcio. \layout Subsection Kial nomiĝas naturan dedukton? \layout Standard Ĉar la rimedojn oni uzas estas la samaj kiujn homoj faras dumpense. \layout Standard Rimarku la klarigitajn ekzercojn. Esprimu la derivojn per vortoj, diru ilin al iu, kaj fine li/ŝi diros vin ke \begin_inset Quotes eld \end_inset \emph on kompreneble, ĉar ... \emph default \begin_inset Quotes erd \end_inset . Vi vidos ke iu ajn eblas rakonti kiel uzu iujn el la 9 reguloj, eĉ malkonante ilian nomon aŭ ekzistecon. \layout Standard Do, por diveni kiel fari ekzercon pri natura dedukto, forgesu regulojn de \emph on enigo \emph default kaj \emph on forigo \emph default , kaj pensu normale, ŝanĝante la literojn per simplaj agoj, se necese. Estas utile pensi pri agoj kiel \emph on pluvas \emph default , \emph on ne pluvas \emph default , \emph on estas sune \emph default , \emph on mi sekas \emph default , ... pro esti simplaj vortoj kiujn ĉiu homo povas bone kompreni, kaj alie, estas facile rilati agojn kiel \emph on ne malsekiĝi \emph default kun \emph on esti sune kaj ne pluvi \emph default , aŭ eĉ kun pli kompleksaj formuloj. \layout Subsection Ĉu la solvo estas nura? \layout Standard Ne. Ju pli kompleksa estas la ekzerco, des pli aliaj manieroj solvi ĝin ekzistas. Ĉe la sekcio pri klarigitaj ekzercoj, mi metis plurajn solvojn por iu ekzerco. \layout Standard Kompreneble, vi povas deduktadi veraĵojn kiuj tute malutilas, kaj atingos alian solvon. Tamen, estas plej bone provi fari ĉiun ekzercon plej eble mallonge. \layout Subsection Aliaj rimedoj por pruvi validecon \layout Standard Natura dedukto estas maniero pruvi la validecon de derivo, sed ne estas la sola rimedo. Jen aliaj: \layout Subsubsection Brutforte \layout Standard Eblas listi la tutajn aranĝaĵojn de valoroj por ĉiu variablo kaj pruvi ke, por ĉiu el ili, se la maldekstra parto de la derivo certas tiam la dekstra parto ankaŭ certas. \layout Standard Por \begin_inset Formula $n$ \end_inset variabloj, estos pruvendaj \begin_inset Formula $2^{n}$ \end_inset okazoj. \layout Standard Tamen, kvantoroj jen estas problemo, ĉar jam partoprenas domajno. Kaj estas neeble listi iajn domajnon, ĉar domajno povas enhavi infinitojn elementojn. \layout Subsubsection Teoremo de refuto \layout Standard Teoremo de refuto diras ke \begin_inset Formula $\Gamma\vDash A\Longleftrightarrow\ \nVdash\Gamma,\neg A$ \end_inset . \layout Standard Pervorte: aro da formuloj \begin_inset Formula $\Gamma$ \end_inset ( \emph on gamma \emph default ) havas kiel sekvo \begin_inset Formula $A$ \end_inset \emph on se kaj nur se \emph default la sistemo formata per \begin_inset Formula $\Gamma$ \end_inset kune de \begin_inset Formula $\neg A$ \end_inset estas malplenumebla. \layout Standard Tio pri kiel pruvi \emph on malplenumeblo \emph default estas alia temo, iom longa, kiel ĝia nomo sugestas. Unu el la facilaj rimedoj estas uzi arbon de klaŭza \emph on rezolucio \emph default . \layout Subsection Kiel pruvi nevalidecon \layout Standard Natura dedukto aldonas procedon por pruvi ke rezonado estas korekta, sed, kial oni pruvas ke rezonado estas malkorekta? Natura dedukto tion ne ebligas. \layout Standard Jen la nuna okazo: oni havas derivon \begin_inset Formula $\Gamma\vdash A$ \end_inset , kaj kredas ke ekzistas \emph on modelo \emph default (aro da valoroj) kiu certigas \begin_inset Formula $\Gamma$ \end_inset - \emph on gamma \emph default - sed ne al \begin_inset Formula $A$ \end_inset . Nu, oni nur devas trovi ĝin por pruvi ke tiu derivo estas nevalida. Al tiu modelo oni nomas \emph on kontraŭmodelo \emph default , kaj estas trovebla per pluraj rimedoj. Mi kredas ke la plej facila estas \emph on intuicie \emph default : provadi kelkajn valorojn kiuj ŝajnas kontraŭmodelon, ĝis oni trovu unu. \layout Standard Ekzemple, \begin_inset Formula $\neg P\Rightarrow\neg Q,\ \neg Q\vdash\neg P\vee Q$ \end_inset estas nevalida ( \begin_inset Formula $\nvDash$ \end_inset ), ĉar kiam \begin_inset Formula $P$ \end_inset certas kaj \begin_inset Formula $Q$ \end_inset falsas, tio el maldekstre ( \emph on premisoj \emph default ) estas certa, sed tio el dekstre ( \emph on konkludo \emph default ) estas falsa, do \begin_inset Formula $\neg P\vee Q$ \end_inset ne estas sekvo de tio el maldekstre. \layout Subsection Kreu viajn ekzercojn \layout Standard Se vi jam legis kaj lernis ĉiujn ekzemplojn el tiu dokumento, jen eraro! Nun vi mankas ekzercojn por praktiki vi mem. \layout Standard Vi ja povas elpensi derivojn kaj provi pruvi ilian validecon; sed plej malfeliĉe , se ili ne estas validaj, vi pasos tro da tempo malutile. Vi devas elpensi derivojn ja validajn, kaj poste pruvi ilin korekte. \layout Standard Kelkaj metodoj por tion atingi estas: \layout Itemize Se \begin_inset Formula $A$ \end_inset kaj \begin_inset Formula $B$ \end_inset estas la sama formulo, sed verkita per aliaj ekvivalentaj formoj, provu pruvi \begin_inset Formula $A\vDash B$ \end_inset aŭ \begin_inset Formula $B\vDash A$ \end_inset . \layout Itemize Prenu veraĵon kaj pruvu ĝin. Ekzemple: \begin_inset Formula $\vdash P\wedge P\Rightarrow P\vee P$ \end_inset . \layout Itemize Prenu malveraĵon, negi ĝin, kaj pruvu tiun formulon. Jen ekzemplo: \begin_inset Formula $\neg(A\wedge(A\Rightarrow B)\wedge\neg B)$ \end_inset . Tiu metodo farigos vin praktiki la \emph on redukto al absurdo \emph default . \layout Itemize Transformu iun formulon al ĝia \emph on norma kaja formo \emph default (ĝi restos kia \emph on io \begin_inset Formula $\wedge$ \end_inset io \begin_inset Formula $\wedge$ \end_inset ... \begin_inset Formula $\wedge$ \end_inset io \emph default ). Tiam vi havas kelkajn formulojn kiuj certas samtempe: ĉiu el la kajeroj. Vi povas preni unu el ili kaj aserti ke kiam la originala formulo certas, tiam tiu kajero ankaŭ certas. \layout Itemize Prenu plurajn formulojn hazarde, kaj supozu ke ĉiuj certas samtempe. Por tion fari, krei ilian konjunkcion ( \emph on unu \emph default \begin_inset Formula $\wedge$ \end_inset \emph on alia \emph default \begin_inset Formula $\wedge$ \end_inset \emph on alia \emph default \begin_inset Formula $\wedge$ \end_inset \emph on ... \emph default ). Tiun formulegon vi povas modifi per la antaŭaj metodoj por serĉi sekvojn. Ĉi ĉio vin utilos por praktiki naturan dedukton kun \emph on pluraj \emph default formuloj certaj maldekstre de la derivo. \layout Subsection Programoj kiuj faras naturan dedukton \layout Standard Ĉu ekzistas komputilaj programoj por fari ĉio kio mi klarigis, sed senpense aŭ senlabore? Nu, mi ne vere scias; mi konas neniun. Ĉiujn ekzemplojn ĉi tie mi faris mi mem, klopodinte. \layout Standard Oni povas provi funkciigi ion kia \begin_inset ERT status Collapsed \layout Standard \backslash htmladdnormallinkfoot{seqprover}{http://bach.istc.kobe-u.ac.jp/seqprover/} \end_inset aŭ \begin_inset ERT status Collapsed \layout Standard \backslash htmladdnormallinkfoot{pandora}{http://www.doc.ic.ac.uk/~yg/projects/AI/prover.html} \end_inset . Mi malatingis tion, kaj iomete mi trovis malfinitajn projektojn. Supozeble, estas malfacila fari tian programon, ĉar dedukto estu \emph on natura \emph default (plej taŭga por homaj mensoj). Tamen, komputiloj ebligas apliki brutforton... \layout Standard Kion vi ja povas provi, kaj bone funkcias, estas \begin_inset ERT status Collapsed \layout Standard \backslash htmladdnormallinkfoot{ludo}{http://www.winterdrache.de/freeware/domino/} \end_inset simila al domeno kiu utilas por pruvi derivojn per koloraj pecoj. Ĝi bezonas iom da prilernado. \layout Section Ekzemploj, pluraj ekzemploj \layout Standard Finonte, mi metas ĉi tie kolekton da multaj ekzemploj (senkomente). Estas faritaj de mi, do se vi ektrovas erarojn, sciigu min. \layout Standard La unuaj 14 estas klarigitaj pervorte ĉe sekcio 5. \layout Subsection \begin_inset Formula $P,\ P\Rightarrow Q\vdash P\wedge Q$ \end_inset \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard P \backslash \backslash \layout Standard P \backslash Rightarrow Q \backslash \backslash \layout Standard Q & E$ \backslash Rightarrow$ 2,1 \backslash \backslash \layout Standard P \backslash wedge Q & I$ \backslash wedge$ 1,3 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Subsection \begin_inset Formula $P\wedge Q\Rightarrow R,\ Q\Rightarrow P,\ Q\vdash R$ \end_inset \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard P \backslash wedge Q \backslash Rightarrow R \backslash \backslash \layout Standard Q \backslash Rightarrow P \backslash \backslash \layout Standard Q \backslash \backslash \layout Standard P & E$ \backslash Rightarrow$ 2,3 \backslash \backslash \layout Standard P \backslash wedge Q & I$ \backslash wedge$ 4,3 \backslash \backslash \layout Standard R & E$ \backslash Rightarrow$ 1,5 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Subsection \begin_inset Formula $P\Rightarrow Q,\ Q\Rightarrow R\vdash P\Rightarrow Q\wedge R$ \end_inset \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard P \backslash Rightarrow Q \backslash \backslash \layout Standard Q \backslash Rightarrow R \backslash \backslash \layout Standard \backslash fh P & H \backslash \backslash \layout Standard \backslash fa Q & E$ \backslash Rightarrow$ 1,3 \backslash \backslash \layout Standard \backslash fa R & E$ \backslash Rightarrow$ 2,4 \backslash \backslash \layout Standard \backslash fa Q \backslash wedge R & I$ \backslash wedge$ 4,5 \backslash \backslash \layout Standard P \backslash Rightarrow Q \backslash wedge R & I$ \backslash Rightarrow$ 3,6 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Subsection \begin_inset Formula $P\vdash Q\Rightarrow P$ \end_inset \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard P \backslash \backslash \layout Standard \backslash fh Q & H \backslash \backslash \layout Standard \backslash fa P & IT 1 \backslash \backslash \layout Standard Q \backslash Rightarrow P & I$ \backslash Rightarrow$ 2,3 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Subsection \begin_inset Formula $P\Rightarrow Q,\ \neg Q\vdash\neg P$ \end_inset \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard P \backslash Rightarrow Q \backslash \backslash \layout Standard \backslash neg Q \backslash \backslash \layout Standard \backslash fh P & H \backslash \backslash \layout Standard \backslash fa Q & E$ \backslash Rightarrow$ 1,3 \backslash \backslash \layout Standard \backslash fa \backslash neg Q & IT 2 \backslash \backslash \layout Standard \backslash neg P & I$ \backslash neg$ 3,4,5 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Subsection \begin_inset Formula $P\Rightarrow(Q\Rightarrow R)\vdash Q\Rightarrow(P\Rightarrow R)$ \end_inset \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard P \backslash Rightarrow (Q \backslash Rightarrow R) \backslash \backslash \layout Standard \backslash fh Q & H \backslash \backslash \layout Standard \backslash fa \backslash fh P & H \backslash \backslash \layout Standard \backslash fa \backslash fa Q \backslash Rightarrow R & E$ \backslash Rightarrow$ 1,3 \backslash \backslash \layout Standard \backslash fa \backslash fa R & E$ \backslash Rightarrow$ 4,2 \backslash \backslash \layout Standard \backslash fa P \backslash Rightarrow R & I$ \backslash Rightarrow$ 3,5 \backslash \backslash \layout Standard Q \backslash Rightarrow (P \backslash Rightarrow R) & I$ \backslash Rightarrow$ 2,6 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Subsection \begin_inset Formula $P\vee(Q\wedge R)\vdash P\vee Q$ \end_inset \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard P \backslash vee (Q \backslash wedge R) \backslash \backslash \layout Standard \backslash fh P & H \backslash \backslash \layout Standard \backslash fa P \backslash vee Q & I$ \backslash vee$ 2 \backslash \backslash \layout Standard \backslash fh Q \backslash wedge R & H \backslash \backslash \layout Standard \backslash fa Q & E$ \backslash wedge$ 4 \backslash \backslash \layout Standard \backslash fa P \backslash vee Q & I$ \backslash vee$ 5 \backslash \backslash \layout Standard P \backslash vee Q & E$ \backslash vee$ 1,3,6 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Subsection \begin_inset Formula $L\wedge M\Rightarrow\neg P,\ I\Rightarrow P,\ M,\ I\vdash\neg L$ \end_inset \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard L \backslash wedge M \backslash Rightarrow \backslash neg P \backslash \backslash \layout Standard I \backslash Rightarrow P \backslash \backslash \layout Standard M \backslash \backslash \layout Standard I \backslash \backslash \layout Standard \backslash fh L & H \backslash \backslash \layout Standard \backslash fa L \backslash wedge M & I$ \backslash wedge$ 5,3 \backslash \backslash \layout Standard \backslash fa \backslash neg P & E$ \backslash Rightarrow$ 1,6 \backslash \backslash \layout Standard \backslash fa P & E$ \backslash Rightarrow$ 2,4 \backslash \backslash \layout Standard \backslash neg L & I$ \backslash neg$ 5,7,8 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Subsection \begin_inset Formula $\vdash P\Rightarrow P$ \end_inset \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard \backslash fh P & H \backslash \backslash \layout Standard \backslash fa P & IT 1 \backslash \backslash \layout Standard P \backslash Rightarrow P & I$ \backslash Rightarrow$ 1,2 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Subsection \begin_inset Formula $\vdash\neg(P\wedge\neg P)$ \end_inset \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard \backslash fh P \backslash wedge \backslash neg P & H \backslash \backslash \layout Standard \backslash fa P & E$ \backslash wedge$ 1 \backslash \backslash \layout Standard \backslash fa \backslash neg P & E$ \backslash wedge$ 1 \backslash \backslash \layout Standard \backslash neg (P \backslash wedge \backslash neg P) & I$ \backslash neg$ 1,2 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Subsection \begin_inset Formula $\vdash P\vee\neg P$ \end_inset \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard \backslash fh \backslash neg (P \backslash vee \backslash neg P) & H \backslash \backslash \layout Standard \backslash fa \backslash fh P & H \backslash \backslash \layout Standard \backslash fa \backslash fa P \backslash vee \backslash neg P & I$ \backslash vee$ 2 \backslash \backslash \layout Standard \backslash fa \backslash fa \backslash neg (P \backslash vee \backslash neg P) & IT 1 \backslash \backslash \layout Standard \backslash fa \backslash neg P & I$ \backslash neg$ 2,3,4 \backslash \backslash \layout Standard \backslash fa P \backslash vee \backslash neg P & I$ \backslash vee$ 5 \backslash \backslash \layout Standard \backslash fa \backslash neg (P \backslash vee \backslash neg P) & IT 1 \backslash \backslash \layout Standard \backslash neg \backslash neg (P \backslash vee \backslash neg P) & I$ \backslash neg$ 1,6,7 \backslash \backslash \layout Standard P \backslash vee \backslash neg P & E$ \backslash neg$ 8 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Subsection \begin_inset Formula $P\vee Q,\ \neg P\vdash Q$ \end_inset \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard P \backslash vee Q \backslash \backslash \layout Standard \backslash neg P \backslash \backslash \layout Standard \backslash fh P & H \backslash \backslash \layout Standard \backslash fa \backslash fh \backslash neg Q & H \backslash \backslash \layout Standard \backslash fa \backslash fa \backslash neg P & IT 2 \backslash \backslash \layout Standard \backslash fa \backslash fa P & IT 3 \backslash \backslash \layout Standard \backslash fa \backslash neg \backslash neg Q & I$ \backslash neg$ 4,5,6 \backslash \backslash \layout Standard \backslash fa Q & E$ \backslash neg$ 7 \backslash \backslash \layout Standard \backslash fh Q & H \backslash \backslash \layout Standard \backslash fa Q & IT 9 \backslash \backslash \layout Standard Q & E$ \backslash vee$ 1,8,10 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Subsection \begin_inset Formula $A\vee B,\ A\Rightarrow C,\ \neg D\Rightarrow\neg B\vdash C\vee D$ \end_inset \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard A \backslash vee B \backslash \backslash \layout Standard A \backslash Rightarrow C \backslash \backslash \layout Standard \backslash neg D \backslash Rightarrow \backslash neg B \backslash \backslash \layout Standard \backslash fh A & H \backslash \backslash \layout Standard \backslash fa C & E$ \backslash Rightarrow$ 2,4 \backslash \backslash \layout Standard \backslash fa C \backslash vee D & I$ \backslash vee$ 5 \backslash \backslash \layout Standard \backslash fh B & H \backslash \backslash \layout Standard \backslash fa \backslash fh \backslash neg D & H \backslash \backslash \layout Standard \backslash fa \backslash fa \backslash neg B & E$ \backslash Rightarrow$ 3,8 \backslash \backslash \layout Standard \backslash fa \backslash fa B & IT 7 \backslash \backslash \layout Standard \backslash fa \backslash neg \backslash neg D & I$ \backslash neg$ 8,9,10 \backslash \backslash \layout Standard \backslash fa D & E$ \backslash neg$ 11 \backslash \backslash \layout Standard \backslash fa C \backslash vee D & I$ \backslash vee$ 12 \backslash \backslash \layout Standard C \backslash vee D & E$ \backslash vee$ 1,6,13 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Subsection \begin_inset Formula $A\Longleftrightarrow B\vdash(A\wedge B)\vee(\neg A\wedge\neg B)$ \end_inset \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard (A \backslash Rightarrow B) \backslash wedge (B \backslash Rightarrow A) \backslash \backslash \layout Standard \backslash fh \backslash neg (A \backslash vee \backslash neg A) & H \backslash \backslash \layout Standard \backslash fa \backslash fh A & H \backslash \backslash \layout Standard \backslash fa \backslash fa A \backslash vee \backslash neg A & I$ \backslash vee$ 3 \backslash \backslash \layout Standard \backslash fa \backslash fa \backslash neg (A \backslash vee \backslash neg A) & IT 2 \backslash \backslash \layout Standard \backslash fa \backslash neg A & I$ \backslash neg$ 3,4,5 \backslash \backslash \layout Standard \backslash fa A \backslash vee \backslash neg A & I$ \backslash vee$ 6 \backslash \backslash \layout Standard \backslash fa \backslash neg (A \backslash vee \backslash neg A) & IT 2 \backslash \backslash \layout Standard \backslash neg \backslash neg (A \backslash vee \backslash neg A) & I$ \backslash neg$ 2,7,8 \backslash \backslash \layout Standard A \backslash vee \backslash neg A & E$ \backslash neg$ 9 \backslash \backslash \layout Standard \backslash fh A & H \backslash \backslash \layout Standard \backslash fa A \backslash Rightarrow B & E$ \backslash wedge$ 1 \backslash \backslash \layout Standard \backslash fa B & E$ \backslash Rightarrow$ 12,11 \backslash \backslash \layout Standard \backslash fa A \backslash wedge B & I$ \backslash wedge$ 11,13 \backslash \backslash \layout Standard \backslash fa (A \backslash wedge B) \backslash vee ( \backslash neg A \backslash wedge \backslash neg B) & I$ \backslash vee$ 14 \backslash \backslash \layout Standard \backslash fh \backslash neg A & H \backslash \backslash \layout Standard \backslash fa \backslash fh B & H \backslash \backslash \layout Standard \backslash fa \backslash fa B \backslash Rightarrow A & E$ \backslash wedge$ 1 \backslash \backslash \layout Standard \backslash fa \backslash fa A & E$ \backslash Rightarrow$ 18,17 \backslash \backslash \layout Standard \backslash fa \backslash fa \backslash neg A & IT 16 \backslash \backslash \layout Standard \backslash fa \backslash neg B & I$ \backslash neg$ 17,19,20 \backslash \backslash \layout Standard \backslash fa \backslash neg A \backslash wedge \backslash neg B & I$ \backslash wedge$ 16,21 \backslash \backslash \layout Standard \backslash fa (A \backslash wedge B) \backslash vee ( \backslash neg A \backslash wedge \backslash neg B) & I$ \backslash vee$ 22 \backslash \backslash \layout Standard (A \backslash wedge B) \backslash vee ( \backslash neg A \backslash wedge \backslash neg B) & E$ \backslash vee$ 10,15,23 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Subsection \begin_inset Formula $P\vdash(P\Rightarrow Q)\Rightarrow Q$ \end_inset \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard P \backslash \backslash \layout Standard \backslash fh P \backslash Rightarrow Q & H \backslash \backslash \layout Standard \backslash fa Q & E$ \backslash Rightarrow$ 2,1 \backslash \backslash \layout Standard (P \backslash Rightarrow Q) \backslash Rightarrow Q & I$ \backslash Rightarrow$ 2,3 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Subsection \begin_inset Formula $P\Rightarrow Q\vdash(Q\Rightarrow R)\Rightarrow(P\Rightarrow R)$ \end_inset \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard P \backslash Rightarrow Q \backslash \backslash \layout Standard \backslash fh Q \backslash Rightarrow R & H \backslash \backslash \layout Standard \backslash fa \backslash fh P & H \backslash \backslash \layout Standard \backslash fa \backslash fa Q & E$ \backslash Rightarrow$ 1,3 \backslash \backslash \layout Standard \backslash fa \backslash fa R & E$ \backslash Rightarrow$ 2,4 \backslash \backslash \layout Standard \backslash fa P \backslash Rightarrow R & I$ \backslash Rightarrow$ 3,5 \backslash \backslash \layout Standard (Q \backslash Rightarrow R) \backslash Rightarrow (P \backslash Rightarrow R) & I$ \backslash Rightarrow$ 2,6 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Subsection \begin_inset Formula $P\Rightarrow Q,\ P\Rightarrow(Q\Rightarrow R)\vdash P\Rightarrow R$ \end_inset \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard P \backslash Rightarrow Q \backslash \backslash \layout Standard P \backslash Rightarrow (Q \backslash Rightarrow R) \backslash \backslash \layout Standard \backslash fh P & H \backslash \backslash \layout Standard \backslash fa Q & E$ \backslash Rightarrow$ 1,3 \backslash \backslash \layout Standard \backslash fa Q \backslash Rightarrow R & E$ \backslash Rightarrow$ 2,3 \backslash \backslash \layout Standard \backslash fa R & E$ \backslash Rightarrow$ 5,4 \backslash \backslash \layout Standard P \backslash Rightarrow R & I$ \backslash Rightarrow$ 3,6 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Subsection \begin_inset Formula $P\wedge Q\Rightarrow R\vdash P\Rightarrow(Q\Rightarrow R)$ \end_inset \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard P \backslash wedge Q \backslash Rightarrow R \backslash \backslash \layout Standard \backslash fh P & H \backslash \backslash \layout Standard \backslash fa \backslash fh Q & H \backslash \backslash \layout Standard \backslash fa \backslash fa P \backslash wedge Q & I$ \backslash wedge$ 2,3 \backslash \backslash \layout Standard \backslash fa \backslash fa R & E$ \backslash Rightarrow$ 1,4 \backslash \backslash \layout Standard \backslash fa Q \backslash Rightarrow R & I$ \backslash Rightarrow$ 3,5 \backslash \backslash \layout Standard P \backslash Rightarrow (Q \backslash Rightarrow R) & I$ \backslash Rightarrow$ 2,6 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Subsection \begin_inset Formula $\neg P\vdash P\Rightarrow Q$ \end_inset \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard \backslash neg P \backslash \backslash \layout Standard \backslash fh P & H \backslash \backslash \layout Standard \backslash fa \backslash fh \backslash neg Q & H \backslash \backslash \layout Standard \backslash fa \backslash fa \backslash neg P & IT 1 \backslash \backslash \layout Standard \backslash fa \backslash fa P & IT 2 \backslash \backslash \layout Standard \backslash fa \backslash neg \backslash neg Q & I$ \backslash neg$ 3,4,5 \backslash \backslash \layout Standard \backslash fa Q & E$ \backslash neg$ 6 \backslash \backslash \layout Standard P \backslash Rightarrow Q & I$ \backslash Rightarrow$ 2,7 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Subsection \begin_inset Formula $A\wedge(B\vee C)\vdash(A\wedge B)\vee(A\wedge C)$ \end_inset \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard A \backslash wedge (B \backslash vee C) \backslash \backslash \layout Standard A & E$ \backslash wedge$ 1 \backslash \backslash \layout Standard B \backslash vee C & E$ \backslash wedge$ 1 \backslash \backslash \layout Standard \backslash fh B & H \backslash \backslash \layout Standard \backslash fa A \backslash wedge B & I$ \backslash wedge$ 2,4 \backslash \backslash \layout Standard \backslash fa (A \backslash wedge B) \backslash vee (A \backslash wedge C) & I$ \backslash vee$ 5 \backslash \backslash \layout Standard \backslash fh C & H \backslash \backslash \layout Standard \backslash fa A \backslash wedge C & I$ \backslash wedge$ 2,7 \backslash \backslash \layout Standard \backslash fa (A \backslash wedge B) \backslash vee (A \backslash wedge C) & I$ \backslash vee$ 8 \backslash \backslash \layout Standard (A \backslash wedge B) \backslash vee (A \backslash wedge C) & E$ \backslash vee$ 3,6,9 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Subsection \begin_inset Formula $\neg A\vee B\vdash A\Rightarrow B$ \end_inset \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard \backslash neg A \backslash vee B \backslash \backslash \layout Standard \backslash fh A & H \backslash \backslash \layout Standard \backslash fa \backslash fh \backslash neg A & H \backslash \backslash \layout Standard \backslash fa \backslash fa \backslash fh \backslash neg B & H \backslash \backslash \layout Standard \backslash fa \backslash fa \backslash fa A & IT 2 \backslash \backslash \layout Standard \backslash fa \backslash fa \backslash fa \backslash neg A & IT 3 \backslash \backslash \layout Standard \backslash fa \backslash fa \backslash neg \backslash neg B & I$ \backslash neg$ 4,5,6 \backslash \backslash \layout Standard \backslash fa \backslash fa B & E$ \backslash neg$ 7 \backslash \backslash \layout Standard \backslash fa \backslash fh B & H \backslash \backslash \layout Standard \backslash fa \backslash fa B & IT 9 \backslash \backslash \layout Standard \backslash fa B & E$ \backslash vee$ 1,8,10 \backslash \backslash \layout Standard A \backslash Rightarrow B & I$ \backslash Rightarrow$ 2,11 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Subsection \begin_inset Formula $\vdash((P\Rightarrow Q)\Rightarrow P)\Rightarrow P$ \end_inset \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard \backslash fh (P \backslash Rightarrow Q) \backslash Rightarrow P & H \backslash \backslash \layout Standard \backslash fa \backslash fh \backslash neg P & H \backslash \backslash \layout Standard \backslash fa \backslash fa \backslash fh P & H \backslash \backslash \layout Standard \backslash fa \backslash fa \backslash fa \backslash fh \backslash neg Q & H \backslash \backslash \layout Standard \backslash fa \backslash fa \backslash fa \backslash fa P & IT 3 \backslash \backslash \layout Standard \backslash fa \backslash fa \backslash fa \backslash fa \backslash neg P & IT 2 \backslash \backslash \layout Standard \backslash fa \backslash fa \backslash fa \backslash neg \backslash neg Q & I$ \backslash neg$ 4,5,6 \backslash \backslash \layout Standard \backslash fa \backslash fa \backslash fa Q & E$ \backslash neg$ 7 \backslash \backslash \layout Standard \backslash fa \backslash fa P \backslash Rightarrow Q & I$ \backslash Rightarrow$ 3,8 \backslash \backslash \layout Standard \backslash fa \backslash fa P & E$ \backslash Rightarrow$ 1,9 \backslash \backslash \layout Standard \backslash fa \backslash fa \backslash neg P & IT 2 \backslash \backslash \layout Standard \backslash fa \backslash neg \backslash neg P & I$ \backslash neg$ 2,10,11 \backslash \backslash \layout Standard \backslash fa P & E$ \backslash neg$ 12 \backslash \backslash \layout Standard ((P \backslash Rightarrow Q) \backslash Rightarrow P) \backslash Rightarrow P & I$ \backslash Rightarrow$ 1,13 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Subsection \begin_inset Formula $Pa,\ Qa\vdash\exists x(Px\wedge Qx)$ \end_inset \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard Pa \backslash \backslash \layout Standard Qa \backslash \backslash \layout Standard Pa \backslash wedge Qa & I$ \backslash wedge$ 1,2 \backslash \backslash \layout Standard \backslash exists x(Px \backslash wedge Qx) & I$ \backslash exists$ 3,a \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Subsection \begin_inset Formula $\forall x(Px\Rightarrow Qx),\ Pa\vdash Qa$ \end_inset \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard \backslash forall x(Px \backslash Rightarrow Qx) \backslash \backslash \layout Standard Pa \backslash \backslash \layout Standard Pa \backslash Rightarrow Qa & E$ \backslash forall$ 1,a \backslash \backslash \layout Standard Qa & E$ \backslash Rightarrow$ 3,2 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Subsection \begin_inset Formula $\forall x(Px\Rightarrow Qx),\ \forall x(Qx\Rightarrow Rx)\vdash\forall x(Px\Rightarrow Rx),$ \end_inset \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard \backslash forall x(Px \backslash Rightarrow Qx) \backslash \backslash \layout Standard \backslash forall x(Qx \backslash Rightarrow Rx) \backslash \backslash \layout Standard \backslash fh Px & H \backslash \backslash \layout Standard \backslash fa Px \backslash Rightarrow Qx & E$ \backslash forall$ 1,x \backslash \backslash \layout Standard \backslash fa Qx \backslash Rightarrow Rx & E$ \backslash forall$ 2,x \backslash \backslash \layout Standard \backslash fa Qx & E$ \backslash Rightarrow$ 4,3 \backslash \backslash \layout Standard \backslash fa Rx & E$ \backslash Rightarrow$ 5,6 \backslash \backslash \layout Standard Px \backslash Rightarrow Rx & I$ \backslash Rightarrow$ 3,7 \backslash \backslash \layout Standard \backslash forall x(Px \backslash Rightarrow Rx) & I$ \backslash forall$ 8 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Subsection \begin_inset Formula $\exists x\forall yPxy\vdash\forall y\exists xPxy$ \end_inset \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard \backslash exists x \backslash forall yPxy \backslash \backslash \layout Standard \backslash fh \backslash forall yPay & H \backslash \backslash \layout Standard \backslash fa Pay & E$ \backslash forall$ 2,y \backslash \backslash \layout Standard \backslash fa \backslash exists xPxy & I$ \backslash exists$ 3,a \backslash \backslash \layout Standard \backslash exists xPxy & E$ \backslash exists$ 1,2,4,a \backslash \backslash \layout Standard \backslash forall y \backslash exists xPxy & I$ \backslash forall$ 5 \layout Standard \backslash end{fitch} \backslash ] \end_inset \the_end