#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 catalan \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 Introducció a la deducció natural \layout Author Daniel Clemente Laboreo \layout Date Agost 2004 (revisat en Maig 2005) \layout Standard \begin_inset LatexCommand \tableofcontents{} \end_inset \layout Section Abans de res... \layout Standard Aquest tutorial està disponible en molts idiomes: \begin_inset ERT status Collapsed \layout Standard \backslash htmladdnormallinkfoot{espanyol}{http://www.danielclemente.com/logica/dn.html} \backslash htmladdnormallink{(i PDF)}{http://www.danielclemente.com/logica/dn.pdf}, \backslash htmladdnormallinkfoot{esperanto}{http://www.danielclemente.com/logica/dn.eo.html} \backslash htmladdnormallink{(i PDF)}{http://www.danielclemente.com/logica/dn.eo.pdf}, \backslash htmladdnormallinkfoot{català}{http://www.danielclemente.com/logica/dn.ca.html} \backslash htmladdnormallink{(i PDF)}{http://www.danielclemente.com/logica/dn.ca.pdf}, i \backslash htmladdnormallinkfoot{anglès}{http://www.danielclemente.com/logica/dn.en.html} \backslash htmladdnormallink{(i PDF)}{http://www.danielclemente.com/logica/dn.en.pdf}. \layout Standard \layout Standard \end_inset \layout Standard Les fórmules queden molt més maques al PDF, però si no t'és possible usar-ho, mira les pàgines en HTML. \layout Subsection Qui soc \layout Standard Em dic Daniel Clemente Laboreo, tinc 19 anys (al 2004), visc a Gavà (Barcelona), i estudio informàtica a la \emph on FIB \emph default ( \emph on UPC \emph default ). Va ser allà, a l'assignatura \emph on ILO \emph default ( \emph on Introducció a la lògica \emph default ), on em van ensenyar tot aquest tema. \layout Subsection Per què escric això \layout Standard Per diversos motius: \layout Itemize Hi ha un buit important en buscar \begin_inset Quotes eld \end_inset \emph on deducció natural \emph default \begin_inset Quotes erd \end_inset al Google. Jo mateix vaig necessitar estudiar-ho abans de l'examen i no vaig trobar res útil que em pogués ajudar. El mateix amb \emph on natural deduction \emph default o \emph on nd \emph default : hi havia alguns tutorials, però cap ben fet: o no s'entenia, o tenia alguns caràcters especials que no es veien bé, o donaven tot per entès. Així que vaig proposar-me aportar aquest tutorial que segur que ajudarà a algú. \layout Itemize És un tema que m'agrada i que se'm dóna bé. \layout Itemize Fa pensar. Potser no té una gran utilitat pràctica, però realment fa falta esforçar-se i passar-hi molta estona per resoldre alguns problemes molt simples. \layout Itemize Bé, confesso que ho vaig escriure per aprendre a processar textos amb \begin_inset ERT status Collapsed \layout Standard \backslash LaTeX \end_inset . Costa bastant d'aprendre, però els resultats fan que valgui la pena. \layout Subsection A qui va dirigit \layout Standard En principi, a qualsevol a qui l'agradi la lògica, la informàtica, o les matemàtiques. Qui vulgui preparar-se per les assignatures de lògica de la universitat també guanyarà alguns conceptes útils. \layout Standard Aquest no pretén ser un curs complet de deducció natural, sinó que continuarà sent només una introducció. Quan aprengui més, el corregiré si cal, però no hi afegiré més seccions (les faria en documents apart). \layout Subsection Llicència \layout Standard Tot el document és \begin_inset ERT status Collapsed \layout Standard \backslash htmladdnormallinkfoot{FDL}{http://www.gnu.org/licenses/fdl.html} \end_inset (com la GPL del software lliure, però per documents). El codi font està fet amb LyX ( \begin_inset ERT status Collapsed \layout Standard \backslash htmladdnormallinkfoot{dn.ca.lyx}{http://www.danielclemente.com/logica/dn.ca.lyx} \end_inset ), i utilitza les macros \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. He usat el programa \begin_inset ERT status Collapsed \layout Standard \backslash htmladdnormallink{latex2html}{http://www.danielclemente.com/linux/l2h.html} \end_inset (lleugerament partxejat) per fer la web. \layout Standard El pots modificar o traduir a altres idiomes que coneguis bé, a més de poder redistribuir-lo, vendre'l, i moltes més coses. \layout Section Conceptes bàsics \layout Standard A això de la lògica s'ha de tenir perfectament clar el significat de cada paraula. Em limitaré a recordar què són i com es llegeixen els símbols estranys que s'usen en aquest document. \layout Subsection Formalització \layout Standard \emph on Formalitzar \emph default vol dir escriure una expressió d'una manera estàndard que tothom pugui entendre. \layout Standard Quan treballem amb algorismes lògics, podem estar pensant tota l'estona en frases com \begin_inset Quotes eld \end_inset \emph on Si plou i no tinc paraigua, llavors em mullo \emph default \begin_inset Quotes erd \end_inset . Es pot, però és massa llarg. És millor representar cada acció amb una lletra, i escriure la frase usant aquestes lletres junt amb paraules senzilles com \emph on i \emph default , \emph on o \emph default , \emph on no \emph default , o \emph on llavors \emph default . \layout Standard Exemple. Tenim aquest vocabulari: \layout Standard \begin_inset Formula $L$ \end_inset : \emph on ploure \layout Standard \begin_inset Formula $P$ \end_inset : \emph on tenir paraigua \layout Standard \begin_inset Formula $M$ \end_inset : \emph on mullar-se \layout Standard La frase \begin_inset Quotes eld \end_inset \emph on Si plou i no tinc paraigua, llavors em mullo \emph default \begin_inset Quotes erd \end_inset queda millor com a \begin_inset Quotes eld \end_inset \emph on si \begin_inset Formula $L$ \end_inset i no \begin_inset Formula $P$ \end_inset , llavors \begin_inset Formula $M$ \end_inset \emph default \begin_inset Quotes erd \end_inset . \layout Standard En deducció natural s'usarà només la versió de les lletres, amb aquestes condicions: \layout Itemize Les lletres (que s'anomenen \emph on lletres proposicionals \emph default ) van en majúscules. \layout Itemize S'acostumen a usar \begin_inset Formula $P$ \end_inset , \begin_inset Formula $Q$ \end_inset , \begin_inset Formula $R$ \end_inset , \begin_inset Formula $S$ \end_inset , ... però qualsevol altra és correcta. \layout Itemize Es posen uns símbols especials per als operadors \emph on i \emph default , \emph on o \emph default , \emph on no \emph default i \emph on implicació \emph default . \layout Subsection Símbols usats \layout Standard Per expressar les relacions entre una acció i una altra, hi ha uns quants dibuixets internacionals. Els operadors bàsics que has de conèixer són \begin_inset Formula $\vee$ \end_inset , \begin_inset Formula $\wedge$ \end_inset , \begin_inset Formula $\neg$ \end_inset , \begin_inset Formula $\Rightarrow$ \end_inset . Els altres són més complicats, però els he posat tots per quan hagis de consultar-los. \layout Standard \begin_inset Tabular \begin_inset Text \layout Standard \series bold Símbol \end_inset \begin_inset Text \layout Standard \series bold Llegit... \end_inset \begin_inset Text \layout Standard \series bold Descripció \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\vee$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on o \end_inset \begin_inset Text \layout Standard \begin_inset Formula $A\vee B$ \end_inset es compleix quan un dels dos, o tots dos, és cert. \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\wedge$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on i \end_inset \begin_inset Text \layout Standard Per a què \begin_inset Formula $A\wedge B$ \end_inset es compleixi, tant \begin_inset Formula $A$ \end_inset com \begin_inset Formula $B$ \end_inset han de ser certs. \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\neg$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on no \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\neg A$ \end_inset només es compleix quan \begin_inset Formula $A$ \end_inset és fals. \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\Rightarrow$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on implica \end_inset \begin_inset Text \layout Standard Indica una conseqüència. La expressió \begin_inset Formula $A\Rightarrow B$ \end_inset diu que quan \begin_inset Formula $A$ \end_inset es compleix, llavors \begin_inset Formula $B$ \end_inset també. A més, \begin_inset Formula $A\Rightarrow B$ \end_inset és cert excepte pel cas \begin_inset Formula $A$ \end_inset cert i \begin_inset Formula $B$ \end_inset fals. Per entendre-ho, pensa en un \begin_inset Formula $A$ \end_inset que impliqui \begin_inset Formula $B$ \end_inset i pregunta't: \emph on és possible que \begin_inset Formula $A$ \end_inset sigui cert i \begin_inset Formula $B$ \end_inset no? \emph default Tampoc et preocupis molt per això, no és important ara. \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\Longleftrightarrow$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on si i només si \end_inset \begin_inset Text \layout Standard \begin_inset Formula $A\Longleftrightarrow B$ \end_inset equival a \begin_inset Formula $(A\Rightarrow B)\wedge(B\Rightarrow A)$ \end_inset . Vol dir que de \begin_inset Formula $A$ \end_inset podem deduir \begin_inset Formula $B$ \end_inset i viceversa, o sigui, que són equivalents. \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\square$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on fals \end_inset \begin_inset Text \layout Standard El quadradet buit representa a \emph on fals \emph default (el \emph on 0 \emph default binari). Més tècnicament, representa a \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 cert \end_inset \begin_inset Text \layout Standard El quadradet ple representa a \emph on cert \emph default (l' \emph on 1 \emph default binari). Més tècnicament, representa a \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 existeix... \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\exists xPx$ \end_inset es llegeix \emph on existeix un \begin_inset Formula $x$ \end_inset tal que \begin_inset Formula $P$ \end_inset de \begin_inset Formula $x$ \end_inset \emph default . Si al nostre domini podem trobar un element (o més) tal que es compleixi la propietat \begin_inset Formula $P$ \end_inset aplicada a aquest element, llavors la fórmula és certa. \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\forall$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on per tot... \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\forall xPx$ \end_inset es llegeix \emph on per tot \begin_inset Formula $x$ \end_inset , \begin_inset Formula $P$ \end_inset de \begin_inset Formula $x$ \end_inset \emph default . Si tots els elements amb què treballem compleixen la propietat \begin_inset Formula $P$ \end_inset , llavors la fórmula és certa. \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\vdash$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on llavors \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\vdash$ \end_inset és el símbol del \emph on seqüent \emph default , que és la manera de dir \begin_inset Quotes eld \end_inset \emph on quan es compleix tot això de l'esquerra passa també tot allò de la dreta \emph default \begin_inset Quotes erd \end_inset . Hi ha seqüents vàlids, com \begin_inset Formula $P\wedge Q\vdash P$ \end_inset o com \begin_inset Formula $P\Rightarrow Q,\ Q\Rightarrow R,\ P\vdash P\wedge R$ \end_inset . També n'hi ha d'invàlids, com \begin_inset Formula $P\Rightarrow Q,\ \neg P\vdash\neg Q$ \end_inset . L'objectiu de la deducció natural és demostrar que un seqüent és vàlid. \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\vDash$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on vàlid \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\phi\vDash\varphi$ \end_inset serveix per dir que \begin_inset Formula $\varphi$ \end_inset és conseqüència lògica de \begin_inset Formula $\phi$ \end_inset , però quan s'escriu \begin_inset Formula $A\vDash B$ \end_inset , es vol dir que el seqüent \begin_inset Formula $A\vdash B$ \end_inset és vàlid; o sigui, que hem pogut demostrar-ho d'alguna manera, i ara es considera cert sota qualsevol interpretació dels símbols de predicat. \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\nvDash$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on invàlid \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\phi\nvDash\varphi$ \end_inset vol dir que \begin_inset Formula $\varphi$ \end_inset no és conseqüència lògica de \begin_inset Formula $\phi$ \end_inset . Si trobes una sèrie de valors ( \emph on model \emph default ) que faci cert a \begin_inset Formula $\phi$ \end_inset però fals a \begin_inset Formula $\varphi$ \end_inset , es demostra la invalidesa. \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\Vdash$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on satisfactible \end_inset \begin_inset Text \layout Standard Un conjunt de fórmules és satisfactible si existeix una sèrie de valors ( \emph on model \emph default ) que les faci certes a totes al mateix temps. \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\nVdash$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on insatisfactible \end_inset \begin_inset Text \layout Standard Un conjunt de fórmules és insatisfactible si no hi ha cap combinació de variables ( \emph on model \emph default ) que les faci totes certes al mateix temps. \end_inset \end_inset \layout Subsection Precedència dels operadors \layout Standard En veure una expressió, has de saber dir què és. Per exemple: \begin_inset Formula $A\vee B\Rightarrow C$ \end_inset és una implicació (no una disjunció!), perquè el \begin_inset Formula $\Rightarrow$ \end_inset és l'últim en evaluar-se (té menor prioritat que el \begin_inset Formula $\vee$ \end_inset ). \layout Standard Aquí poso els operadors, ordenats inversament per prioritat. \layout Itemize \begin_inset Formula $\Longleftrightarrow$ \end_inset \layout Itemize \begin_inset Formula $\Rightarrow$ \end_inset \layout Itemize \begin_inset Formula $\vee$ \end_inset i \begin_inset Formula $\wedge$ \end_inset (tenen la mateixa prioritat) \layout Itemize \begin_inset Formula $\neg$ \end_inset \layout Standard Això vol dir que \begin_inset Formula $\neg$ \end_inset és qui més \begin_inset Quotes eld \end_inset \emph on s'agarra \emph default \begin_inset Quotes erd \end_inset al símbol que acompanya. Un exemple de quan i on fan falta els parèntesis: \layout Standard \begin_inset Formula $P\vee\neg Q\Rightarrow R\wedge P\Longleftrightarrow\neg(R\vee S)\wedge A\Rightarrow B$ \end_inset és el mateix que \begin_inset Formula $(\ (P\vee(\neg Q))\ \Rightarrow\ (R\wedge P)\ )\Longleftrightarrow(\ ((\neg(R\vee S))\wedge A)\Rightarrow B\ )$ \end_inset \layout Standard Tranquil, no tornaré a utilitzar expressions tan llargues. \layout Section Deducció natural \layout Standard Ara toca explicar què és, com es fa, i si té cap utilitat. \layout Subsection Per a què serveix \layout Standard La deducció natural serveix per intentar demostrar que un raonament és correcte ( \begin_inset Quotes eld \end_inset \emph on per comprovar la validesa d'un seqüent \emph default \begin_inset Quotes erd \end_inset , diu la teoria). Exemple: \layout Standard Jo et dic: \begin_inset Quotes eld \end_inset \emph on A l'estiu fa calor, i ara estem a l'estiu, per tant fa calor \emph default \begin_inset Quotes erd \end_inset . Et poses a fer càlculs, i finalment dius: \begin_inset Quotes eld \end_inset \emph on Ja està, puc demostrar que el raonament que has fet és correcte \emph default \begin_inset Quotes erd \end_inset . Per a això serveix la deducció natural. \layout Standard No sempre és tan fàcil: \begin_inset Quotes eld \end_inset \emph on si suspens una assignatura, l'has de repetir. Si no l'estudies, la suspens. Suposem que no la repeteixes. Llavors, o l'estudies, o la suspens, o totes dues coses alhora \emph default \begin_inset Quotes erd \end_inset . Aquest raonament és vàlid i es pot demostrar amb la deducció natural. \layout Standard Fixa't que no cal que et creguis o entenguis tot allò que jo et digui. Per exemple, jo dic: \begin_inset Quotes eld \end_inset \emph on Els tiristors són petits i divertits; un cigró no és petit, així que no és un tiristor \emph default \begin_inset Quotes erd \end_inset . Encara que no sàpigues de què estic parlant, o et sembli una idiotesa (que ho és), has d'estar completament segur/a que el raonament és correcte. \layout Standard O sigui, que donada una suposició \begin_inset Quotes eld \end_inset \emph on si passa això llavors passa això altre \emph default \begin_inset Quotes erd \end_inset , la deducció natural permet dir \begin_inset Quotes eld \end_inset \emph on sí, així és \emph default \begin_inset Quotes erd \end_inset . En llenguatge lògic: si et donen un seqüent \begin_inset Formula $A\vdash B$ \end_inset , pots acabar concloent que és \begin_inset Formula $\vDash$ \end_inset ( \emph on vàlid \emph default ). Llavors s'escriu \begin_inset Formula $A\vDash B$ \end_inset ( \begin_inset Formula $A$ \end_inset té com a conseqüència \begin_inset Formula $B$ \end_inset ). \layout Subsection Per a què no serveix \layout Standard No serveix per demostrar la \emph on invalidesa \emph default d'una suposició. Si jo dic \begin_inset Quotes eld \end_inset \emph on si és de dia, no és de nit; i ara és de dia, per tant també és de nit \emph default \begin_inset Quotes erd \end_inset podràs passar-te una estona intentant provar les regles de la deducció natural, però sense aconseguir res útil. Al cap d'un temps aniràs intuint que probablement el raonament no sigui vàlid, i és llavors quan s'haurien de provar altres mètodes -que no són el de deducció natural- amb la fi de demostrar la invalidesa. Estan explicats més endavant. \layout Standard O sigui, que la deducció natural només serveix per demostrar la validesa, però no la invalidesa. Quina pena, no? \layout Standard Tampoc serveix per donar una bona resposta a la pregunta \begin_inset Quotes eld \end_inset \emph on Què passaria si...? \emph default \begin_inset Quotes erd \end_inset . Quan demanen demostrar la validesa de \begin_inset Formula $A\vdash B$ \end_inset , hem de pensar en què coses passarien si es complís \begin_inset Formula $A$ \end_inset , i si descobrim que una d'elles és \begin_inset Formula $B$ \end_inset , ja hem acabat. Però mai podrem donar una llista finita de totes aquestes coses. \layout Subsection Funcionament \layout Standard Es demana demostrar la validesa de \begin_inset Formula $\Gamma\vdash S$ \end_inset , on \begin_inset Formula $\Gamma$ \end_inset (es llegeix \emph on gamma \emph default ) és un grup de fórmules separades per comes, i \begin_inset Formula $S$ \end_inset és una sola fórmula. \layout Standard Partim de que totes les fórmules de \begin_inset Formula $\Gamma$ \end_inset són certes, i, mitjançant 9 regles concretes, podem anar descobrint què més coses són certes. La nostra intenció és veure que \begin_inset Formula $S$ \end_inset és certa; un cop aconseguit ja podrem acabar. \layout Standard Alguns cops no podrem treure veritats de cap lloc, i haurem de fer suposicions: \begin_inset Quotes eld \end_inset \emph on bé, no estic segur que \begin_inset Formula $A\wedge B$ \end_inset sigui sempre cert, però si es compleix \begin_inset Formula $C$ \end_inset , llavors sí que ho és \emph default \begin_inset Quotes erd \end_inset . Doncs ja hem descobert una altra cosa certa: que \begin_inset Formula $C\Rightarrow A\wedge B$ \end_inset . \layout Standard Com veus, sempre s'ha de pensar en cap a on volem dirigir-nos, perquè d'altra forma podríem endevinar un munt de coses que són certes però que no ens estan demanant. Per exemple, amb \begin_inset Formula $A\vee B,\ \neg A\vdash B$ \end_inset hem d'arribar a que \begin_inset Formula $B$ \end_inset és cert. Podem descobrir que \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 , i moltes més coses, però el que ens interessa és \begin_inset Formula $B$ \end_inset i res més. O sigui, que si no vas pel camí correcte, pots fer-te un embolic. \layout Subsection Notació \layout Standard Hi ha moltes maneres d'escriure els esquemes de deducció natural. Jo usaré l'estil Fitch, perquè és el que em van ensenyar, és fàcil d'entendre, i ocupa poc espai. És semblant a: \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 Amb això s'ha demostrat la validesa de \begin_inset Formula $P\Rightarrow Q,\ Q\Rightarrow R\vdash P\Rightarrow Q\wedge R$ \end_inset . \layout Standard L'esquema es va fent línia per línia, de dalt a baix. Els números de l'esquerra indiquen el número de línia, i sempre van en ordre. \layout Standard Les primeres línies contenen cadascuna de les fórmules que hi ha a la part esquerra del seqüent. En aquest cas són dues: \begin_inset Formula $P\Rightarrow Q$ \end_inset i \begin_inset Formula $Q\Rightarrow R$ \end_inset . A partir d'aquestes hem d'arribar a \begin_inset Formula $P\Rightarrow Q\wedge R$ \end_inset . \layout Standard A cada línia apuntem què cosa hem descobert certa, i a la dreta expliquem com l'hem trobada. Aquests símbols de la dreta (les \begin_inset Formula $E$ \end_inset i \begin_inset Formula $I$ \end_inset ) són les sigles que identifiquen a cadascuna de les 9 regles. Per exemple, aquí surten l' \emph on eliminació de la implicació \emph default ( \begin_inset Formula $E\Rightarrow$ \end_inset ), la \emph on introducció de la conjunció \emph default ( \begin_inset Formula $I\wedge$ \end_inset ), i la \emph on introducció de la implicació \emph default ( \begin_inset Formula $I\Rightarrow$ \end_inset ). Els numerets que les acompanyen donen informació sobre d'on s'han tret les fórmules necessàries per aplicar la regla. Són números de línia, o sigui, que per aplicar una regla hem de basar-nos en allò que ja hem escrit abans. \layout Standard Per últim, aquella ratlla vertical que va la línia 3 a la 6 és una hipòtesi (per això s'ha posat una \begin_inset Formula $H$ \end_inset a la dreta). Tot el que hi ha dins no és cert sempre, sinó només quan es compleix \begin_inset Formula $P$ \end_inset (l'encapçalament de la hipòtesi, a la línia 3). Per això, tot allò que fem dins de la hipòtesi no ho podem usar fora, perquè no sempre es compleix. \layout Standard El procediment acaba quan descobrim que és cert allò de la dreta del seqüent, en aquest cas \begin_inset Formula $P\Rightarrow Q\wedge R$ \end_inset (surt a l'última línia). \layout Section Les regles \layout Standard Aquí hi són enunciades i explicades les nou regles bàsiques que s'usen a la deducció natural. Indiquen quan i com podem afegir noves fórmules que segueixin sent certes. \layout Standard Els exemples (explicats) són a la següent secció. \layout Subsection Iteració \layout Standard Aquesta és una regla molt senzilla: \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 Sí, ho sé, escrit així queda bastant estrany, però és per a què serveixi com a definició. Això de dalt vol dir que si en la línia número \begin_inset Formula $n$ \end_inset tenim escrit \begin_inset Formula $A$ \end_inset (sigui l'expressió que sigui) llavors podem tornar a escriure \begin_inset Formula $A$ \end_inset a la línia actual, i per justificar-ho hem d'escriure a la dreta \begin_inset Formula $IT\ n$ \end_inset . \layout Standard Que per a què serveix això? Doncs de moment, per res, però tindrà la seva utilitat quan comencem a fer allò de les hipòtesis. Com que una hipòtesi és \emph on tancada \emph default , totes les regles hauran de treballar amb fórmules que es trobin dins de la hipòtesi. Si una fórmula està just a fora, la podem ficar dins amb això de la \emph on iteració \emph default . \layout Standard Alguns creuen que no és necessari gastar una línia així, però queda molt més clar quan s'usa. El que no s'accepta és usar-la només per \begin_inset Quotes eld \end_inset \emph on apropar \emph default \begin_inset Quotes erd \end_inset una fórmula que queda vàries línies per damunt: no fa falta tornar a escriure una línia si ja la tenim a dalt en la derivació actual. \layout Subsection Introducció de la conjunció \layout Standard La conjunció (que és la \emph on i \emph default ) la podem crear fàcilment: \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 Entén bé el funcionament de les figures com aquesta. Quan es posa una ratlla horitzontal llarga, normalment és per separar les \emph on premisses \emph default (a sobre) de la \emph on conclusió \emph default (a sota). Les premisses són les condicions que s'han de complir per aplicar la regla, i la conclusió (o \emph on resolvent \emph default ) el resultat de l'aplicació de la regla. \layout Standard Aquesta regla diu que si a una línia tenim escrita una cosa certa, i a una altra en tenim altra, també certa, llavors podem deixar escrit en una sola línia que ambdues coses són certes. Haurem d'anotar a la dreta les línies d'on hem tret la primera i la segona fórmula. \layout Standard Això és bastant lògic, no? Si sabem que és veritat que \emph on plou \emph default , i que és veritat que \emph on fa sol \emph default , aleshores no hi ha cap problema en dir que \emph on plou i fa sol \emph default (al mateix temps). Si alguna cosa no quadra, no és culpa nostra, sinó de qui ens ha dit que \emph on plou \emph default o que \emph on fa sol \emph default . \layout Standard Fixa't que agafant les línies al revés pots obtenir \begin_inset Formula $B\wedge A$ \end_inset , i que agafant la mateixa línia pots arribar a \begin_inset Formula $A\wedge A$ \end_inset i \begin_inset Formula $B\wedge B$ \end_inset , que també són certes. \layout Subsection Eliminació de la conjunció \layout Standard Això és justament l'operació contrària a l'anterior. Té dues parts. La primera: \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 I la segona, per si vols extreure \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 O sigui, que pots separar en vàries línies els \emph on conjuntands \emph default d'una conjunció (sí, s'utilitza aquesta paraulota). Per això la regla s'anomena \emph on eliminació de la conjunció \emph default , perquè d'una línia que conté símbols de conjunció ( \begin_inset Formula $\wedge$ \end_inset ) treus altres que ja no ho tenen, suposadament en un intent per apropar-te a allò que vols demostrar. \layout Subsection Introducció de la implicació \layout Standard Aquesta és més interessant, perquè permet fer quelcom útil amb les hipòtesis (aquelles subdemostracions que porten una barra vertical a l'esquerra). És: \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 I el que vol dir és que si hem suposat alguna cosa (diguem-li \begin_inset Formula $A$ \end_inset ), i hem descobert (mitjançant les regles) que suposar \begin_inset Formula $A$ \end_inset fa cert a \begin_inset Formula $B$ \end_inset (el que sigui), llavors tenim una cosa clara: no podem assegurar que \begin_inset Formula $B$ \end_inset sigui sempre cert, però sí que \begin_inset Formula $A$ \end_inset implica \begin_inset Formula $B$ \end_inset , que s'escriu \begin_inset Formula $A\Rightarrow B$ \end_inset . \layout Standard Això ens permet sortir de la subdemostració i continuar amb allò que estiguéssim fent. Recorda que no es pot acabar la deducció natural ficats a dins d'una subdemostr ació. \layout Subsection Eliminació de la implicació \layout Standard Aquesta regla és més senzilla ja que no té a veure amb suposicions sinó amb fets: \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 Simplement, si ens diuen que quan passa \begin_inset Formula $A$ \end_inset també passa \begin_inset Formula $B$ \end_inset (que és el que significa \begin_inset Formula $A\Rightarrow B$ \end_inset ), i també ens diuen que ara passa \begin_inset Formula $A$ \end_inset , aleshores podem assegurar que \begin_inset Formula $B$ \end_inset . \layout Standard A aquesta regla també se l'anomena \emph on modus ponens \emph default . \layout Subsection Introducció de la disjunció \layout Standard La disjunció (que és la \emph on o \emph default ) és molt fàcil però no òbvia: \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 Bé, per ser exacte, diré que també està disponible en l'altre ordre: \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 Què bonic, no? Si sabem que \begin_inset Quotes eld \end_inset \emph on avui és dijous \emph default \begin_inset Quotes erd \end_inset també sabem que \begin_inset Quotes eld \end_inset \emph on avui és dijous o les vaques volen \emph default \begin_inset Quotes erd \end_inset , \begin_inset Quotes eld \end_inset \emph on avui és dijous o divendres \emph default \begin_inset Quotes erd \end_inset , o fins i tot \begin_inset Quotes eld \end_inset \emph on avui és dijous... o no \emph default \begin_inset Quotes erd \end_inset . Totes són certes. \layout Standard Recorda que, quan parlem, gairebé sempre s'utilitza la \emph on o exclusiva \emph default ( \emph on XOR \emph default ), que es compleix si un dels dos \emph on disjuntands \emph default és cert però no quan tots dos ho són alhora. Per a un lògic, la frase habitual \begin_inset Quotes eld \end_inset \emph on avui és dijous o divendres \emph default \begin_inset Quotes erd \end_inset és fa certa en tres casos: quan \emph on avui és dijous \emph default , quan \emph on avui és divendres \emph default , i quan \emph on avui és dijous i divendres alhora \emph default (una mica difícil al món real, però els matemàtics són capaços de fer tot tipus de suposicions...). \layout Subsection Eliminació de la disjunció \layout Standard Aquesta és la regla més complicada, precisament perquè si ens donen una frase amb \emph on o \emph default , tal com \begin_inset Quotes eld \end_inset \emph on avui és dijous o divendres \emph default \begin_inset Quotes erd \end_inset , què podem treure d'aquí? Que \emph on avui és dijous \emph default ? No, podria ser divendres. Que \emph on avui és divendres \emph default ? No, podria ser dijous. Que \emph on avui és dijous o divendres \emph default ? Bé, és clar, però això ja ho sabíem... \layout Standard La regla (ara l'explico): \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 Necessitem més informació apart d'un \begin_inset Formula $A\vee B$ \end_inset . Si, per casualitat, sabem que \begin_inset Formula $A\Rightarrow C$ \end_inset , i que també \begin_inset Formula $B\Rightarrow C$ \end_inset , aleshores sí que podem saber què passa quan \begin_inset Formula $A\vee B$ \end_inset : tant una opció com l'altra ens porten a \begin_inset Formula $C$ \end_inset , per tant \begin_inset Formula $C$ \end_inset és certa. \layout Standard Aquest tipus de coses només passen quan l'exercici està preparat per a què hi apareixi una \emph on eliminació de la disjunció \emph default , o quan \begin_inset Formula $A$ \end_inset i \begin_inset Formula $B$ \end_inset s'assemblen molt (llavors trobarem una \begin_inset Formula $C$ \end_inset tal que totes dues l'impliquin). \layout Standard Un exemple: quan vaig contractar l'accés a Internet per ADSL, va ser amb \emph on Telefónica \emph default o \emph on Terra \emph default , però no sé exactament amb qui (ni tan sols ells ho sabien). Qualsevol opció era lenta, caríssima, i plena de problemes (a tot això li diré \begin_inset Formula $M$ \end_inset ), per tant qualsevol companyia era una \begin_inset Formula $M$ \end_inset . En concret, sabem que \begin_inset Formula $Telefonica\Rightarrow M$ \end_inset , i que \begin_inset Formula $Terra\Rightarrow M$ \end_inset , així que no hi ha dubtes sobre la qualitat de la meva connexió ADSL: també era una \begin_inset Formula $M$ \end_inset , tant si la tenia amb una companyia com amb l'altra. I a més em va costar 9 mesos completar l'alta... sort que aquestes coses van passar ja fa molts anys. \layout Standard A aquesta regla l'anomenen \emph on prova per casos \emph default , perquè s'ha de comprovar cada possible cas per veure que tots porten a la mateixa conclusió. \layout Subsection Introducció de la negació \layout Standard Aquesta és molt maca i interessant: \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 Si en suposar que \begin_inset Formula $A$ \end_inset , has arribat a la conclusió que són certes \begin_inset Formula $B$ \end_inset i \begin_inset Formula $\neg B$ \end_inset a la vegada, no estàs perdut, ja que acabes de descobrir una altra veritat: que no és possible que \begin_inset Formula $A$ \end_inset sigui cert, per tant, que \begin_inset Formula $\neg A$ \end_inset és cert. \layout Standard Per exemple, confesso que \emph on si uso Windows, no aprofito el temps que estic amb l'ordinador \emph default . Des de fa anys \emph on sí que l'aprofito \emph default , per tant la conclusió és que \emph on no uso Windows \emph default . Per arribar a aquesta conclusió, el camí que hauries seguit (potser sense pensar-hi) és precisament el que demana aquesta regla: suposem que \emph on sí que utilitzo Windows \emph default , en aquest cas \emph on no aprofitaria el meu ordinador \emph default . Però dic que \emph on sí que ho aprofito \emph default , així que la suposició ha de ser equivocada. \layout Standard A aquest procediment se l'anomena \emph on reducció a l'absurd \emph default ( \emph on reductio ad absurdum \emph default ): suposar quelcom per arribar a una contradicció i poder afirmar que allò suposat és fals. Va molt bé si comences suposant \emph on allò contrari \emph default al que vols demostrar: si arribes a una contradicció, ja està gairebé tot fet. \layout Standard He d'avisar de que aquest és un \emph on abús de notació \emph default : resulta que per a que quadrin els teoremes de la lògica, tota subdemostració ha de tenir \emph on una \emph default conclusió (no dues); i en aquesta hipòtesi que surt a la regla de dalt, no queda clar quina és la conclusió (si \begin_inset Formula $B$ \end_inset o \begin_inset Formula $\neg B$ \end_inset ). La forma correcta d'escriure-ho seria usar la \emph on introducció de la conjunció \emph default per dir que \begin_inset Formula $B\wedge\neg B$ \end_inset , i aquesta és la conclusió que ens fa veure que la hipòtesi inicial era errònia. Però els meus professors s'estalviaven aquesta línia. \layout Subsection Eliminació de la negació \layout Standard Aquesta és molt senzilla, però cal dir-la: \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 O sigui, que quan veiem la negació de la negació d'alguna cosa, podem treure aquestes dues negacions seguides. \layout Standard Recorda que la negació de \begin_inset Quotes eld \end_inset \emph on això és blanc \emph default \begin_inset Quotes erd \end_inset no és pas \begin_inset Quotes eld \end_inset \emph on això és negre \emph default \begin_inset Quotes erd \end_inset sinó \begin_inset Quotes eld \end_inset \emph on això no és blanc \emph default \begin_inset Quotes erd \end_inset . \layout Subsection No hi ha més regles \layout Standard Doncs ja està, no n'hi ha més de bàsiques. Encara hi ha algunes que parlen de \emph on quantificadors \emph default i dos de \emph on cert \emph default i \emph on fals \emph default , que explico més endavant, però amb aquestes nou ja es pot intentar demostrar la validesa de qualsevol seqüent d'aquest document (excepte els que tenen quantificadors...). \layout Standard Recorda altre cop que no hi ha més regles: no pots canviar de \begin_inset Formula $A\vee\neg A$ \end_inset a \begin_inset Formula $\blacksquare$ \end_inset ( \emph on cert \emph default ) directament, ni de \begin_inset Formula $\neg(A\vee B)$ \end_inset a \begin_inset Formula $\neg A\wedge\neg B$ \end_inset , ni usar la propietat distributiva, associativa, o commutativa. Ho has de fer tot pas a pas; ni tan sols els canvis senzills estan permesos (de moment). Per què? Perquè potser no són tan senzills com creus: ja ho veuràs quan et toqui demostrar que \begin_inset Formula $A\vee\neg A$ \end_inset és sempre cert... (està a la següent secció). \layout Section Exercicis explicats \layout Standard Exercicis de molts nivells explicats pas a pas. Si encara vols més exemples (però sense comentar), mira l'última secció. El que intento explicar aquí no són les regles, sinó el com s'ha de pensar per a que et vingui al cap la idea màgica que ho soluciona. \layout Standard Això és el que més vaig trobar a faltar quan havia d'estudiar deducció natural. \layout Subsection Un molt senzill. \begin_inset Formula $P,\ P\Rightarrow Q\vdash P\wedge Q$ \end_inset \layout Standard La solució a \begin_inset Formula $P,\ P\Rightarrow Q\vdash P\wedge Q$ \end_inset és: \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 Aquí no hem de pensar molt, només cal usar bé les regles i les seves justificaci ons. \layout Standard El primer és entendre el que ens han dit: diuen que ara passen \emph on dues \emph default coses, la primera és que \begin_inset Formula $P$ \end_inset i la segona és que \begin_inset Formula $P\Rightarrow Q$ \end_inset (són les dues fórmules que hi ha a l'esquerra del \begin_inset Formula $\vdash$ \end_inset ). Aquestes dues coses les hem d'apuntar, una per línia, perquè en aquesta demostració seran sempre certes (ens agradi o no). \layout Standard L'objectiu d'aquesta demostració és saber que \begin_inset Formula $P\wedge Q$ \end_inset també és cert, perquè ens han contat que quan \begin_inset Formula $P$ \end_inset i \begin_inset Formula $P\Rightarrow Q$ \end_inset són certs, llavors \begin_inset Formula $P\wedge Q$ \end_inset també, i volem comprovar si això és veritat. Al final ho hem aconseguit, perquè a l'última línia hi surt escrit el \begin_inset Formula $P\wedge Q$ \end_inset . \layout Standard I ara com seguim? Ens hem de fixar en on volem arribar. Si \begin_inset Formula $P\wedge Q$ \end_inset ha de ser cert, llavors tant \begin_inset Formula $P$ \end_inset com \begin_inset Formula $Q$ \end_inset ho hauran de ser; doncs preocupem-nos primer per demostrar que ho són. \layout Standard \begin_inset Formula $P$ \end_inset és cert, perquè ens ho han dit, i ho tenim apuntat a la línia 1. \layout Standard Però no ens han dit que \begin_inset Formula $Q$ \end_inset ho sigui. Què ens han dit sobre \begin_inset Formula $Q$ \end_inset ? Buscant-la a les línies 1 i 2, l'únic que coneixem és que \begin_inset Formula $Q$ \end_inset és certa quan passa \begin_inset Formula $P$ \end_inset (ho diu a la 2). I com \begin_inset Formula $P$ \end_inset és certa, podem usar una de les regles per deduir \begin_inset Formula $Q$ \end_inset a partir del \begin_inset Formula $P\Rightarrow Q$ \end_inset i de \begin_inset Formula $P$ \end_inset . Fixa't en què és el més important que ha passat en canviar de \begin_inset Formula $P\Rightarrow Q$ \end_inset a \begin_inset Formula $Q$ \end_inset : s'ha deixat d'usar el símbol de la implicació; així que la regla que necessite m s'anomena \emph on eliminació de la implicació \emph default . \layout Standard Per utilitzar aquesta regla, mirem la seva definició, i veiem que hem de posar en una nova línia la \begin_inset Formula $Q$ \end_inset , i com a justificació s'ha d'escriure \begin_inset Formula $E\Rightarrow\ 2,1$ \end_inset . La \begin_inset Formula $E$ \end_inset ve d' \emph on eliminació \emph default , el \begin_inset Formula $\Rightarrow$ \end_inset és per \emph on implicació \emph default , el primer número és el de la línia que conté implicació ( \begin_inset Formula $P\Rightarrow Q$ \end_inset ), i el segon número és el de la línia que conté la veritat coneguda ( \begin_inset Formula $P$ \end_inset ). És incorrecte posar-los al revés ( \begin_inset Formula $E\Rightarrow\ 1,2$ \end_inset ), perquè a la definició de la regla diu que la línia que conté la implicació ha de ser citada en primer lloc. \layout Standard Ja hem aplicat la regla, i ja sabem tres coses que són certes: que \begin_inset Formula $P$ \end_inset , que \begin_inset Formula $P\Rightarrow Q$ \end_inset , i que \begin_inset Formula $Q$ \end_inset . Totes són igual de certes. Ara estem més a prop de l'objectiu, \begin_inset Formula $P\wedge Q$ \end_inset , perquè ja sabem que \begin_inset Formula $P$ \end_inset i \begin_inset Formula $Q$ \end_inset són certes, així que \begin_inset Formula $P\wedge Q$ \end_inset també ha de ser-ho (és obvi). A la fórmula que busquem hi ha un signe de conjunció ( \begin_inset Formula $\wedge$ \end_inset ) que no tenim, per tant cal usar la \emph on introducció de la conjunció \emph default per afirmar que \begin_inset Formula $P\wedge Q$ \end_inset és cert perquè \begin_inset Formula $P$ \end_inset ho és i \begin_inset Formula $Q$ \end_inset també. Com a justificació posem \begin_inset Formula $I\wedge\ 1,3$ \end_inset (la línia on diu que \begin_inset Formula $P$ \end_inset , i on diu que \begin_inset Formula $Q$ \end_inset ). No val posar \begin_inset Formula $I\wedge\ 3,1$ \end_inset , això seria per assegurar que \begin_inset Formula $Q\wedge P$ \end_inset , que no és el que ens demanen demostrar. \layout Standard Llavors ja sabem que 4 coses són certes: \begin_inset Formula $P$ \end_inset , \begin_inset Formula $P\Rightarrow Q$ \end_inset , \begin_inset Formula $Q$ \end_inset , i \begin_inset Formula $P\wedge Q$ \end_inset . Podríem continuar descobrint encara més coses certes, però és que ja hem acabat, perquè ens demanaven demostrar que \begin_inset Formula $P\wedge Q$ \end_inset és cert i ja ho hem aconseguit (a la línia 4). Per tant, aquesta serà l'última línia, i no s'ha d'escriure res més. \layout Standard Ah, un exemple d'això amb paraules: \begin_inset Quotes eld \end_inset \emph on ara és estiu, i a l'estiu fa calor. Per això ara és estiu i fa calor \emph default \begin_inset Quotes erd \end_inset . \layout Subsection Una mica més complicat. \begin_inset Formula $P\wedge Q\Rightarrow R,\ Q\Rightarrow P,\ Q\vdash R$ \end_inset \layout Standard Prova a fer tu sol el \begin_inset Formula $P\wedge Q\Rightarrow R,\ Q\Rightarrow P,\ Q\vdash R$ \end_inset . Després mira la solució: \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 L'única forma que hi ha d'arribar a \begin_inset Formula $R$ \end_inset és usant la primera fórmula, \begin_inset Formula $P\wedge Q\Rightarrow R$ \end_inset , però només la podem usar quan \begin_inset Formula $P\wedge Q$ \end_inset és cert, per tant anem a per això. \layout Standard Sabem que \begin_inset Formula $Q\Rightarrow P$ \end_inset (línia 2) i que \begin_inset Formula $Q$ \end_inset (línia 3), així que deduïm que \begin_inset Formula $P$ \end_inset . Com que ara \begin_inset Formula $P$ \end_inset és cert i \begin_inset Formula $Q$ \end_inset també, \begin_inset Formula $P\wedge Q$ \end_inset també ho és. Fins aquí és semblant a l'exercici anterior. \layout Standard Per últim, tenim que \begin_inset Formula $P\wedge Q\Rightarrow R$ \end_inset , i sabem que \begin_inset Formula $P\wedge Q$ \end_inset , per tant acabem dient que \begin_inset Formula $R$ \end_inset . \layout Subsection Començant a suposar coses. \begin_inset Formula $P\Rightarrow Q,\ Q\Rightarrow R\vdash P\Rightarrow Q\wedge R$ \end_inset \layout Standard Aquest, \begin_inset Formula $P\Rightarrow Q,\ Q\Rightarrow R\vdash P\Rightarrow Q\wedge R$ \end_inset , és més interessant: \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 Fixa't en els següents detalls: \layout Itemize No ens donen cap informació sobre què passa ara (ni han donat la fórmula \begin_inset Formula $P$ \end_inset , ni \begin_inset Formula $Q\wedge R$ \end_inset , etc.). Només ens diuen coses com que \emph on si passés \begin_inset Formula $P$ \end_inset , llavors també passaria \begin_inset Formula $Q$ \end_inset \emph default . \layout Itemize De la mateixa forma, el que hem de demostrar no és que \emph on ara mateix passa alguna cosa \emph default , sinó que \emph on si passa \begin_inset Formula $P$ \end_inset , llavors \begin_inset Formula $Q$ \end_inset i \begin_inset Formula $R$ \end_inset són certes \emph default . \layout Itemize \begin_inset Formula $P\Rightarrow Q\wedge R$ \end_inset és una implicació ( \emph on una cosa implica una altra \emph default ), perquè l'operador \begin_inset Formula $\Rightarrow$ \end_inset té menys prioritat que el \begin_inset Formula $\wedge$ \end_inset . És un error greu interpretar aquesta fórmula com \begin_inset Formula $(P\Rightarrow Q)\wedge R$ \end_inset . \layout Standard Ja que la fórmula que volem és una implicació ( \begin_inset Formula $P\Rightarrow Q\wedge R$ \end_inset ), haurem d'usar la \emph on introducció de la implicació \emph default , però aquesta regla requereix tenir una subdemostració (consulta la seva definició). \layout Standard No és gens complicat entendre per què: \begin_inset Formula $P\Rightarrow Q\wedge R$ \end_inset diu que \emph on si passa \begin_inset Formula $P$ \end_inset , llavors passa \begin_inset Formula $Q\wedge R$ \end_inset \emph default , així que el primer que caldrà fer serà suposar que sí que passa \begin_inset Formula $P$ \end_inset . Llavors haurem de trobar que, en aquest cas en què \begin_inset Formula $P$ \end_inset és cert, també ho és \begin_inset Formula $Q\wedge R$ \end_inset . Quan ho aconseguim, apliquem la regla, i ho deixem ben escrit: \begin_inset Formula $P\Rightarrow Q\wedge R$ \end_inset . \layout Standard Per això a la línia 3 es fa una hipòtesi (justificada amb la \begin_inset Formula $H$ \end_inset a la dreta): suposem que \begin_inset Formula $P$ \end_inset és cert. Ara comencem una subdemostració, on podem usar les veritats que hi ha escrites a la demostració pare (línies 1 i 2 en aquest cas), i també podem usar \begin_inset Formula $P$ \end_inset com si fos veritat. \layout Standard Hem fet aquesta hipòtesi amb l'objectiu de saber que \begin_inset Formula $Q\wedge R$ \end_inset , per tant ho deduïm igual que als exemples anteriors. Fixa't que usem veritats de dins i de fora de la subdemostració, i que, mentre no l'acabem, s'ha de posar aquella ratlla vertical a l'esquerra. \layout Standard A la línia 6 ja tenim el \begin_inset Formula $Q\wedge R$ \end_inset , que és el que volíem. Usant la regla de \emph on introducció de la implicació \emph default , podem sortir d'aquesta subdemostració dient que \emph on si la hipòtesi és certa, llavors tot allò que hem deduït a partir d'ella també \emph default . Es deixa de posar la ratlleta vertical, perquè \begin_inset Formula $P\Rightarrow Q\wedge R$ \end_inset és cert sempre (no depèn de si \begin_inset Formula $P$ \end_inset és veritat o no). La justificació usada, \begin_inset Formula $I\Rightarrow\ 3,6$ \end_inset , diu que 3 és la línia on hem fet la suposició, i 6 la línia on hem descobert quelcom interessant que passa en fer aquesta suposició. \layout Standard \begin_inset Formula $P\Rightarrow Q\wedge R$ \end_inset és el que volíem, per tant ja hem acabat. I acabem de la mateixa forma que sempre, perquè estem fora de tota subdemostrac ió. \layout Subsection Usant la iteració. \begin_inset Formula $P\vdash Q\Rightarrow P$ \end_inset \layout Standard Aquest és molt curt: \begin_inset Formula $P\vdash Q\Rightarrow P$ \end_inset . Solució: \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 El camí és directe: hem de suposar \begin_inset Formula $Q$ \end_inset , i acabar veient que, en aquest cas, és cert \begin_inset Formula $P$ \end_inset . El truc: \begin_inset Formula $P$ \end_inset és sempre cert, tant si suposem \begin_inset Formula $Q$ \end_inset com si no. \layout Standard Haurem d'usar la \emph on introducció de la implicació \emph default , però això requereix tenir una hipòtesi, i, línies més avall, el resultat d'haver suposat això. És llavors quan podem tancar la hipòtesi. \layout Standard Després d'obrir-la (línia 2), haurem de fer alguna cosa per deixar escrit que \begin_inset Formula $P$ \end_inset . Com ja ho tenim escrit a la línia 1, simplement posem la \begin_inset Formula $P$ \end_inset altre cop i ho justifiquem amb \begin_inset Formula $IT\ 1$ \end_inset , que vol dir \begin_inset Quotes eld \end_inset \emph on això ho he copiat de la línia 1 \emph default \begin_inset Quotes erd \end_inset . El \begin_inset Formula $IT$ \end_inset és per \emph on iteració \emph default . \layout Standard Ja complim els requisits per aplicar la regla, així que l'apliquem, sortim de la subdemostració, i hem acabat. \layout Subsection Reducció a l'absurd. \begin_inset Formula $P\Rightarrow Q,\ \neg Q\vdash\neg P$ \end_inset \layout Standard Aquesta és una tècnica molt útil. La validesa de \begin_inset Formula $P\Rightarrow Q,\ \neg Q\vdash\neg P$ \end_inset es demostra amb: \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 A on s'ha d'arribar és a \begin_inset Formula $\neg P$ \end_inset , que és \emph on la negació d'alguna cosa \emph default , per això s'haurà d'utilitzar la regla de \emph on introducció de la negació \emph default , coneguda per \emph on reducció a l'absurd \emph default . \layout Standard La forma de fer-ho serà suposar el contrari de \begin_inset Formula $\neg P$ \end_inset (que és \begin_inset Formula $P$ \end_inset ) i arribar a una contradicció. En suposar \begin_inset Formula $P$ \end_inset arribarem a \begin_inset Formula $Q$ \end_inset (per \emph on eliminació de la implicació \emph default ), i com que també tenim \begin_inset Formula $\neg Q$ \end_inset , podem aplicar la regla. Aquest \begin_inset Formula $\neg Q$ \end_inset l'haurem de repetir a dintre la subdemostració amb la regla d' \emph on iteració \emph default , per a que estigui junt amb la \begin_inset Formula $Q$ \end_inset però també \emph on dins \emph default de la subdemostració. Tot el que hi ha a dins de la subdemostració és conseqüència de \begin_inset Formula $P$ \end_inset , així que és important veure que tant \begin_inset Formula $Q$ \end_inset com \begin_inset Formula $\neg Q$ \end_inset ho són. \layout Standard Per a la \emph on introducció de la negació \emph default , la forma de justificar la regla és posant el número de línia on comença la suposició (errònia), i els números de les dues línies on hem vist la contradicció. La conclusió d'aquesta regla és el contrari d'allò que s'havia suposat, en aquest cas \begin_inset Formula $\neg P$ \end_inset , per tant ja podem acabar el procediment. \layout Standard Aquest raonament normalment el fem sense pensar-hi gaire. En paraules seria semblant a: \begin_inset Quotes eld \end_inset \emph on és clar que \begin_inset Formula $\neg P$ \end_inset , perquè si fos \begin_inset Formula $P$ \end_inset llavors \begin_inset Formula $Q$ \end_inset , i em diuen que \begin_inset Formula $\neg Q$ \end_inset , així que no pot ser \begin_inset Formula $P$ \end_inset \emph default \begin_inset Quotes erd \end_inset . \layout Subsection Amb subdemostracions. \begin_inset Formula $P\Rightarrow(Q\Rightarrow R)\vdash Q\Rightarrow(P\Rightarrow R)$ \end_inset \layout Standard Es compliquen les coses. La solució 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 Primerament: aquí només usarem les dues regles que ajuden a afegir i treure implicacions, perquè és l'únic operador que tenim. \layout Standard Com que volem arribar a \begin_inset Formula $Q\Rightarrow(P\Rightarrow R)$ \end_inset , haurem de fer una hipòtesi \begin_inset Formula $Q$ \end_inset dins la qual s'ha de demostrar \begin_inset Formula $P\Rightarrow R$ \end_inset . Doncs fem això ara per simplificar el problema: obrim la subdemostració a la línia 2. No la tancarem fins que no s'arribi a saber que \begin_inset Formula $P\Rightarrow R$ \end_inset és cert. \layout Standard Ara el problema és una mica més fàcil. Necessitem comprovar que \begin_inset Formula $P\Rightarrow R$ \end_inset , i tenim dues línies amb dues veritats: la primera diu que \begin_inset Formula $P\Rightarrow(Q\Rightarrow R)$ \end_inset , i la segona diu que \begin_inset Formula $Q$ \end_inset . \layout Standard Com podem aconseguir el \begin_inset Formula $P\Rightarrow R$ \end_inset ? Doncs com sempre: s'ha de suposar que \begin_inset Formula $P$ \end_inset , i aconseguir veure que \begin_inset Formula $R$ \end_inset , d'alguna manera. Encara que no sembli molt fàcil, és el que s'ha de fer, perquè la \emph on introducció de la implicació \emph default va així. Per tant, anem a obrir una altra hipòtesi, ara suposant que \begin_inset Formula $P$ \end_inset , i anem a veure si arribem a \begin_inset Formula $R$ \end_inset . Aquesta serà una hipòtesi dins d'una hipòtesi, però no hi ha cap problema en fer això. \layout Standard Després d'escriure la línia 3, i, ficats a dins d'una \emph on subsubdemostració \emph default , tenim al nostre abast que \begin_inset Formula $P\Rightarrow(Q\Rightarrow R)$ \end_inset , que \begin_inset Formula $Q$ \end_inset , i que \begin_inset Formula $P$ \end_inset . Hem de provar que \begin_inset Formula $R$ \end_inset . Ja no sembla tan difícil, no? Si sabem que \begin_inset Formula $P$ \end_inset , podem usar l' \emph on eliminació de la implicació \emph default amb la línia 1, i així aconseguirem la fórmula certa \begin_inset Formula $Q\Rightarrow R$ \end_inset . Com també és cert \begin_inset Formula $Q$ \end_inset (línia 2), podem tornar a usar la mateixa regla per saber que \begin_inset Formula $R$ \end_inset . \layout Standard Hem vist que el suposar \begin_inset Formula $P$ \end_inset ens ha portat a la conclusió de que \begin_inset Formula $R$ \end_inset , així que podem deixar escrit que \begin_inset Formula $P\Rightarrow R$ \end_inset , que és allò que anàvem buscant. Ara ja hem sortit de la subsubdemostració, i només estem dins la suposició que \begin_inset Formula $Q$ \end_inset és cert. Com veiem que aquesta suposició implica la certesa de la fórmula \begin_inset Formula $P\Rightarrow R$ \end_inset , podem sortir d'aquesta subdemostració concloent que \begin_inset Formula $Q\Rightarrow(P\Rightarrow R)$ \end_inset . \layout Standard \begin_inset Formula $Q\Rightarrow(P\Rightarrow R)$ \end_inset és precisament el que s'havia de demostrar, per tant ja s'ha acabat. \layout Subsection Un de prova per casos. \begin_inset Formula $P\vee(Q\wedge R)\vdash P\vee Q$ \end_inset \layout Standard S'haurà d'usar la regla més complicada: l' \emph on eliminació de la disjunció \emph default . \begin_inset Formula $P\vee(Q\wedge R)\vdash P\vee Q$ \end_inset solucionat: \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 Ja coneixes les regles, així que explico la forma de pensar d'un humà que no entengui de deducció natural però que pensi una mica: \layout Standard Necessitem comprovar que \begin_inset Formula $P\vee Q$ \end_inset és cert sempre. L'expressió de l'esquerra, \begin_inset Formula $P\vee(Q\wedge R)$ \end_inset , es pot complir per dos motius: \layout Itemize si es compleix perquè \begin_inset Formula $P$ \end_inset és cert, llavors \begin_inset Formula $P\vee Q$ \end_inset és cert. \layout Itemize si es compleix perquè \begin_inset Formula $Q\wedge R$ \end_inset és cert, és que \begin_inset Formula $Q$ \end_inset i \begin_inset Formula $R$ \end_inset són certes, i per tant \begin_inset Formula $P\vee Q$ \end_inset és cert gràcies a \begin_inset Formula $Q$ \end_inset . \layout Standard O sigui, que de qualsevol de les maneres, \begin_inset Formula $P\vee Q$ \end_inset és cert. \layout Standard Doncs ara l'únic que queda és traduir a llenguatge lògic, seguint el mateix ordre en què s'ha pensat, i anant a poc a poc. \layout Standard Es comença demostrant un camí, després l'altre, i per últim s'aplica la regla d' \emph on eliminació de la disjunció \emph default . Per justificar-la s'ha d'escriure la línia on està la disjunció, i les dues línies de dins de cada subdemostració on es vegi que tant en suposar una cosa com en suposar l'altra, el resultat és el mateix. \layout Standard Fixa't que, encara que esbrinem que \begin_inset Formula $P\Rightarrow P\vee Q$ \end_inset i que \begin_inset Formula $Q\wedge R\Rightarrow P\vee Q$ \end_inset , no fa falta usar la \emph on introducció de la implicació \emph default per deixar-ho escrit. \layout Standard El més complicat de la \emph on prova per casos \emph default sol ser decidir quina expressió demostraràs en ambdós casos. Ha de ser la mateixa als dos casos! \layout Subsection Un per pensar-hi. \begin_inset Formula $L\wedge M\Rightarrow\neg P,\ I\Rightarrow P,\ M,\ I\vdash\neg L$ \end_inset \layout Standard Intenta fer \begin_inset Formula $L\wedge M\Rightarrow\neg P,\ I\Rightarrow P,\ M,\ I\vdash\neg L$ \end_inset de cap; després escriu-lo en paper. Queda: \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 L'expresso per paraules: \begin_inset Quotes eld \end_inset \emph on si uses Linux i Mozilla com a navegador, t'evites els problemes. En canvi, si uses Internet Explorer tindràs problemes. Ara tu uses Mozilla, però també Internet Explorer a vegades. Per tant, sé que no uses Linux \emph default \begin_inset Quotes erd \end_inset . \layout Standard Potser sembla evident: \begin_inset Quotes eld \end_inset \emph on és clar, perquè IE no està en Linux \emph default \begin_inset Quotes erd \end_inset , però fixa't que no he dit això en cap moment. No hi surt el \begin_inset Formula $I\Rightarrow\neg L$ \end_inset enlloc. \layout Standard La forma en què hauries de pensar mentre prepares l'exercici és: \layout Enumerate Necessito demostrar \begin_inset Formula $\neg L$ \end_inset , que és la negació d'alguna cosa. No es veu cap regla de la forma \emph on quelcom implica \begin_inset Formula $\neg L$ \end_inset \emph default que em permeti obtenir-ho directament. S'haurà de fer d'una altra forma, per exemple amb la \emph on introducció de la negació \emph default ( \emph on reducció a l'absurd \emph default ): suposem que sí que uso Linux. \layout Enumerate En el cas de que usés Linux, usaria Linux i Mozilla, perquè ja usava Mozilla abans (és la tercera veritat que hi surt escrita a l'enunciat). \layout Enumerate En usar Linux i Mozilla, no tindria problemes informàtics, perquè \begin_inset Formula $L\wedge M\Rightarrow\neg P$ \end_inset . \layout Enumerate Però també usava Internet Explorer (quarta veritat), i com que IE genera problemes, jo tindré problemes. \begin_inset Formula $P$ \end_inset . \layout Enumerate He arribat a una contradicció: \begin_inset Formula $\neg P$ \end_inset i \begin_inset Formula $P$ \end_inset . Per tant, el que passa és que la suposició que he fet de que uso Linux és incorrecta: resulta que \begin_inset Formula $\neg L$ \end_inset . \layout Standard Doncs ara només s'ha de seguir el mateix procediment, però escrivint-ho pas per pas i usant les regles. S'obtindrà la mateixa figura que surt a dalt, que casualment té 5 línies de procediment (les 4 primeres són només per copiar les veritats). Cada línia es correspon amb els passos que he explicat aquí. \layout Subsection La part esquerra buida. \begin_inset Formula $\vdash P\Rightarrow P$ \end_inset \layout Standard Demostrar \begin_inset Formula $\vdash P\Rightarrow P$ \end_inset és molt fàcil i curt: \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 Aquest cas encara no havia sortit: resulta que el costat esquerre del seqüent està buit. Això vol dir que no ens donen cap veritat en què basar-nos per demostrar que \begin_inset Formula $P\Rightarrow P$ \end_inset . Per què? Doncs perquè \begin_inset Formula $P\Rightarrow P$ \end_inset és cert sempre, sense importar el valor de \begin_inset Formula $P$ \end_inset o de la resta de fórmules. \layout Standard És molt més còmode i interessant resoldre una d'aquestes demostracions, perquè pots començar a treballar directament en la fórmula a la qual vols arribar. Però ves amb compte, perquè hi ha algunes \emph on veritats absolutes \emph default (de les que són certes sempre) molt difícils i llargues de demostrar. \layout Standard Apunta: sempre que la part esquerra estigui buida, s'ha de començar amb una hipòtesi (quina altra cosa podríem fer?). \layout Standard Per aconseguir provar que \begin_inset Formula $P\Rightarrow P$ \end_inset fem el de sempre: suposem que \begin_inset Formula $P$ \end_inset i intentem arribar a veure que \begin_inset Formula $P$ \end_inset és cert. Com ho hem just suposat a la primera línia, usem la regla de \emph on iteració \emph default per copiar-ho endins, i acabem la subdemostració mitjançant la \emph on introducció de la implicació \emph default . I ja està tot fet, en tres línies. \layout Standard Fixa't en que \begin_inset Formula $P\Rightarrow P$ \end_inset és cert perquè \begin_inset Formula $\blacksquare\Rightarrow\blacksquare$ \end_inset i \begin_inset Formula $\square\Rightarrow\square$ \end_inset . Ja de pas, recordo que també \begin_inset Formula $\square\Rightarrow\blacksquare$ \end_inset , però \begin_inset Formula $\blacksquare\nRightarrow\square$ \end_inset . \layout Subsection Suposar el contrari. \begin_inset Formula $\vdash\neg(P\wedge\neg P)$ \end_inset \layout Standard Un altre de senzill, \begin_inset Formula $\vdash\neg(P\wedge\neg P)$ \end_inset . Es fa així: \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 Tots sabem que no poden passar dues coses contràries alhora, però, com ho demostrem? S'ha d'utilitzar la \emph on reducció a l'absurd \emph default : \layout Standard Suposem que sí que passa \begin_inset Formula $P\wedge\neg P$ \end_inset . Llavors passa \begin_inset Formula $P$ \end_inset i passa \begin_inset Formula $\neg P$ \end_inset , els dos alhora, i això és una contradicció. Per tant, la suposició que hem fet no pot ser certa; o sigui que és falsa. Així es demostra que \begin_inset Formula $\neg(P\wedge\neg P)$ \end_inset . \layout Standard Quan vegis alguna cosa tan \emph on clara \emph default i \emph on òbvia \emph default com \begin_inset Formula $\neg(P\wedge\neg P)$ \end_inset , aleshores el seu contrari serà \emph on clarament \emph default fals i absurd. Per tant, no et costarà molt demostrar que no s'aguanta i que es contradiu per si sol. Un cop fet això, podem assegurar que la fórmula original és certa ja que el seu contrari és fals. \layout Subsection Aquest sembla fàcil. \begin_inset Formula $\vdash P\vee\neg P$ \end_inset \layout Standard A veure si \begin_inset Formula $\vdash P\vee\neg P$ \end_inset és tan obvi com diuen: \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 Un dels més simples i llargs que he trobat. Sembla fins i tot que no faci falta demostrar-ho, perquè tothom sap que entre \begin_inset Quotes eld \end_inset \emph on avui és dijous \emph default \begin_inset Quotes erd \end_inset i \begin_inset Quotes eld \end_inset \emph on avui no és dijous \emph default \begin_inset Quotes erd \end_inset , una de les dues és certa (no poden ser falses totes dues alhora). \layout Standard Podríem començar pensant en el mètode de \emph on prova per casos \emph default , perquè de \begin_inset Formula $P$ \end_inset podem deduir \begin_inset Formula $P\vee\neg P$ \end_inset , i de \begin_inset Formula $\neg P$ \end_inset podem deduir \begin_inset Formula $P\vee\neg P$ \end_inset , o sigui, la mateixa fórmula. Però no serveix de res, perquè la regla de \emph on prova per casos \emph default és la d' \emph on eliminació de la disjunció \emph default , i no tenim cap disjunció per eliminar; de fet, tampoc tenim la fórmula certa \begin_inset Formula $A\vee B$ \end_inset tal que \begin_inset Formula $A\Rightarrow C$ \end_inset i \begin_inset Formula $B\Rightarrow C$ \end_inset , com demana la regla. En realitat, no tenim cap fórmula que sapiguem que sigui certa (el costat esquerre del seqüent està buit). \layout Standard Sabem que s'ha de començar amb una hipòtesi (no hi ha altra alternativa). Com sembla bastant clar que \begin_inset Formula $P\vee\neg P$ \end_inset és cert, també pot semblar fàcil demostrar que el seu contrari, \begin_inset Formula $\neg(P\vee\neg P)$ \end_inset , és fals. Així que usarem la \emph on reducció a l'absurd \emph default : fent aquesta suposició a la línia 1, hem d'intentar arribar a una contradicció , la que sigui. \layout Standard Jo em vaig proposar arribar a la contradicció \begin_inset Formula $\neg P$ \end_inset i \begin_inset Formula $P$ \end_inset . Però no tenim cap d'aquestes dues fórmules; d'on les traiem? Doncs tornem a fer \emph on reducció a l'absurd \emph default : per veure que \begin_inset Formula $\neg P$ \end_inset , anem a suposar que \begin_inset Formula $P$ \end_inset per arribar a una contradicció. Igual que en altres ocasions, va molt bé aprofitar les possibilitats que ofereix la \emph on introducció de la disjunció \emph default : en suposar que \begin_inset Formula $P$ \end_inset , podrem convertir-lo en \begin_inset Formula $P\vee\neg P$ \end_inset per buscar la contradicció. Com tenim el \begin_inset Formula $\neg(P\vee\neg P)$ \end_inset dalt de tot, el podem usar per acabar demostrant que \begin_inset Formula $\neg P$ \end_inset . El mateix farem per demostrar que \begin_inset Formula $P$ \end_inset , però aquest cop suposant \begin_inset Formula $\neg P$ \end_inset . \layout Standard Quan ja hem arribat a tenir \begin_inset Formula $P$ \end_inset i \begin_inset Formula $\neg P$ \end_inset després de suposar \begin_inset Formula $\neg(P\vee\neg P)$ \end_inset , es veu que aquesta fórmula no pot ser certa, així que la seva negació, \begin_inset Formula $\neg\neg(P\vee\neg P)$ \end_inset , ho és. Per \emph on eliminació de la negació \emph default , ens queda la fórmula que buscàvem: \begin_inset Formula $P\vee\neg P$ \end_inset . \layout Standard Ho he fet d'aquesta manera per a que quedés bastant simètric, però es pot fer més curt si es busca altra contradicció, per exemple \begin_inset Formula $P\vee\neg P$ \end_inset i \begin_inset Formula $\neg(P\vee\neg P)$ \end_inset . Llavors quedaria així: \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 Un d'interessant. \begin_inset Formula $P\vee Q,\ \neg P\vdash Q$ \end_inset \layout Standard Un altre que sembla fàcil: \begin_inset Formula $P\vee Q,\ \neg P\vdash Q$ \end_inset . A veure: \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 És molt senzill d'entendre per qualsevol: es compleix \begin_inset Formula $P\vee Q$ \end_inset , però \begin_inset Formula $P$ \end_inset és fals, per tant el cert és \begin_inset Formula $Q$ \end_inset . \layout Standard Es pot fer de moltes formes, però en algun moment hauràs de fer servir l' \emph on eliminació de la disjunció \emph default per tal d'usar el \begin_inset Formula $P\vee Q$ \end_inset . Intentarem provar que tant \begin_inset Formula $P$ \end_inset com \begin_inset Formula $Q$ \end_inset porten al mateix lloc, que serà la nostra fórmula objectiu \begin_inset Formula $Q$ \end_inset (ja que es pot, anem directament a per \begin_inset Formula $Q$ \end_inset ). \layout Standard Obrim la subdemostració suposant que \begin_inset Formula $P$ \end_inset , i hem de veure que \begin_inset Formula $Q$ \end_inset . No és molt difícil perquè tenim el \begin_inset Formula $\neg P$ \end_inset a la línia 2; això ajuda a contradir tot allò que vulguem. Com el que busquem és \begin_inset Formula $Q$ \end_inset , suposem \begin_inset Formula $\neg Q$ \end_inset i per \emph on reducció a l'absurd \emph default obtenim \begin_inset Formula $\neg\neg Q$ \end_inset , que és \begin_inset Formula $Q$ \end_inset . \layout Standard L'altre camí, quan es suposa que \begin_inset Formula $Q$ \end_inset és cert, ens porta directament a \begin_inset Formula $Q$ \end_inset . \layout Standard Per tant, ambdós camins van a \begin_inset Formula $Q$ \end_inset i per \emph on eliminació de la disjunció \emph default demostrem que \begin_inset Formula $Q$ \end_inset és cert sempre. \layout Subsection Aquest me'l van posar a un examen. \begin_inset Formula $A\vee B,\ A\Rightarrow C,\ \neg D\Rightarrow\neg B\vdash C\vee D$ \end_inset \layout Standard A l'examen final d' \emph on ILO \emph default em van posar \begin_inset Formula $A\vee B,\ A\Rightarrow C,\ \neg D\Rightarrow\neg B\vdash C\vee D$ \end_inset , i vaig passar molta, molta estona fins que em va sortir: \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 Fixa't en que el resultat que busquem, \begin_inset Formula $C\vee D$ \end_inset , és una disjunció. Com ja coneixes la \emph on introducció de la disjunció \emph default , podries buscar simplement que \begin_inset Formula $C$ \end_inset , i després utilitzar aquesta regla per treure \begin_inset Formula $C\vee D$ \end_inset . O si no trobessis que \begin_inset Formula $C$ \end_inset és certa, doncs podries provar amb \begin_inset Formula $D$ \end_inset , perquè si \begin_inset Formula $D$ \end_inset és certa llavors \begin_inset Formula $C\vee D$ \end_inset ho és i hem acabat. \layout Standard Desgraciadament, \begin_inset Formula $C$ \end_inset no és certa sempre, i \begin_inset Formula $D$ \end_inset tampoc és certa sempre (en canvi \begin_inset Formula $C\vee D$ \end_inset sí que ho és sempre, i això és precisament el que volem demostrar). Després d'entendre això, s'haurà de buscar un altre mètode que treballi amb les dues fórmules \begin_inset Formula $C$ \end_inset i \begin_inset Formula $D$ \end_inset , al mateix temps, perquè sembla que si agafem una sola sense mirar l'altra, no proporciona molta informació. \layout Standard Per usar el \begin_inset Formula $A\vee B$ \end_inset s'haurà de fer la \emph on prova per casos \emph default . Intentarem arribar a que tant \begin_inset Formula $A$ \end_inset com \begin_inset Formula $B$ \end_inset condueixen a \begin_inset Formula $C\vee D$ \end_inset , perquè si ho aconseguim ja haurem acabat. \layout Standard \begin_inset Formula $A$ \end_inset implica \begin_inset Formula $C$ \end_inset , i si \begin_inset Formula $C$ \end_inset és cert també ho és \begin_inset Formula $C\vee D$ \end_inset , per tant \begin_inset Formula $A$ \end_inset implica \begin_inset Formula $C\vee D$ \end_inset . \layout Standard Sobre \begin_inset Formula $B$ \end_inset , el poc que sabem no la relaciona amb \begin_inset Formula $C$ \end_inset sinó amb la \begin_inset Formula $D$ \end_inset . Volem \begin_inset Formula $C\vee D$ \end_inset . Difícilment aconseguirem que \begin_inset Formula $C\vee D$ \end_inset es compleixi gràcies a \begin_inset Formula $C$ \end_inset , així que intentarem que sigui \begin_inset Formula $D$ \end_inset la certa. Per fer-ho, usem \emph on reducció a l'absurd \emph default : suposem que \begin_inset Formula $D$ \end_inset és fals, llavors es compleix \begin_inset Formula $\neg B$ \end_inset per la fórmula de la línia 3. Però érem sota la suposició que \begin_inset Formula $B$ \end_inset era cert, així que la nostra hipòtesi \begin_inset Formula $\neg D$ \end_inset no pot ser certa, i llavors \begin_inset Formula $D$ \end_inset és certa, i per tant \begin_inset Formula $C\vee D$ \end_inset també. \layout Standard Com \begin_inset Formula $A\vee B$ \end_inset és cert, i tots dos camins ens porten a \begin_inset Formula $C\vee D$ \end_inset , acabem veient que \begin_inset Formula $C\vee D$ \end_inset sempre és cert. \layout Standard Si tens pràctica treballant amb fórmules lògiques, hauràs vist que \begin_inset Formula $\neg D\Rightarrow\neg B$ \end_inset és \begin_inset Formula $B\Rightarrow D$ \end_inset . Això simplifica molt el problema i ajuda a entendre'l abans. De totes formes, no pots canviar \begin_inset Formula $\neg D\Rightarrow\neg B$ \end_inset per \begin_inset Formula $B\Rightarrow D$ \end_inset directament, sinó que s'ha de fer pas a pas. \layout Subsection Un \begin_inset Quotes eld \end_inset curt \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 Sembla fàcil: si dues expressions són equivalents, és perquè són ambdues certes, o ambdues falses. He pogut demostrar la validesa de \begin_inset Formula $A\Longleftrightarrow B\vdash(A\wedge B)\vee(\neg A\wedge\neg B)$ \end_inset així: \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 Primer: no va bé escriure \begin_inset Formula $A\Longleftrightarrow B$ \end_inset perquè no tenim regles per al \begin_inset Formula $\Longleftrightarrow$ \end_inset . Com que gairebé no s'usa, quan surt un \begin_inset Formula $\Longleftrightarrow$ \end_inset es permet canviar-lo per \begin_inset Formula $(A\Rightarrow B)\wedge(B\Rightarrow A)$ \end_inset , que és el mateix. \layout Standard Bé, això és l'únic que se m'ha acudit... Et deixo com a exercici el buscar una manera més curta (si és que n'hi ha). El que jo he fet és deixar escrit que \begin_inset Formula $A\vee\neg A$ \end_inset és cert (aquest exercici ja ha sortit, aquí he repetit els mateixos passos). Un cop sé que es compleix \begin_inset Formula $A\vee\neg A$ \end_inset , veig que tant el cas \begin_inset Formula $A$ \end_inset com el cas \begin_inset Formula $\neg A$ \end_inset porten a la mateixa fórmula, que és la solució. \layout Section Coses incorrectes \layout Standard Errors comuns que no has de cometre. Recorda que un professor de lògica corregirà els teus exercicis amb un \emph on cert \emph default o un \emph on fals \emph default , així que aprèn a fer-ho perfecte. \layout Subsection Introducció i eliminació d' \emph on \begin_inset Quotes eld \end_inset allò que em vagi bé \begin_inset Quotes erd \end_inset \layout Standard Les regles de \emph on introducció \emph default i \emph on eliminació \emph default no són per a que puguis escriure tot el que tu vulguis, sinó per ajudar-te a utilitzar o generar una fórmula amb un operador concret. \layout Standard Per tant, si tens \begin_inset Formula $P$ \end_inset no pots dir \begin_inset Quotes eld \end_inset \emph on doncs ara faig \emph default introducció de negació \emph on i obtinc \begin_inset Formula $\neg P$ \end_inset , que és el que em feia falta \emph default \begin_inset Quotes erd \end_inset . Hi ha uns quants requisits per cada regla, i si no es satisfan, no la pots aplicar. \layout Standard Exemple: la regla d' \emph on eliminació de la implicació \emph default no permet accedir així a les fórmules de la primera línia. \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 Per poder fer-ho, s'hauria d'estar segur de que \begin_inset Formula $P$ \end_inset és cert sempre; llavors sí que es podria aplicar la regla, escrivint bé els números de línia. \layout Subsection Iterar una fórmula d'una subdemostració no accesible \layout Standard A dins de la demostració principal (la qual va de la primera a l'última línia), podem obrir \emph on demostracions filles \emph default ( \emph on subdemostracions \emph default ). Dins d'una subdemostració també podem tenir una \emph on subsubdemostració \emph default , que tindria com pare a la subdemostració i com avi a la demostració principal. \layout Standard Per a il·lustrar, aquí poso l'exemple 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 Doncs bé, una demostració qualsevol només pot accedir a les fórmules de dins de si mateixa, a les del seu pare, a les del pare del seu pare, a les del pare del pare del seu pare, ... Em sembla que a tots aquest se'ls diu \emph on ancestres \emph default , així que: \emph on una demostració pot accedir a si mateixa i als seus ancestres \emph default . \layout Standard Per exemple, si estem a la línia 10, les regles poden usar fórmules dels següents llocs: \layout Itemize de la demostració actual (línies 8 i 9 ara per ara). \layout Itemize de la demostració pare de la 8-10, o sigui, de la línia 7. \layout Itemize de la demostració pare de la que comença a la línia 7, o sigui, línies 1 a 3. \layout Standard En cap cas pot usar les fórmules de les línies 4 a 6, que és la demostració \emph on oncle \emph default / \emph on tia \emph default de l'actual (germana del pare), perquè tota aquella demostració es basa en la hipòtesi que \begin_inset Formula $A$ \end_inset (línia 4), i ja hem deixat de fer aquella suposició. \layout Standard En llenguatge lògic, es diu que una fórmula \begin_inset Formula $A$ \end_inset és \emph on actual \emph default en la fórmula \begin_inset Formula $B$ \end_inset si estant en \begin_inset Formula $B$ \end_inset es pot usar \begin_inset Formula $A$ \end_inset . Per que això sigui possible, \begin_inset Formula $A$ \end_inset s'ha d'haver escrit abans que \begin_inset Formula $B$ \end_inset , i algun ancestre de \begin_inset Formula $B$ \end_inset ha de ser pare de \begin_inset Formula $A$ \end_inset . \layout Standard O sigui, que per demostrar \begin_inset Formula $P\wedge Q$ \end_inset no es pot fer això: \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 Posar malament els parèntesis \layout Standard Quan he escrit les definicions de les regles, he usat les lletres \begin_inset Formula $A$ \end_inset i \begin_inset Formula $B$ \end_inset , però aquestes poden representar qualsevol expressió. \layout Standard Per exemple, aquí es fa la \emph on introducció de la negació \emph default , on -segons la regla- es suposa una fórmula \begin_inset Formula $A$ \end_inset , s'arriba a una contradicció, i es conclou que \begin_inset Formula $\neg A$ \end_inset , o sigui, la fórmula original, però negada. Vegem: \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 Suposo que queda clar que el \begin_inset Formula $A$ \end_inset que surt a la regla representa a \begin_inset Formula $P\Rightarrow Q$ \end_inset en aquest exemple. El problema el tenim quan fem el \begin_inset Formula $\neg A$ \end_inset . La negació de \begin_inset Formula $P\Rightarrow Q$ \end_inset no és \begin_inset Formula $\neg P\Rightarrow Q$ \end_inset , sinó \begin_inset Formula $\neg(P\Rightarrow Q)$ \end_inset . És necessari el parèntesi perquè si no es posa, només afecta a \begin_inset Formula $P$ \end_inset . \layout Standard Si no saps quan posar parèntesis, posa'ls sempre i després treu els que no facin falta. Per exemple, si has d'escriure que \begin_inset Formula $\neg P\vee R$ \end_inset implica a \begin_inset Formula $R\wedge Q$ \end_inset , envolta cada expressió en parèntesis i escriu \begin_inset Formula $(\neg P\vee R)\Rightarrow(R\wedge Q)$ \end_inset . Així no t'has equivocat. Ara aprèn quan és possible treure els parèntesis, i treu tots els que puguis. En aquest cas, tots dos es poden treure i queda \begin_inset Formula $\neg P\vee R\Rightarrow R\wedge Q$ \end_inset . \layout Subsection Acabar dins d'una subdemostració \layout Standard No pots acabar la deducció dins d'una subdemostració. L'última línia no ha de tenir cap ratlleta vertical a l'esquerra. \layout Standard La raó és que tot el que hi ha a dins de la subdemostració és vàlid només quan es compleix la suposició, i el que ens demanen a l'enunciat és demostrar que el que hi ha a la dreta del \begin_inset Formula $\vdash$ \end_inset es compleix \emph on sempre \emph default . \layout Standard Exemple d'algú amb molta cara intentant demostrar \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 S'ha suposat que \begin_inset Formula $P$ \end_inset , i també que \begin_inset Formula $Q$ \end_inset . En aquest cas, és clar que \begin_inset Formula $P\wedge Q$ \end_inset és cert, però només en aquest cas. No podem assegurar a ningú que \begin_inset Formula $P\wedge Q$ \end_inset sigui cert sempre. Per tant, s'hauria d'anar tancant cada demostració (primer la de dins, i després la de fora) per intentar treure alguna conclusió que sigui vàlida sempre. \layout Standard Tampoc es podria fer allò d' \emph on iterar \emph default en la línia 4. Ja ho he explicat fa alguns apartats. \layout Subsection Saltar-se passos \layout Standard Encara que coneguis equivalències entre fórmules, és molt millor si no les uses. Per exemple, si et toca escriure la negació de \begin_inset Formula $\neg P$ \end_inset , no pots posar \begin_inset Formula $P$ \end_inset directament, sinó que s'ha de posar \begin_inset Formula $\neg\neg P$ \end_inset . \layout Standard Pensa que no tot és tan obvi com sembla, i que et poden demanar demostrar coses com \begin_inset Formula $P\vdash\neg\neg P$ \end_inset , a on si poguessis usar les simplificacions, gairebé no hi hauria treball a fer. \layout Standard Per exemple, passar de tenir \begin_inset Formula $\neg(A\vee B)$ \end_inset en una línia a tenir \begin_inset Formula $\neg A\wedge\neg B$ \end_inset a la següent no es pot justificar amb cap de les 9 regles. Però si aconsegueixes demostrar i comprendre que \begin_inset Formula $\neg(A\vee B)\vdash\neg A\wedge\neg B$ \end_inset , aleshores podries afegir-ho com una regla addicional per usar-la en futures demostracions. Dono vàries d'aquestes a la propera secció. \layout Section Complicant-ho una mica més \layout Standard Aquí acabo d'explicar tot allò que em van ensenyar (tot i que no ho vam usar gaire). El tema dels quantificadors és important però més enrevessat. \layout Subsection Regles de cert i fals \layout Standard Podem treballar directament amb els valors \begin_inset Formula $\blacksquare$ \end_inset ( \emph on cert \emph default ) i \begin_inset Formula $\square$ \end_inset ( \emph on fals \emph default ), i també ficar-los o fer-los fora de la nostra demostració amb regles senzilles. \layout Subsubsection Introducció de cert \layout Standard Aquesta és la més fàcil que hi ha: \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 O sigui, que sempre, i sense cap requisit, podem deixar escrit que \begin_inset Formula $\blacksquare$ \end_inset és cert, perquè sempre ho és. \layout Subsubsection Eliminació de fals \layout Standard Una regla molt divertida: \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 Explicació: si hem arribat a la conclusió de que \begin_inset Formula $\square$ \end_inset és cert, llavors ja hem arribat a l'extrem en què podem inventar-nos qualsevol cosa i dir que és certa; al menys, tan certa com que \begin_inset Formula $\square$ \end_inset ( \emph on fals \emph default ) és cert. \layout Standard A aquesta regla li diuen \emph on ex falso quodlibet sequitur \emph default , que deu voler dir \begin_inset Quotes eld \end_inset \emph on de fals pot sortir qualsevol cosa \emph default \begin_inset Quotes erd \end_inset . \layout Subsection Regles de quantificadors \layout Standard Estem molt limitats si només podem usar \begin_inset Formula $P$ \end_inset , \begin_inset Formula $Q$ \end_inset , \begin_inset Formula $R$ \end_inset , ... per traduir frases a llenguatge lògic. Els quantificadors ens permetran fer moltes més coses. \layout Subsubsection Què és això \layout Standard No podré explicar-ho tot perquè fa falta entendre molts conceptes previs, però ho dic una mica per sobre. El primer, uns canvis: \layout Standard Ara no només parlarem de coses generals ( \emph on plou \emph default , \emph on fa calor \emph default , etc.), sinó que tindrem un \emph on domini \emph default de coses conegudes, i haurem de dir quina propietat és certa per a cada element. \layout Standard Exemple: tenim el domini \begin_inset Formula $\{ p,\ t,\ r\}$ \end_inset , que representen a la pantalla, el teclat, i el ratolí d'un ordinador. \layout Standard Afegim una \emph on lletra de predicat \emph default (ja no es diuen \emph on lletres proposicionals \emph default ) \begin_inset Formula $E$ \end_inset , tal que quan posem \begin_inset Formula $Ex$ \end_inset (llegit \begin_inset Quotes eld \end_inset \emph on \begin_inset Formula $E$ \end_inset de \begin_inset Formula $x$ \end_inset \emph default \begin_inset Quotes erd \end_inset , escrit tot junt) volem dir que \emph on \begin_inset Formula $x$ \end_inset és un dispositiu d'entrada \emph default . També tenim \begin_inset Formula $Sx$ \end_inset per dir que \emph on \begin_inset Formula $x$ \end_inset és un dispositiu de sortida \emph default , i \begin_inset Formula $Tx$ \end_inset que significarà \emph on \begin_inset Formula $x$ \end_inset necessita tinta per funcionar \emph default . \layout Standard Ara sabem que es compleixen \begin_inset Formula $Et$ \end_inset , \begin_inset Formula $Er$ \end_inset , \begin_inset Formula $Sp$ \end_inset i cap més. \layout Standard Els quantificadors ens permetran escriure veritats que facin referència a alguns elements del domini. N'hi ha dos, de quantificadors: \layout Itemize El quantificador universal: \begin_inset Formula $\forall$ \end_inset . Quan es posa \begin_inset Formula $\forall xPx$ \end_inset ( \begin_inset Quotes eld \end_inset \emph on per tot \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 ), es vol dir que tots els elements del domini compleixen la propietat \begin_inset Formula $P$ \end_inset . \layout Itemize El quantificador existencial: \begin_inset Formula $\exists$ \end_inset . \begin_inset Formula $\exists xPx$ \end_inset ( \begin_inset Quotes eld \end_inset \emph on existeix un \begin_inset Formula $x$ \end_inset tal que \begin_inset Formula $P$ \end_inset de \begin_inset Formula $x$ \end_inset \emph default \begin_inset Quotes erd \end_inset ) vol dir que al menys un element del domini fa certa la propietat \begin_inset Formula $P$ \end_inset . \layout Standard Per exemple, aquí són certes les següents fórmules: \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 i moltes més. Els quantificadors tenen tanta prioritat com el \begin_inset Formula $\neg$ \end_inset . \layout Standard Les regles explicades aquí treballaran amb \emph on substitucions lliures \emph default . Ho sento per no explicar què és, però és que no em vull sortir del tema. \layout Subsubsection Introducció de l'existencial \layout Standard Si veiem una prova de la seva existència, podem dir que una propietat es compleix per algun element: \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 Això de \begin_inset Formula $A\{ t/x\}$ \end_inset és una \emph on substitució \emph default (es llegeix \begin_inset Quotes eld \end_inset \emph on \begin_inset Formula $t$ \end_inset sobre \begin_inset Formula $x$ \end_inset \emph default \begin_inset Quotes erd \end_inset i consisteix en canviar \begin_inset Formula $x$ \end_inset per \begin_inset Formula $t$ \end_inset ). \layout Standard Aquesta regla diu que si veiem \begin_inset Formula $At$ \end_inset , on \begin_inset Formula $t$ \end_inset és un element, podem dir que \begin_inset Formula $\exists xAx$ \end_inset , perquè sabem que quan \begin_inset Formula $x$ \end_inset és \begin_inset Formula $t$ \end_inset sí que es compleix. \layout Subsubsection Eliminació de l'existencial \layout Standard Treure quelcom cert d'un \begin_inset Formula $\exists xPx$ \end_inset costa, però es fa així: \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 O sigui, que si un dels \begin_inset Formula $A$ \end_inset implica \begin_inset Formula $B$ \end_inset , llavors sabem que \begin_inset Formula $B$ \end_inset , perquè sabem que un dels \begin_inset Formula $A$ \end_inset és cert. No ha d'aparèixer cap \begin_inset Formula $a$ \end_inset en \begin_inset Formula $B$ \end_inset ni en cap hipòtesi accesible (perdó per les frases críptiques; són part de la teoria). \layout Subsubsection Introducció de l'universal \layout Standard Aquesta és bastant fàcil: \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 O sigui, que si \begin_inset Formula $A$ \end_inset es compleix sempre, es compleix per qualsevol valor de \begin_inset Formula $x$ \end_inset . No ha d'haver cap \begin_inset Formula $x$ \end_inset \emph on lliure \emph default en cap hipòtesi accesible. \layout Subsubsection Eliminació de l'universal \layout Standard Una altra fàcil d'entendre: \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 Si sabem que \begin_inset Formula $A$ \end_inset es compleix per qualsevol element, llavors podem escollir un element qualsevol i sabem que es complirà \begin_inset Formula $A$ \end_inset en aquell element. \layout Subsubsection Exemples \layout Standard A l'última secció hi ha algun exemple amb quantificadors, però sense explicar. Suposo que hauràs de mirar algun llibre de lògica si t'interessa entendre'ls. \layout Subsection Regles derivades \layout Standard A molts llibres i tutorials s'accepta tenir altres regles (apart de les 9 bàsiques) que permeten tractar amb les fórmules més fàcilment. Representen una abstracció: deixar de pensar en els detalls per dedicar-se a problemes més complicats (és com allò dels llenguatges de programació d' \emph on alt nivell \emph default ). \layout Standard Si decideixes usar-les, et perdràs moltes coses interessants per fer, però acabaràs abans. El meu consell és que utilitzis una regla només si saps demostrar la seva validesa mitjançant les 9 bàsiques. \layout Standard Algunes de les que vaig trobar per diversos llocs són: \layout Itemize \emph on Llei de doble negació \emph default : permet passar de \begin_inset Formula $A$ \end_inset a \begin_inset Formula $\neg\neg A$ \end_inset i viceversa. \layout Itemize \emph on Modus Tollens \emph default : si tens \begin_inset Formula $A\Rightarrow B$ \end_inset i \begin_inset Formula $\neg B$ \end_inset , llavors \begin_inset Formula $\neg A$ \end_inset . \layout Itemize \emph on Sil·logisme disjuntiu \emph default : si \begin_inset Formula $A\vee B$ \end_inset i \begin_inset Formula $\neg A$ \end_inset , llavors \begin_inset Formula $B$ \end_inset . I si \begin_inset Formula $A\vee B$ \end_inset i \begin_inset Formula $\neg B$ \end_inset , llavors és que \begin_inset Formula $A$ \end_inset . \layout Itemize \emph on Eliminació de \begin_inset Formula $\neg$ \end_inset \begin_inset Formula $\Rightarrow$ \end_inset \emph default : si tens \begin_inset Formula $\neg(A\Rightarrow B)$ \end_inset , llavors passen tant \begin_inset Formula $A$ \end_inset com \begin_inset Formula $\neg B$ \end_inset . \layout Itemize \emph on Eliminació de \begin_inset Formula $\neg$ \end_inset \begin_inset Formula $\vee$ \end_inset \emph default : si tens \begin_inset Formula $\neg(A\vee B)$ \end_inset , llavors \begin_inset Formula $\neg A$ \end_inset , i també \begin_inset Formula $\neg B$ \end_inset . \layout Itemize \emph on Eliminació de \begin_inset Formula $\neg\wedge$ \end_inset \emph default : si tens \begin_inset Formula $\neg(A\wedge B)$ \end_inset , llavors \begin_inset Formula $\neg A\vee\neg B$ \end_inset . \layout Itemize \emph on Teoremes que pots incorporar quan vulguis \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 i més. \layout Itemize \emph on Canvi de fórmules equivalents \emph default : si \begin_inset Formula $A\Longleftrightarrow B$ \end_inset , llavors on vegis \begin_inset Formula $A$ \end_inset pots posar \begin_inset Formula $B$ \end_inset i viceversa. \layout Standard N'hi ha moltes més; però si et demanen fer un exercici ja et diran quines regles estan permeses i quines no (per exemple, a nosaltres només ens deixaven usar les bàsiques). \layout Section Extra \layout Standard Si ja sabies tot això que he explicat, o tens dubtes que no tenen a veure amb el com es fa, queda't a aquesta secció. \layout Subsection Per què es diu deducció natural? \layout Standard Perquè els procediments que s'han d'usar són els mateixos que els que fa la gent en pensar. \layout Standard Fixa't en els exercicis resolts. Expressa els seqüents en forma de paraules, digues-els a algú, i acabarà dient-te que \begin_inset Quotes eld \end_inset \emph on és clar que és així, perquè ... \emph default \begin_inset Quotes erd \end_inset . Veuràs que qualsevol és capaç d'explicar-te com s'usen algunes de les 9 regles, encara que no coneguin el nom o ni tals sols la seva existència. \layout Standard Per aquesta raó, si vols descobrir com fer un cert exercici de deducció natural, oblida't de regles de \emph on introducció \emph default i \emph on eliminació \emph default , i pensa de forma normal, canviant les lletres per accions senzilles si fa falta. Va molt bé pensar en tot això de \emph on plou \emph default , \emph on no plou \emph default , \emph on fa sol \emph default , \emph on no em mullo \emph default , ... perquè són paraules curtes i a més tothom té molt clar què passa quan plou, i relacionen ràpidament el \emph on no mullar-se \emph default amb el \emph on fer sol i no ploure \emph default , i fins i tot fórmules molt més complexes. \layout Subsection La solució és única? \layout Standard No. Quant més complicat és l'exercici, més formes correctes hi ha de solucionar-ho. A la secció dels exercicis explicats ja hi ha algun pel qual dono més d'una versió. \layout Standard Naturalment, pots començar a deduir coses que no serveixin de res, i aconseguirà s una solució diferent a les altres. Però és millor intentar fer cada exercici el més curt possible. \layout Subsection Altres formes de demostrar validesa \layout Standard La deducció natural és una forma de demostrar la validesa d'un seqüent, però n'hi ha més. Altres són: \layout Subsubsection Força bruta \layout Standard Podem llistar totes les possibles combinacions de valors per cada variable, i comprovar que, per cada una, si la part esquerra del seqüent es compleix llavors la part dreta també. \layout Standard Si hi ha \begin_inset Formula $n$ \end_inset variables, farà falta comprovar \begin_inset Formula $2^{n}$ \end_inset casos. \layout Standard El problema està en si hi ha quantificadors, perquè llavors ja hi intervé un domini. I no podem llistar alguns dels possibles dominis existents, perquè un domini pot contenir infinits elements. \layout Subsubsection Teorema de refutació \layout Standard El teorema de refutació diu que \begin_inset Formula $\Gamma\vDash A\Longleftrightarrow\ \nVdash\Gamma,\neg A$ \end_inset . \layout Standard En paraules: el conjunt de fórmules \begin_inset Formula $\Gamma$ \end_inset ( \emph on gamma \emph default ) té com conseqüència a \begin_inset Formula $A$ \end_inset \emph on si i només si \emph default el sistema format per \begin_inset Formula $\Gamma$ \end_inset junt amb \begin_inset Formula $\neg A$ \end_inset és insatisfactible. \layout Standard El com demostrar la \emph on insatisfactibilitat \emph default és un altre tema, bastant llarg, tal com el seu nom suggereix. Un dels mètodes fàcils d'usar és el de l'arbre de \emph on resolució \emph default clausular. \layout Subsection Com demostrar la invalidesa \layout Standard La deducció natural dóna un procediment per demostrar que un raonament és correcte, però com es demostra que un raonament és erroni? No es pot fer amb deducció natural. \layout Standard Estem en aquest cas: tenim el seqüent \begin_inset Formula $\Gamma\vdash A$ \end_inset , i creiem que hi ha un \emph on model \emph default (conjunt de valors) que fa cert a \begin_inset Formula $\Gamma$ \end_inset - \emph on gamma \emph default - però no a \begin_inset Formula $A$ \end_inset . Doncs tan sols hem de trobar-lo per demostrar que el seqüent és invàlid. A aquest model se l'anomena \emph on contramodel \emph default , i es pot trobar de moltes formes. Crec que la més senzilla és \emph on fer-ho a ull \emph default : anar provant diferents valors que creiem que poden ser contramodel, fins trobar-ne un. \layout Standard Per exemple, \begin_in