Sistema formal: diferenças entre revisões
Conteúdo apagado Conteúdo adicionado
m r2.7.3) (Robô: A adicionar: ky:Аксиоматикалык метод |
|||
Linha 1:
Um '' sistema formal '' é, por assim dizer, qualquer [[abstração|sistema de pensamento abstrato]] [[bem definido]], em um modelo [[matemática|matemático]]. Tecnicamente, [[Os Elementos| Os Elementos de Euclides]], com um modelo consistindo de 23 definições e 10 postulados/axiomas publicados em 13 livros de teoremas com provas, é frequentimente 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 distinque o sitema formal de outros que podem ter alguma base em uma 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 matematica moderna, como a [[teoria dos modelos]].
== Visão Geral ==
Cada sistema formal tem uma [[linguagem formal]], que é composta por [[lógica simbólica|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 [[axioma|axiomas]]. O sistema, por tanto, consiste em um número de fómulas construídas através de finitas combinações dos simbolos primitivos - combinações, estas, formadas a partir de axiomas em concordância com as regras estabelecidas.<ref>Encyclopædia Britannica, [http://www.britannica.com/eb/article-9034889/formal-system Formal system] definition, 2007.</ref>
sistemas formais, em matemática, consite nos seguintes elementos:
# um conjunto finito de símbolos (i.e. o [[Alfabeto_(ciência_da_computação)| alfabeto]]), que pode ser usado para a construção de fórmulas (i.e. finitas cadeias de símbolos);
# a [[gramática]], que nos mostra como [[fórmula bem formada| 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;
# um conjunto de axiomas: cada axioma deve ser fbf;
# um conjunto de regras de inferência.
O sistema formal é dito como sendo [[Conjunto recursivo|recursivo]] se os conjunto de axiomas e o conjunto de regras de inferência são [[Conjunto recursivo|conjunto decidíveis]] ou [[Conjunto recursivo|conjunto semidecidíveis]], dependento do contexto.
Algus 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 particula 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 (lógica)|interpretação]] de um [[Teoria dos modelos|modelo teórico]], que atribui [[valor de verdade| valor veridativo]] às [[sentença]]s da linguagem formal, isso é, formulas que não contêm [[Variáveis livres e ligadas|variáveis livres]]. A lógica é [[Correção|correta]] se todas as sentenças que possam ser derivadas de sua interpretação são verdadeiras, e [[Completude (lógica)|completas]] se, reciprocamente, todas as sentencas verdadeiras possam ser derivadas.
=== Prova Formal ===
{{Main|Teoria da Prova}}
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 inferencia apalicadas 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 um disciplina para a discussão de sistemas formais. Qualquer linguagem que qualqeur um use para falar sobre o sistema formal é chamado de ''[[metalinguagem]]'. A metalinguagem pode não ser nada mais que uma linguagem natural comum, ou pode ser parcialmente fomarlizada, 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 pode ser provados dentro do sistema formal. Esse conjunto consiste de todas as fbfs que existe um prova. Assim, todos os axiomas são considerados teoremas. Ao contrário da gramática para fbfs, nao existe garantia que existirá um [[Decidibilidade| procedimento para decidir]] quando um fbf dada é um teorema ou não. Essa noção de ''teorema'' não deve ser confundida com '' temoras sobre o sistema formal'', que, para evitar confusão, são normalmente chamadas de [[metateoremas]].
=== Linguagem Formal ===
{{Main|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ântica]]s 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 ===
{{Main|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 de caracteres| 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 formal|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.
== See also ==
{{col-begin}}
{{col-3}}
;Examples of formal systems
* [[Sistema axiomático]]
* [[Ética formal]]
* [[Cálculo Lambda]]
{{col-3}}
;Other related topics
* [[Axioma]]
* [[Gramática Formal]]
* [[Linguagem Formal]]
* [[Métodos Formais]]
* [[Ciências Formais]]
* [[Teoremas da incompletude de Gödel]]
* [[QED manifesto]]
{{col-3}}
{{Portal|Lógica}}
{{col-end}}
== Referências ==
{{reflist}}
== Leitura Adicional ==
* Raymond M. Smullyan, 1961. ''Theory of Formal Systems: Annals of Mathematics Studies'', Princeton University Press (April 1, 1961) 156 pages ISBN 0-691-08047-X
* S. C. Kleene, 1967. ''Mathematical Logic'' Reprinted by Dover, 2002. ISBN 0-486-42533-9
* [[Douglas Hofstadter]], 1979,. ''[[Gödel, Escher, Bach: An Eternal Golden Braid]]'' ISBN 978-0-465-02656-2. 777 pages.
== Links Externos ==
{{Wiktionary|formalisation}}
* Encyclopædia Britannica, [http://www.britannica.com/eb/article-9034889/formal-system Formal system] definition, 2007.
* Christer Blomqvist, [http://hemsidor.torget.se/users/m/mauritz/math/logic/inform.htm an introduction to formal systems], webpage 1997.
* [http://www.cs.indiana.edu/~port/teach/641/formal.sys.haug.html What is a Formal System?]: Some quotes from John Haugeland's `Artificial Intelligence: The Very Idea' (1985), pp. 48–64.
* Heinrich Herre [http://www-ls.informatik.uni-tuebingen.de/psh/forschung/publikationen/RoutledgeFLS1995.pdf Formal Language and systems], 1997.
* Peter Suber, [http://www.earlham.edu/~peters/courses/logsys/machines.htm Formal Systems and Machines: An Isomorphism], 1997.
{{Lógica}}
{{Sistemas}}
{{Portal3|Matemática}}
| |||