Modus ponens

O modus ponens, ou de separación, é unha figura de razoamento lóxico relativa á implicación . Consiste en afirmar unha implicación ("se A entón B ") e despois poñer o antecedente ("ou A ") para deducir o consecuente ("entón B ").

Modus ponens
Instancia de regra de inferencia
Subclase de regra do corte
Parte de lóxica clásica lóxica intuicionista lóxica mínima
[ Wikidata ]

O termo modus ponens é unha abreviatura do latín modus ponendo ponens, que significa "o modo que, ao afirmar, afirma". Provén do feito de que ao afirmar A, afírmase B (ponendo é o xerundio do verbo ponere, que significa afirmar, e ponens é o participio presente).

O siloxismo é unha forma de aplicación do modus ponens .

Formalización

A regra do modus ponens ou separación é unha regra primitiva do razoamento. Está escrita formalmente (dependendo do contexto):

${\displaystyle A,\ A\Rightarrow B\vdash B}$ ou

${\displaystyle \left({\begin{array}{c}A\rightarrow B\\A\\\hline B\end{array}}\right)}$

e podémola ler: "de A e de A ⇒ B deducimos B " ou "A e A ⇒ B, polo tanto B"; é dicir, que afirmamos A e A ⇒ B, e deducimos que podemos afirmar B.

Aínda que o conector de implicación (representado normalmente como "⇒" ou "→") e a relación de dedución (notada como “⊢”) están estreitamente relacionados, pertencen a ámbitos distintos e non deben identificarse. Esta diferenza é fundamental para poder formalizar o razoamento de maneira rigorosa. Por exemplo, a tautoloxía proposicional [A ∧ (A ⇒ B)] ⇒ B non constitúe unha regra de inferencia, polo que non pode considerarse unha formulación do modus ponens para o conectivo "⇒". Neste contexto, o modus ponens interprétase como a regra que permite aplicar unha implicación no curso dunha demostración.

Os asistentes de demostración adoitan incluír nas súas bibliotecas unha formulación do modus ponens como regra de inferencia. Por exemplo, no contexto da metamatemática:

min $e ⊢ φ
maj $e ⊢ ( φ → ψ )
ax-mp $a ⊢ ψ

Exemplos

A seguinte frase constitúe un modus ponens: "Se x é un número cuxa suma de díxitos é divisible por 3, entón x é divisible por 3. A suma dos díxitos de 31782 é divisible por 3. Polo tanto, 31782 é divisible por 3".

Estilo de Hilbert

Nos sistemas de dedución ao estilo de Hilbert, o modus ponens é, a miúdo —aínda que non necesariamente— a única regra de inferencia explícita para o cálculo propo­sicional. Isto débese a que as regras correspondentes a outros conectores lóxicos poden expresarse mediante axiomas adecuados combinados co modus ponens.

Por exemplo, a regra que permite deducir A a partir de A ∧ B deriva do modus ponens aplicado ao axioma (A ∧ B) ⇒ A.

Así mesmo, é o modus ponens o que permite establecer principios como o da explosión o razoamento polo absurdo na lóxica clásica.

Esta regra é esencial nos sistemas de Hilbert: tal redución non é posible para o propio modus ponens, para deducilo por exemplo de [ A ∧ ( A ⇒ B )] ⇒ B, serían necesarios outros axiomas... e varias aplicacións do propio modus ponens .

Dedución natural

Unha forma de modus ponens atópase nos sistemas de dedución natural co nome de regra de eliminación da implicación, onde necesariamente ten unha forma máis xeral, no sentido de que cómpre usala en presenza de hipóteses adicionais. Esta xeneralización non é necesaria nos sistemas de Hilbert, nos que a regra simétrica de introdución, "de A ⊢ B deducimos A ⇒ B ", é unha regra derivada, coñecida como teorema da dedución, que se demostra de novo a partir da regra do modus ponens e dos axiomas axeitados, pero dun xeito máis complexo, usando unha recorrencia na lonxitude da dedución (polo tanto, a tradución depende da dedución).

Cálculo de secuentes

O cálculo de secuentes, como a dedución natural, débese a Gerhard Gentzen e non ten unha regra de modus ponens directa. Isto pódese derivar da regra de corte, que é un modus ponens a nivel de dedución (esencialmente, cando temos ⊢ A e A ⊢ B temos ⊢ B, e estas deducións fanse nun determinado contexto) e da regra da implicación esquerda, que nos permite demostrar o secuente A, A ⇒ B ⊢ B. Gentzen demostrou que a regra de corte podía eliminarse no cálculo de secuencias para o cálculo de predicados puro (sen igualdade e fóra do marco dunha teoría axiomática) e que, neste marco, a demostración dunha fórmula só podía usar subfórmulas dela. Isto non é posible nun sistema de Hilbert, onde, en canto se usa o modus ponens, introdúcese unha fórmula máis complexa que a fórmula que se vai demostrar.

Na dedución natural, a propiedade de normalización, que corresponde á eliminación de cortes no cálculo de secuentes, mostra que é posible (aínda no cálculo de predicados puro) restrinxir o uso do modus ponens ás subfórmulas da fórmula que se vai demostrar.

A propiedade da subfórmula para estes dous sistemas (dedución natural e cálculo de secuencias) ten como contrapartida a introdución dun nivel adicional, o das secuencias, onde a dedución de sistemas ao estilo de Hilbert só trata con fórmulas.

Véxase tamén

Bibliografía

• René Cori e Daniel Lascar, Logique mathématique I. Calcul propositionnel, algèbres de Boole, calcul des prédicats. Editorial: Masson (colección Axiomes), 1993, ISBN: 2‑225‑84079‑2

Outros artigos

• Razoamento
• Regra de inferencia
• Siloxismo