Conseqüent

En llògica matemàtica, un conseqüent és un tipo molt general d'afirmació condicional.

$A_1,\dots ,A_m⊢B_1,\dots ,B_n.$

Un conseqüent pot tindre qualsevol número m de les fòrmules de condició Ai (cridades "antecedents") i qualsevol número n de fòrmules B_j declarades (cridades "sucedentes" o "secuentes"). S'entén que un conseqüent significa que si totes les condicions antecedents són verdaderes, llavors a lo manco una de les fòrmules conseqüents és verdadera. Este estil d'asserció condicional està casi sempre associat en el marc conceptual del càlcul de conseqüents.

Introducció

Els conseqüents es comprenen millor en el context dels següents tres tipos de juïns llògics:

1. Afirmació incondicional. No hi ha fòrmules antecedents.
   • Eixemple: ⊢ B
   • Significat: B és verdader. Qualsevol número de fòrmules anteriors.
2. Asserció condicional.
   Simple asseveració condicional. Fòrmula única conseqüent.
   • Eixemple: A₁, A₂, A₃ ⊢ B
   Significat: SI A₁ I A₂ I A₃ són verdaders, llavors B és verdader.
   1. Conseqüent. Qualsevol número de fòrmules conseqüents.
      • Eixemple: A₁, A₂, A₃ ⊢ B₁, B₂, B₃, B₄
      • Significat: SI A₁ I A₂ I A₃ són verdaders, ENTONCES B₁ O B₂ OR B₃ OR B₄ és verdader.

Aixina, els conseqüents són una generalisació d'afirmacions condicionals simples, que són una generalisació de asserció incondicionals.

La paraula "O" ací és l'OR inclusivo. La motivació per a la semàntica disjuntiva en el costat dret d'un conseqüent du en si tres ventages principals.

1. La simetria de les regles d'inferència clàssiques per a seqüències en semàntica semblant.
2. La facilitat i senzillea de convertir tals regles clàssiques a regles intuicionistas.
3. La capacitat de demostrar l'integritat del càlcul predicat quan s'expressa d'esta manera.

Estos tres beneficis varen ser identificats en el document de fundació de Gentzen (1934, p. 194).

No tots els autors es varen adherir al significat original de Gentzen per a la paraula "conseqüent". Per eixemple,Lemmon (1965) va usar la paraula "conseqüent" estrictament per a afirmacions condicionals simples en una i només una fòrmula conseqüent. La mateixa definició consecutiva per a un secuente és donada per Huth & Ryan 2004, p. 5.

Detalls de la sintaxis

El conseqüent té la forma:

$\Gamma ⊢\Sigma$

a on tant Γ com Σ són seqüències de fòrmules llògiques, no conjunts. Per lo tant són significatius tant el número com l'orde d'aparicions de les fòrmules. En particular, la mateixa fòrmula pot aparéixer dos voltes en la mateixa seqüència. El conjunt complet de regles d'inferència de càlcul seqüencial conté regles per a intercanviar fòrmules adjacents a l'esquerra i a la dreta del símbol d'asserció (i per lo tant permutar arbitrariamente els conseqüents de l'esquerra i de la dreta), i també per a insertar fòrmules arbitràries i eliminar còpies duplicades dins de l'esquerra i els conseqüents correctes. (No obstant, Smullyan (1995, pp. 107-108), utilisa conjunts de fòrmules en seqüències en lloc de seqüències de fòrmules. En conseqüència, no es requerixen els tres parells de regles estructurals cridades "adelgazamiento", "contracció" i "intercanvi".)

El símbol ' $⊢$ ' es referix a voltes com "torniquet", "tachuela dreta", "tee", "signe d'asserció" o "símbol d'asserció". Per lo general es llig, sugestivamente, com "produïx", "demostra" o "implica".

Propietats

Efectes d'insertar i eliminar proposicions

ya que cada fòrmula en l'antecedent (el costat esquerre) deu ser verdadera per a concloure la veritat de per lo manco una fòrmula en el sucediente (el costat dret), agregant les fòrmules a cada costat dona lloc a un conseqüent més dèbil, mentres que llevant d'abdós costats dona un més fort. Esta és una de les ventages de simetria que es deriva de l'us de la semàntica disyuntiva en el costat dret del símbol de l'asserció, mentres que la semàntica conjuntiva s'inserta en el costat esquerre.

Conseqüències de llistes buides de fòrmules

En el cas extrem a on la llista de fòrmules antecedents d'un conseqüent està buida, el conseqüent és incondicional. Açò diferix de la simple afirmació incondicional perque el número de conseqüents és arbitrari, no necessàriament un sol conseqüent. Per eixemple, ' ⊢ B₁, B₂ significa que B₁, o B₂, o abdós, deuen ser verdaders. Una llista de fòrmules antecedents buides és equivalent a la proposició "sempre verdadera", cridada "tautologia", denominada "⊤". (Vore T (símbol).)

En el cas extrem a on la llista de fòrmules conseqüents d'un conseqüent estiga buida, la regla és que a lo manco un terme a la dreta és verdader, la qual cosa és clarament impossible. Açò és significat per la proposició "sempre falsa", cridada "contradiccion, o absurt", que es denomina "⊥". Com a conseqüència és falsa, a lo manco un dels antecedents deu ser fals. Per eixemple, ' A₁, A₂ ⊢ ' significa que a lo manco un dels antecedents A₁ A₂ deu ser fals.

Es veu ací de nou una simetria a causa de la semàntica disyuntiva en el costat dret. Si el costat esquerre està buit, llavors una o més proposicions del costat dret deuen ser verdaderes. Si el costat dret està buit, llavors una o més de les proposicions del costat esquerre deuen ser falses.

El cas doblement extrem '⊢', a on les llistes de fòrmules antecedents i conseqüents estiguen buides, és "no satifactorio, ni fiable ". En este cas, el significat del conseqüent és efectivament '⊤ ⊢ ⊥'. Açò és equivalent al següent '⊢ ⊥', que clarament no pot ser vàlit.

Eixemples

Una seqüència de la forma 'α, β', per a les fòrmules llògiques α i β, significa que α és verdadera o β és verdadera. Pero no significa que α o β siguen tautologia. Per a aclarir açò, considerar l'eixemple ' ⊢ B ∨ A, C ∨ ¬A'. Esta és una seqüència vàlida ya siga perque B ∨ A és verdader o C ∨ ¬A és verdader. Pero cap d'estes expressions és una tautologia aïllada. És la disjunció d'estes dos expressions la que és una tautologia.

De la mateixa manera, un conseqüent en la forma 'α, β ⊢', per a les fòrmules llògiques α i β, significa que α és fals o β és fals. Pero açò no significa que α és una contradicció o β és una contradicció. Per a aclarir açò, considere l'eixemple 'B ∧ A, C ∧ ¬A ⊢'. Est és un conseqüent vàlit perque B ∧ A és fals o C ∧ ¬A és fals. Pero cap d'estes expressions és una contradicció aïllada. La conjunció d'estes dos expressions és una contradicció.

Regles

La majoria dels sistemes de demostració proporcionen maneres de deduir una conseqüent d'un atre. Estes regles d'inferència s'escriuen en una llista de seqüències per damunt i per baix d'una llínea. Esta regla indica que si tot lo que està per damunt de la llínea és verdader, també ho és tot lo que està baix la llínea.

Una regla típica és:

$\frac{\Gamma ,\alpha ⊢\Sigma \Gamma ⊢\Sigma ,\alpha }{\Gamma ⊢\Sigma }$

Açò indica que, si és possible deduir que $\Gamma ,\alpha$ du a $\Sigma$ i que $\Gamma$ du a $\Sigma ,\alpha$, llavors també és possible deduir que $\Gamma$ du a $\Sigma$. (Vore també el conjunt complet de regles d'inferència de càlcul seqüencial.)

Interpretació

Història del significat de les afirmacions successives

El símbol d'asserció en conseqüents originalment significava exactament lo mateix que l'operador d'implicació. Pero en el temps, el seu significat ha canviat per a significar demostrabilidad dins d'una teoria més que la veritat semàntica en tots els models.

En 1934, Gentzen no va definir el símbol d'asserció '⊢' en un conseqüent per a significar provabilitat. Ell ho va definir per a significar exactament igual que l'operador de l'implicació "⇒". Usant '→' en lloc de '⊢' i '⊃' en lloc de '⇒', va escriure: "El conseqüent A₁, ..., A_μ → B₁, ..., B_ν significa, sobre el contingut, exactament igual que la fòrmula (A₁ & ... & A_μ) ⊃ (B₁ ∨ ... ∨ B_ν)". (Gentzen va amprar el símbol de la flecha dreta entre els antecedents i els conseqüents dels successius, amprant el símbol ' ⊃ ' per a l'operador de l'implicació llògica).

Aixina mateix, en 1939, Hilbert i Bernays varen declarar que un conseqüent té el mateix significat que la corresponent fòrmula d'implicació.

"No obstant, l'us del teorema de la deducció com a regla primitiva o derivada no deu confondre's en l'us de Sequenzen de Gentzen. Per a la flecha de Gentzen, →, no és comparable a la nostra notació sintàctica, ⊢, sino que pertany al seu llenguage objecte (com es desprén del fet de que les expressions que ho contenen apareixen com a premisses i conclusions en les aplicacions de les seues regles d'inferència)."

Numeroses publicacions despuix d'este temps han declarat que el símbol d'asserció en secuentes sí significa provabilitat dins de la teoria a on es formulen els conseqüents. Curry en 1963, Lemmon en 1965, and Huth and Ryan en 2004 tots els estats que el símbol d'asserció conseqüent significa provabilitat. No obstant,Ben-Ari (2012, p. 69) va afirmar que el símbol d'asserció en les conseqüències del sistema de Gentzen, que va denotar com ' ⇒ ', és part del llenguage d'objectes, no del metallenguage.

Intuitivamente, un conseqüent representa una 'forma provable' en el sentit de que les fòrmules en O són suposicions per al conjunt de fòrmules V que han de provar-se. El símbol ⇒ és similar al símbol ⊢ en sistemes de Hilbert, excepto que ⇒ és part del llenguage d'objecte del sistema deductivo que s'està formalisant, mentres que ⊢ és una notació de metallenguage usada per a raonar sobre sistemes deductivos."</ref>

Segons Prawitz (1965): "Els càlculs de conseqüents poden ser entesos com fique-càlculs per a la relació de deducibilidad en els sistemes corresponents de deducció natural." I ademés: "Una prova en un càlcul de conseqüents pot ser vista com una instrucció sobre cóm construir una deducció natural corresponent." En atres paraules, el símbol d'asserció és part del llenguage d'objectes per al càlcul seqüencial, que és una espècie de meta-càlcul, pero simultàneament significa deducibilidad en un sistema de deducció natural subjacent.

Significat intuïtiu

El significat intuïtiu d'un subsegüent $\Gamma ⊢\Sigma$ és tal que, baixe el supòsit de Γ, és demostrabe la conclusió de Σ. Clásicamente, les fòrmules a l'esquerra del trinquet poden ser interpretades com una conjunció, mentres que les fòrmules de la dreta poden considerse com una disjunció. Açò significa que si totes les fòrmules en el conjunt Γ anaren verdaderes, llavors per lo manco una fòrmula Σ també té que ser verdadera. Si el sucedente està buit, s'interpreta esta situació com una falsetat, és dir, $\Gamma ⊢$ significa que Γ/implica falsetat i per lo tant és inconsistente. Per un atre costat, assumim un buit com a verdader, és dir, $⊢\Sigma$ significa que Σ procedix sense cap supòsit, o siga, la disjunció és sempre verdadera. Una afirmació llògica es veu com un secuente en el format $⊢\Sigma$.

Són possibles atres explicacions intuïtives equivalents. Per eixemple, $\Gamma ⊢\Sigma$ pot llegir-se com una afirmació de que no és provable que es produïxca un cas en el que totes les fòrmules de Γ siguen verdaderes i totes les fòrmules de Σ siguen falses (açò està relacionat en la regla d'inferència de la doble negació).

En qualsevol cas, estes llectures intuïtives són de propòsit merament pedagògic. Cóm les proves formals en teoria de la prova són purament sintàctica, la semàntica de (o derivació de) un subsegüent es dona solament per les propietats del càlcul que determina les regles d'inferència.

Llevat qualsevol contradicció en la definició tècnica donada anteriorment, podem descriure conseqüents en la mateixa forma llògica. L'expressió $\Gamma$ representa un conjunt de suposicions en les quals comencem el nostre procés llògic. Per eixemple: "Sócrates és humà" i "Tots els humans són mortals". El símbol $\Sigma$ representa una conclusió llògica és frut del resultat d'eixes premisses. Per eixemple, la conclusió "Sócrates és mortal" és frut del resultat d'una formalisació raonable dels supòsits mencionats anteriorment, i per lo tant es pot insertar en el costat dret, $\Sigma$, del trinquet. Per lo tant, el símbol $⊢$ pot ser interpretat com el procés de raonament, o "per lo tant" en espanyol.

Vore també

• Llògica intuicionista
• Gerhard Gentzen
• Deducció natural

Bibliografia

• (1993) Mathematical logic for computer science, Londres: Springer. ISBN 978-1-4471-4128-0.
• (1944) Introduction to mathematical logic, Princeton, Nova Jersey: Princeton University Press. ISBN 978-0-691-02906-1.

• (1963) Foundations of mathematical logic, Nova York: Dover Publications Inc.. ISBN 978-0-486-63462-3.
• (1934).Mathematische Zeitschrift.39 (2)

176–210.doi:10.1007/bf01201353.

• (1935).Mathematische Zeitschrift.39 (3)

405–431.doi:10.1007/bf01201363.

• (1939) Grundlagen der Mathematik II, Segona edició, Berlin, Nova York: Springer-Verlag. ISBN 978-3-642-86897-9.
• (2004) Logic in Computer Science, Segona edició, Cambridge, United Kingdom: Cambridge University Press. ISBN 978-0-521-54310-1.
• (1952) Introduction to metamathematics, Ishi Press International. ISBN 978-0-923891-57-2.
• (1967) Mathematical logic, Mineola, Nova York: Dover Publications. ISBN 978-0-486-42533-7.
• (1965) Beginning logic, Thomas Nelson. ISBN 0-17-712040-1.
• (1965) Natural deduction: A proof-theoretical study, Mineola, Nova York: Dover Publications. ISBN 978-0-486-44655-4.
• (1968) First-order logic, Nova York: Dover Publications. ISBN 978-0-486-68370-6.
• (1957) Introduction to logic, Mineola, Nova York: Dover Publications. ISBN 978-0-486-40687-9.
• (1975) Proof theory, Segona edició, Mineola, Nova York: Dover Publications. ISBN 978-0-486-49073-1.

• Plantilla:Springer