Lógica de segunda ordem monádica

Na lógica, o calculo monádico de predicados (também referido como lógica de primeira ordem monádica) é um fragmento da lógica de primeira ordem na qual, todos os simbolos de relações da assinatura são monádicas (isso é, só podem receber um argumento), e não existem símbolos de funções. Todas Fórmula atômicas são da forma $P(x)$, onde $P$ é um símbolo de relação e $x$ é uma variável.

Calculo monádico de predicados pode ser contrastado com o calculo poliádico de predicados, que possibilita símbolos relacionais que aceitam dois ou mais argumentos.

Expressividade

A ausência de símbolos relacionais poliádicos restringe severamente o que pode ser expresso no calculo monádico de predicados. Isso é tão fraco que, diferentemente do calculo de predicado completo, isso é decidível – existe um procedimento de decisão que determine quando uma fórmula arbitrária de calculo monádico de predicados é logicamente válida (verdade para todos domínios não vazios). Adicionando um único símbolo de relação binária à lógica monádica, entretanto, resulta em uma lógica indefinível.

Relação com a lógica de termos

A necessidade de ir além da lógica monádica não foi apreciada até o trabalho da lógica de relações, por Augustus De Morgan e Charles Sanders Peirce no século XIX, e por Frege em Begriffsschrifft de 1879. Por conta do trabalho desses três homens, Lógica (lógica simbólica) foi considerada adequada para lógica dedutiva formal.

Inferências na lógica de termos podem ser representadas no calculo monádico de predicados. Por exemplo o silogismo

Todos cães são mamíferos.

Nenhum mamífero é um pássaro.

Então, nenhum cão é pássaro.

pode ser transcrito para a linguagem do calculo monádico de predicados como

$(\forall x\,D(x)\Rightarrow M(x))\land \neg (\exists y\,M(y)\land B(y))\Rightarrow \neg (\exists z\,D(z)\land B(z))$

onde $D$, $M$ e $B$ denotam os predicados de serem, respectivamente, um cão, um mamífero, e um pássaro.

Entretanto, calculo monádico de predicados não é significantemente mais expressivo que a lógica de termos. Cada fórmula no calculo monádico de predicados é equivalente a uma formula na qual quantificadors aparece apenas uma vez em subformulas fechadas da forma

$\exists x\,\neg P_{1}(x)\land \cdots \land \neg P_{n}(x)\land P'_{1}(x)\land \cdots \land P'_{m}(x),$

ou

$\exists x\,\neg P_{1}(x)\land \cdots \land \neg P_{n}(x)\land P'_{1}(x)\land \cdots \land P'_{m}(x),$

Estas fórmulas generalizam levemente os julgamentos básicos considerados na lógica de termos. Por exemplo, esta forma permite afirmações como "Todo mamífero é um herbívoro ou um carnívoro (ou ambos)", $(\forall x\,\neg M(x)\lor H(x)\lor C(x))$. Pensando sobre essas afirmações pode, entretanto, ainda ser manipulada dentro da estrutura da lógica de termos, porém não pelos 19 clássicos silogismos Aristotelicos apenas.

Tomando lógica proposicional como é dada, toda fórmula no calculo monádico de predicado expressa algo que pode também ser formulada na lógica de termos. Todavia, uma visão moderna do problema de multiplas generalizações na lógica tradicional conclui que quantificadores não podem ser aninhados de forma útil se não houverem predicados poliádicos para relacionar as variáveis conectadas.

Variantes

O sistema formalmente descrito acima é algumas vezes chamado de puro calculo monádico de predicados, onde "puro" significa a ausência de funções de letras. Permitindo as letras de funções monádicas mudar a lógica apenas superficialmente, mesmo que adimitindo apenas uma única função binária de letra resulta em uma lógica indecidível.

Monádico lógica de segunda ordem permite predicados de aridade mais alta em fórmulas, mas restringe quantificações de segunda ordem para predicados unários, i.e. as únicas variáveis de segunda ordem permitidas são variáveis de subconjuntos.