Lógica e metalógica
Em certo sentido, a lógica deve ser identificada com o cálculo predicado de primeira ordem, o cálculo no qual as variáveis estão confinadas a indivíduos de um domínio fixo - embora possa incluir também a lógica da identidade, simbolizada como "=", que toma as propriedades comuns da identidade como parte da lógica. Nesse sentido, Gottlob Frege alcançou um cálculo formal da lógica já em 1879. Contudo, às vezes a lógica é interpretada como incluindo também cálculos de predicados de ordem superior, que admitem variáveis de tipos mais altos, como aquelas que ultrapassam predicados (ou classes e relações).) e assim por diante. Mas, então, é um pequeno passo para a inclusão da teoria dos conjuntos e, de fato, a teoria axiomática dos conjuntos é frequentemente vista como parte da lógica. Para os fins deste artigo, no entanto, é mais apropriado limitar a discussão à lógica no primeiro sentido.
É difícil separar descobertas significativas na lógica daquelas na metalógica, porque todos os teoremas de interesse dos lógicos são sobre lógica e, portanto, pertencem à metalógica. Se p é um teorema matemático - em particular, um sobre lógica - e P é a conjunção dos axiomas matemáticos empregados para provar p, então todo p pode ser transformado em um teorema, “não-P ou p”, na lógica. A matemática não é feita, no entanto, executando explicitamente todos os passos formalizados na lógica; a seleção e a compreensão intuitiva dos axiomas são importantes tanto para a matemática quanto para a metamatemática. Derivações reais na lógica, como as realizadas imediatamente antes da Primeira Guerra Mundial por Alfred North Whitehead e Bertrand Russell, são de pouco interesse intrínseco para os lógicos. Portanto, pode parecer redundante introduzir o termo metalógico. Na presente classificação, no entanto, metalogic é concebido como lidando não apenas com descobertas sobre cálculos lógicos, mas também com estudos de sistemas formais e linguagens formais em geral.
Um sistema formal comum difere de um cálculo lógico, pois o sistema geralmente tem uma interpretação pretendida, enquanto o cálculo lógico deixa deliberadamente em aberto as possíveis interpretações. Assim, fala-se, por exemplo, da verdade ou falsidade de sentenças em um sistema formal, mas com relação a um cálculo lógico fala-se de validade (isto é, sendo verdadeira em todas as interpretações ou em todos os mundos possíveis) e de satisfação (ou ter um modelo - isto é, ser verdadeiro em alguma interpretação em particular). Portanto, a completude de um cálculo lógico tem um significado bastante diferente do de um sistema formal: um cálculo lógico permite muitas sentenças de modo que nem a sentença nem sua negação sejam um teorema, porque é verdade em algumas interpretações e falso em outras, e requer apenas que toda sentença válida seja um teorema.
