Sistema formal - Formal system

Um sistema formal é uma estrutura abstrata usada para inferir teoremas de axiomas de acordo com um conjunto de regras. Essas regras, que são usadas para realizar a inferência de teoremas de axiomas, são o cálculo lógico do sistema formal. Um sistema formal é essencialmente um " sistema axiomático ".

Em 1921, David Hilbert propôs usar tal sistema como base para o conhecimento em matemática . Um sistema formal pode representar um sistema bem definido de pensamento abstrato .

O termo formalismo às vezes é sinônimo áspera para sistema formal , mas também se refere a um determinado estilo de notação , por exemplo, Paul Dirac 's notação bra-ket .

Fundo

Cada sistema formal usa símbolos primitivos (que coletivamente formam um alfabeto ) para construir finitamente uma linguagem formal a partir de um conjunto de axiomas por meio de regras inferenciais de formação .

O sistema, portanto, consiste em fórmulas válidas construídas por meio de combinações finitas dos símbolos primitivos - combinações que são formadas a partir dos axiomas de acordo com as regras estabelecidas.

Mais formalmente, isso pode ser expresso da seguinte forma:

  1. Um conjunto finito de símbolos, conhecido como alfabeto, que concatenam fórmulas, de forma que uma fórmula é apenas uma sequência finita de símbolos tirados do alfabeto.
  2. Uma gramática que consiste em regras para formular fórmulas a partir de fórmulas mais simples. Uma fórmula é considerada bem formada se puder ser formada usando as regras da gramática formal. Freqüentemente, é necessário que haja um procedimento de decisão para decidir se uma fórmula está bem formada.
  3. Um conjunto de axiomas, ou esquemas de axioma , que consiste em fórmulas bem formadas.
  4. Um conjunto de regras de inferência . Uma fórmula bem formada que pode ser inferida dos axiomas é conhecida como teorema do sistema formal.

Recursiva

Um sistema formal é considerado recursivo (isto é, eficaz) ou recursivamente enumerável se o conjunto de axiomas e o conjunto de regras de inferência são conjuntos decidíveis ou conjuntos semidecidíveis , respectivamente.

Inferência e vinculação

A vinculação do sistema por seu fundamento lógico é o que distingue um sistema formal de outros que podem ter alguma base em um modelo abstrato. Freqüentemente, o sistema formal será a base ou mesmo identificado com uma teoria ou campo mais amplo (por exemplo, geometria euclidiana ) consistente com o uso na matemática moderna, como a teoria dos modelos .

Linguagem formal

Uma linguagem formal é aquela definida por um sistema formal. Como as linguagens na linguística , as linguagens formais geralmente têm dois aspectos:

  • a sintaxe de uma linguagem é a aparência da linguagem (mais formalmente: o conjunto de expressões possíveis que são enunciados válidos na linguagem) estudada na teoria da linguagem formal
  • a semântica de uma linguagem é o que os enunciados da linguagem significam (o que é formalizado de várias maneiras, dependendo do tipo de linguagem em questão)

Em ciência da computação e linguística geralmente apenas a sintaxe de uma linguagem formal é considerada por meio da noção de uma gramática formal . Uma gramática formal é uma descrição precisa da sintaxe de uma linguagem formal: um conjunto de strings . As duas categorias principais de gramática formal são as gramáticas gerativas , que são conjuntos de regras para como strings em uma linguagem podem ser geradas, e as de gramáticas analíticas (ou gramática redutiva), que são conjuntos de regras de como uma string pode ser analisado para determinar se é um membro do idioma. Em suma, uma gramática analítica descreve como reconhecer quando as strings são membros do conjunto, enquanto uma gramática generativa descreve como escrever apenas essas strings no conjunto.

Na matemática , uma linguagem formal geralmente não é descrita por uma gramática formal, mas por (uma) linguagem natural, como o inglês. Os sistemas lógicos são definidos tanto por um sistema dedutivo quanto por uma linguagem natural. Os sistemas dedutivos, por sua vez, são definidos apenas pela linguagem natural (veja abaixo).

Sistema dedutivo

Um sistema dedutivo , também chamado de aparato dedutivo ou lógica , consiste em axiomas (ou esquemas de axioma ) e regras de inferência que podem ser usadas para derivar teoremas do sistema.

Esses sistemas dedutivos preservam qualidades dedutivas nas fórmulas que são expressas no sistema. Normalmente, a qualidade com a qual nos preocupamos é a verdade, e não a falsidade. No entanto, outras modalidades , como justificação ou crença podem ser preservadas em seu lugar.

Para sustentar sua integridade dedutiva, um aparato dedutivo deve ser definível sem referência a qualquer interpretação pretendida da linguagem. O objetivo é garantir que cada linha de uma derivação seja meramente uma consequência sintática das linhas que a precedem. Não deve haver nenhum elemento de qualquer interpretação da linguagem que se envolva com a natureza dedutiva do sistema.

Um exemplo de sistema dedutivo é a lógica de predicados de primeira ordem .

Sistema lógico

Um sistema lógico ou linguagem (não deve ser confundido com o tipo de "linguagem formal" discutido acima, que é descrito por uma gramática formal), é um sistema dedutivo (ver seção acima; mais comumente lógica de predicado de primeira ordem ) junto com adicional (não lógico) axiomas e uma semântica . De acordo com a interpretação teórica do modelo , a semântica de um sistema lógico descreve se uma fórmula bem formada é satisfeita por uma dada estrutura. Uma estrutura que satisfaça todos os axiomas do sistema formal é conhecida como modelo do sistema lógico. Um sistema lógico é válido se cada fórmula bem formada que pode ser inferida dos axiomas for satisfeita por todos os modelos do sistema lógico. Por outro lado, um sistema lógico está completo se cada fórmula bem formada que é satisfeita por todos os modelos do sistema lógico pode ser inferida dos axiomas.

Um exemplo de sistema lógico é a aritmética de Peano .

História

Os primeiros sistemas lógicos incluem a lógica indiana de Pāṇini , a lógica silogística de Aristóteles, a lógica proposicional do estoicismo e a lógica chinesa de Gongsun Long (c. 325-250 aC). Em tempos mais recentes, contribuíram com George Boole , Augustus De Morgan e Gottlob Frege . A lógica matemática foi desenvolvida na Europa do século XIX .

Formalismo

Programa de Hilbert

David Hilbert instigou um movimento formalista que acabou sendo temperado pelos teoremas da incompletude de Gödel .

Manifesto QED

O manifesto QED representou um esforço subsequente, ainda sem sucesso, na formalização da matemática conhecida.

Exemplos

Exemplos de sistemas formais incluem:

Variantes

Os sistemas a seguir são variações dos sistemas formais.

Sistema de prova

As provas formais são sequências de fórmulas bem formadas (ou wff para abreviar). Para que uma wff se qualifique como parte de uma prova, pode ser um axioma ou ser o produto da aplicação de uma regra de inferência em wffs anteriores na sequência de prova. A última wff na sequência é reconhecida como um teorema .

O ponto de vista de que gerar provas formais é tudo o que existe na matemática é freqüentemente chamado de formalismo . David Hilbert fundou a metamatemática como uma disciplina para discutir sistemas formais. Qualquer linguagem que alguém usa para falar sobre um sistema formal é chamada de metalinguagem . A metalinguagem pode ser uma linguagem natural, ou pode ser parcialmente formalizada em si mesma, mas geralmente é menos completamente formalizada do que o componente de linguagem formal do sistema formal sob exame, que é então chamado de linguagem objeto , isto é, o objeto da discussão em questão.

Uma vez que um sistema formal é dado, pode-se definir o conjunto de teoremas que podem ser provados dentro do sistema formal. Este conjunto consiste em todas as wffs para as quais existe uma prova. Assim, todos os axiomas são considerados teoremas. Ao contrário da gramática para wffs, não há garantia de que haverá um procedimento de decisão para decidir se um dado wff é um teorema ou não. A noção de teorema que acabamos de definir não deve ser confundida com teoremas sobre o sistema formal , que, para evitar confusão, são normalmente chamados de metateoremas .

Veja também

Referências

Leitura adicional

links externos