Regla d'inferència

Plantilla:Regles de transformació En llògica, una regla d'inferència, o regla de transformació és una forma llògica que consistix en una funció que pren premisses, analisa la seua sintaxis, i torna una conclusió (o conclusions).

Per eixemple, la regla d'inferència modus ponendo ponens pren dos premisses, un en la forma «Si p, llavors q» i una atra en la forma «p», i torna la conclusió «q». La regla és vàlida sobre la semàntica de la llògica clàssica (aixina com la semàntica de moltes atres llògiques no clàssiques), en el sentit de que si les premisses són verdaderes (baixe una interpretació), llavors també ho serà la conclusió.

Per lo general, una regla d'inferència conserva la veritat, una propietat semàntica. En molts valors llògics, esta conserva una designació general. Pero l'acció de la regla d'inferència és purament sintàctica, i no és necessari preservar cap propietat semàntica: qualsevol funció de conjunts de fòrmules conta com una regla d'inferència.

Llavors, encara que l'aplicació d'una regla d'inferència és un procediment purament sintàctic, deu preservar la validea. Per a que el requisit de preservació de la validea tinga sentit, és necessària una certa forma semàntica per a les asserció de les regles d'inferència i les regles d'inferència en sí mateixes.

Les regles significatives d'inferència en la llògica proposicional inclouen modus ponens, modus tollens i contraposició. La llògica de predicats de primer orde usa regles d'inferència per a liderar en quantificadors llògics.

La forma estàndar de regles d'inferència

En llògica formal (i moltes àrees relacionades), les regles d'inferència solen donar-se generalment en la següent forma estàndar:

  Premissa#1
  Premissa#2
        ...
  Premissan
  Conclusió

Esta expressió indica que cada volta que en el curs s'haja obtingut alguna derivació llògica a partir de les premisses donades, la conclusió especificada pot donar-se també per assentat . El llenguage formal exacte utilisat per a descriure tant premisses com les conclusions depén del context real de les derivació. En un cas senzill, es pot utilisar fòrmules llògiques, tals com en:

\begin{matrix} A \to B \\ A \\ ∴ & B \end{matrix}

Esta és la regla modus ponendo ponens de la llògica proposicional. Per lo general, les regles d'inferència es formulen com esquemes amprant metavariables.^[1] En la regla (esquema), les metavariables A i B poden crear instàncies de qualsevol element de l'univers (o, a voltes, per convenció, un subconjunt restringit com proposicions) per a formar un conjunt infinit de regles d'inferència.

Un sistema de prova està format per un conjunt de regles encadenades entre sí per a formar proves, també cridades derivació. Qualsevol derivació té una sola conclusió final, que és la declaració provada o derivada. Si les premisses queden insatisfetes en la derivació, en conseqüència, la derivació és una prova d'una declaració hipotètica: «si les premisses es mantenen, llavors la conclusió és vàlida».

Eixemple: Sistemes de Hilbert per a dos proposicions llògiques

En un sistema de Hilbert, les premisses i la conclusió de les regles d'inferència són simplement fòrmules d'algun llenguage, usualment amprant metavariables. Per compacidad gràfica de la presentació i fent recalcament en la distinció entre axioma i regles d'inferència, esta secció utilisa la notació secuente (⊢) en lloc d'una presentació de regles en forma vertical.

El llenguage formal de la llògica proposicional clàssica es pot expressar usant solament la negació (¬), l'implicació (→) i els símbols proposicionals. Una axiomatisació molt coneguda, que comprén tres esquema del axioma i una regla d'inferència (modus ponendo ponens), és:

(CA1) ⊢ A → (B → A)

(CA2) ⊢ (A → (B → C)) → ((A → B) → (A → C))

(CA3) ⊢ (¬A → ¬B) → (B → A)

(MP)  A, A → B ⊢ B

Esta seqüència diferix de la llògica clàssica pel canvi en axioma 2 i l'adició d'axioma 4. El teorema de la deducció clàssic no es complix en esta llògica; sí ho fa una forma modificada: A ⊢ B si i solament si ⊢ A → (A → B). No obstant, existix una distinció a destacar també en este cas: la primera notació descriu una deducció, que és una activitat de passar de sentències a sentències; mentres que A → B és simplement una fòrmula integrada en un conector llògic, en est case implicació. Sense una regla d'inferència (en este cas com modus ponens), no hi ha cap deducció o inferència. Este punt s'ilustra en el diàlec de Lewis Carroll cridat «Lo que la tortuga va dir a Achilles».^[2]

En algunes llògiques no clàssiques, no es complix la teorema de deducció. Per eixemple, la llògica trivalente Ł3 de Łukasiewicz pot ser axiomatizada com:^[3]

(CA1) ⊢ A → (B → A)

(LA2) ⊢ (A → B) → ((B → C) → (A → C))

(CA3) ⊢ (¬A → ¬B) → (B → A)

(LA4) ⊢ ((A → ¬A) → A) → A

(MP)  A, A → B ⊢ B

Esta seqüència diferix de la llògica clàssica pel canvi en axioma 2 i l'adició d'axioma 4. La teorema de deducció clàssica no es complix per a esta llògica, no obstant si ho fa una forma modificada , a saber, A ⊢ B si i solament si ⊢ A → (A → B).^[4]

Vore també

Referències

↑ John C. Reynolds (2009). Theories of Programming Languages (en anglés), Cambridge University Press, p. 12. ISBN 978-0-521-10697-9.
↑
Kosta Dosen (1996). «Logical consequence: a turn in style», Maria Luisa Dalla Chiara, Kees Doets, Daniele Mundici, Johan van Benthem (ed.). Logic and Scientific Methods: Volume One of the Tenth International Congress of Logic, Methodology and Philosophy of Science, Florence, Agust 1995, Springer, p. 290. ISBN 978-0-7923-4383-7. preprint (en diferent paginació)
- Archivat el 1 de febrer de 2014 archivat en Wayback Machine.
↑ Bergmann, Merrie (2008). An introduction to many-valued and fuzzy logic: semantics, algebras, and derivation systems, Cambridge University Press, p. 100. ISBN 978-0-521-88128-9.
↑ Bergmann, Merrie (2008). An introduction to many-valued and fuzzy logic: semantics, algebras, and derivation systems, Cambridge University Press, p. 114. ISBN 978-0-521-88128-9.

Referències

Este artícul conté una traducció derivada de «Regla de inferencia» de Wikipedia en castellà publicada baix la Llicència de documentació lliure de GNU i la Llicència Creative Commons Reconeiximent-CompartirIgual 4.0 Internacional.

[Reynolds2009-1] John C. Reynolds (2009). Theories of Programming Languages (en anglés), Cambridge University Press, p. 12. ISBN 978-0-521-10697-9.

[ChiaraDoets1996-2] Kosta Dosen (1996). «Logical consequence: a turn in style», Maria Luisa Dalla Chiara, Kees Doets, Daniele Mundici, Johan van Benthem (ed.). Logic and Scientific Methods: Volume One of the Tenth International Congress of Logic, Methodology and Philosophy of Science, Florence, Agust 1995, Springer, p. 290. ISBN 978-0-7923-4383-7. preprint (en diferent paginació)
Archivat el 1 de febrer de 2014 archivat en Wayback Machine.

[3] Archivat el 1 de febrer de 2014 archivat en Wayback Machine.

[3] Bergmann, Merrie (2008). An introduction to many-valued and fuzzy logic: semantics, algebras, and derivation systems, Cambridge University Press, p. 100. ISBN 978-0-521-88128-9.

[4] Bergmann, Merrie (2008). An introduction to many-valued and fuzzy logic: semantics, algebras, and derivation systems, Cambridge University Press, p. 114. ISBN 978-0-521-88128-9.

[1]

[2]

[3]

[4]