Sistema formal

Esta página cita fontes, mas que não cobrem todo o conteúdo. Ajude a inserir referências. Conteúdo não verificável pode ser removido.—Encontre fontes: ABW  • CAPES  • Google (N • L • A) (Julho de 2012)

Um sistema formal ou sistema lógico é, por assim dizer, qualquer sistema de pensamento abstrato bem definido, em um modelo matemático. Tecnicamente, Os Elementos de Euclides, com um modelo consistindo de 23 definições e 10 postulados/axiomas publicados em 13 livros de teoremas com provas, é frequentemente considerado o primeiro sistema formal e mostra as características de um sistema formal. A implicação de um sistema por sua base lógica é o que distingue o sistema formal de outros que podem ter alguma base em um modelo abstrato. Muitas vezes, o sistema formal será a base, ou será identificado por si só, como uma teoria maior ou um campo consistente com o uso da matemática moderna, como a teoria dos modelos.

Visão geral

Cada sistema formal tem uma linguagem formal, que é composta por símbolos primitivos. Esse símbolos agem em um certa regra de formação e são desenvolvidos por inferência a partir de um conjunto de axiomas. O sistema, por tanto, consiste em um número de fórmulas construídas através de finitas combinações dos símbolos primitivos - combinações, estas, formadas a partir de axiomas em concordância com as regras estabelecidas.

Sistemas formais, em matemática, consiste nos seguintes elementos:

1. um conjunto finito de símbolos (i.e. o alfabeto), que pode ser usado para a construção de fórmulas (i.e. finitas cadeias de símbolos);
2. a gramática, que nos mostra como fórmulas bem formadas, abreviando fbf, são construídas pelos símbolos do alfabeto. Normalmente, é necessário que exista um procedimento para identificar se a fórmula está bem formada ou não;
3. um conjunto de axiomas: cada axioma deve ser fbf;
4. um conjunto de regras de inferência.

O sistema formal é dito como sendo recursivo se os conjunto de axiomas e o conjunto de regras de inferência são conjunto decidíveis ou conjunto semidecidíveis, dependendo do contexto.

Alguns teóricos usam o de maneira grosseira o termo formalismo como sinônimo para sistema formal, mas esse termo é também usado para se referir a um estilo particular de notação, por exemplo, a Notação Bra-ket de Paul Dirac.

Assuntos relacionados

Sistema lógico

O sistema lógico ou, simplesmente, lógica é o sistema formal junto com a semântica, geralmente na forma de interpretação de um modelo teórico, que atribui valor veridativo às sentenças da linguagem formal, isso é, formulas que não contêm variáveis livres. A lógica é correta se todas as sentenças que possam ser derivadas de sua interpretação são verdadeiras, e completas se, reciprocamente, todas as sentenças verdadeiras possam ser derivadas.

Prova formal

Provas formais são as sequencias de fbf's. Para uma fbf ser qualificada com parte da prova, ela pode ser tanto um axioma quanto o produto das regras de inferência aplicadas em fbfs anteriores na sequencia de provas. A última fbf na sequência de provas é reconhecida como um teorema.

O ponto de vista de que a geração de provas formais é tudo que existe para a matemática é, frequentemente, chamado de formalismo. David Hilbert fundou a metamatemática como uma disciplina para a discussão de sistemas formais. Qualquer linguagem que seja usada para falar sobre o sistema formal é chamada de metalinguagem'. A metalinguagem pode não ser nada mais que uma linguagem natural comum, ou pode ser parcialmente formalizada, porém, é geralmente menos do que o componente da linguagem formal do sistema formal ao qual está sendo examinado, que é então chamado de Linguagem objeto, isto é, objeto que está em questão na discussão.

Uma vez dado um sistema formal, pode se definir o conjunto de teoremas que podem ser provados dentro do sistema formal. Esse conjunto consiste de todas as fbfs para as quais existe uma prova. Assim, todos os axiomas são considerados teoremas. Ao contrário da gramática para fbfs, não existe garantia que existirá um procedimento para decidir quando uma fbf dada é um teorema ou não. Essa noção de teorema não deve ser confundida com teoremas sobre o sistema formal, que, para evitar confusão, são normalmente chamados de metateoremas.

Linguagem formal

Na matemática, na lógica, e na ciência da computação, a linguagem formal é a linguagem que é definida por modelos matemáticos ou máquinas de processamento de fórmulas. Como línguas em linguística, a linguagem formal possui dois aspectos:

• a sintaxe de uma linguagem é o que a linguagem aparenta (mais formalmente: o conjunto de possíveis expressões que são declarações válidas na linguagem);
• as semânticas da linguagem são o que as declarações de linguagem significam (que são formalizadas de várias maneiras, dependendo do tipo de linguagem em questão).

Existe um ramo especial da matemática e da ciência da computação que é dedicado exclusivamente à teoria da sintaxe da linguagem:[[linguagem formal| Teoria da Linguagem Formal. Na teoria da linguagem formal, a língua é nada mais que sua própria sintaxe; questões de semântica não são incluídas nessa especialidade.

Gramática formal

Em ciência da computação e em linguística gramática formal é uma descrição precisa de uma linguagem formal: um conjunto de cadeias. As duas principais categorias da gramática formal são: a gramática gerativa, que é conjunto de regras de como cadeias podem ser geradas em uma linguagem, e a gramática analítica, que é conjunto de regras de como cadeias podem ser analisadas para determinar se pertencem à linguagem. Em resumo, a gramática analítica descreve como reconhecer quando cadeias são membros de um conjunto, ao passo que a gramática gerativa descreve somente como escrever essas cadeiras no conjunto.

Ver também