# Modus ponens

Na lógica proposicional, modus ponendo ponens (em latim significa "a maneira que afirma afirmando", muitas vezes abreviado para MP ou modus ponens) ou a eliminação da implicação é uma válida e simples forma de argumento e regra de inferência. Ele pode ser resumido como "P implica Q, P é afirmado verdade, portanto, Q deve ser verdade." A história do modus ponens nos leva de volta a antiguidade.
Como modus ponens é um dos conceitos mais utilizados na lógica não deve ser confundido com uma lei da lógica, mas sim como um dos mecanismos aceitos para a construção de provas dedutivas, que inclui a "regra de definição" e a "regra de substituição" modus ponens permite eliminar uma instrução condicional de uma prova lógica ou argumento e, assim, não levar esses antecedentes para frente em uma seqüência sempre crescente de símbolos; por essa razão modus ponens é às vezes chamado a regra do desapego. Enderton, por exemplo, observa que "modus ponens pode produzir fórmulas mais curtas de mais longas", e Russell observa que "o processo de inferência não pode ser reduzido a símbolos. Seu único registro é a ocorrência de ⊦ q [consequente] ... uma inferência é o lançamento de uma premissa verdadeira, que é a dissolução de uma implicação".
A justificativa para a "confiança em inferência é acreditar que, se duas afirmações anteriores não estão erradas, a afirmação final [a consequente] não é um erro". Em outras palavras:. Se uma declaração ou proposição implica uma segunda, e a primeira declaração ou proposição é verdadeira, então a segunda também é verdadeira. Se P implica Q e P é verdadeira, então Q é verdadeira. Um exemplo é:
    Se estiver chovendo, eu encontrarei você no cinema.
    Está chovendo.
    Então, encontrarei você no cinema.
Modus ponens pode ser simbolizado formalmente da seguinte forma:
    ${\frac {P\to Q,\;P}{\therefore Q}}$
Onde a regra é que sempre que uma instância de "P → Q" e "P" aparecem em linhas de uma prova lógica, Q pode validamente ser colocado em uma linha subsequente.
Modus ponens está intimamente relacionada com outra forma válida de argumento, modus tollens - ambos têm formas aparentemente semelhantes.

## Notação Formal

A regra Modus ponens pode ser escrita na forma de sequentes, como é mostrado a seguir:
    $P\to Q,\;P\;\;\vdash \;\;Q$
onde ⊦é um símbolo que significa que Q é uma derivação sintática de P → Q e P em algum sistema lógico;
ou representado como a declaração de uma tautologia ou teorema da lógica proposicional:
    $((P\to Q)\land P)\to Q$
Onde P e Q são proposições expressar em um sistema lógico.

## Explicação

O argumento tem duas premissas (hipótese). A primeira premissa é o "if-then" ou afirmação condicional, ou seja, que P implica Q. A segunda premissa é que P, o antecedente do pedido condicional, é verdade. A partir dessas duas premissas pode ser logicamente concluído que Q, consequente da afirmação condicional, deve ser verdade também. Em inteligência artificial, modus ponens é freqüentemente chamado de encadeamento de encaminhamento.
Um exemplo cabe na forma de modus ponens é:
    Se hoje é terça, então João vai ao trabalho.
    Hoje é terça.
    Então, João vai ao trabalho.
Esse argumento é válido, mas isso não tem qualquer influência sobre se alguma das declarações no argumento são verdadeiras, pois para o modus ponens ser um argumento sólido, as sentenças devem ser verdade para qualquer instância verdadeira da conclusão. Um argumento pode ser válido, mas ainda assim instável se uma ou mais premissas são falsas; se um argumento é válido e todas as premissas são verdadeiras, então o argumento é estável. Por exemplo, João pode estar indo para o trabalho na quarta-feira. Neste caso, o raciocínio para João indo para o trabalho (porque é quarta-feira) não é sólido. O argumento não é apenas seguro às terças-feiras (quando João vai para o trabalho), mas válida em todos os dias da semana. Um argumento proposicional utilizando modus ponens é dito ser dedutivo.
Em um cálculo de sequentes com uma única conclusão, modus ponens é a regra de corte. O teorema de corte de eliminação para um cálculo diz que toda prova envolvendo corte pode ser transformado (em geral, através de um método construtivo) em uma prova sem corte, e, portanto o corte é admissível.
O isomorfismo de Curry–Howard entre provas e programas relaciona modus ponens para funcionar na aplicação: se f é uma função do tipo P → Q e x é do tipo P, então f(x) é do tipo Q.

## Relação com Modus Tollens

Qualquer regra Modus Ponens pode ser provada usando uma regra de Modus Tollens e transposição.
    Podemos provar como se segue:
    1. P → Q
    2. P /∴ Q
    3.~Q → ~P 1 Transposição
    4.~~P 2 Negação Dupla
    5.~~Q 3,4 Modus Tollens
    6. 5 Negação Dupla

## Justificativa através da Tabela Verdade

A validade de modus ponens numa lógica clássica de dois valores pode ser claramente demonstrada pelo uso da tabela verdade, como está exposto abaixo:
| p | q | p → q |
| T | T | T |
| T | F | F |
| F | T | T |
| F | F | T |
Nas instancias de modus ponens podemos assumir como premissas que p → q é verdadeiro e p é verdadeiro também. Apenas uma linha da tabela verdade (a primeira) satisfaz essas duas condições (p e p → q). Nessa linha, q também é verdadeiro. Portanto, em qualquer situação em que p → q é verdadeiro, q também deve ser verdadeiro.