Sistema Frege - Frege system

Na complexidade da prova , um sistema de Frege é um sistema de prova proposicional cujas provas são sequências de fórmulas derivadas usando um conjunto finito de regras de inferência sólidas e implicacionalmente completas . Os sistemas de Frege (mais frequentemente conhecidos como sistemas de Hilbert na teoria da prova geral ) são nomeados após Gottlob Frege .

Definição formal

Seja K um conjunto funcionalmente completo finito de conectivos Booleanos e considere fórmulas proposicionais construídas a partir das variáveis p ₀ , p ₁ , p ₂ , ... usando K- conectivos. Uma regra de Frege é uma regra de inferência do formulário

${\ displaystyle r = {\ frac {B_ {1}, \ dots, B_ {n}} {B}},}$

onde B ₁ , ..., B _n , B são fórmulas. Se R é um conjunto finito de regras de Frege, então F = ( K , R ) define um sistema de derivação da seguinte maneira. Se X é um conjunto de fórmulas e A é uma fórmula, então uma derivação F de A dos axiomas X é uma sequência de fórmulas A ₁ , ..., A _m tal que A _m  =  A , e todo A _k é um membro de X , ou é derivada de algumas das fórmulas um _i , i  <  k , por uma substituição exemplo de uma regra de R . Uma prova F de uma fórmula A é uma derivação F de A a partir do conjunto vazio de axiomas (X = ∅). F é chamado de sistema Frege se

• F é boa: toda fórmula F provada é uma tautologia.
• F é implicationally completa: para cada fórmula A e um conjunto de fórmulas X , se X implica um , então não é um F -derivation de um de X .

O comprimento (número de linhas) em uma prova A ₁ , ..., A _m é m . O tamanho da prova é o número total de símbolos.

Um sistema de derivação F como acima é refutationally completa, se para cada conjunto inconsistente de fórmulas X , há uma F -derivation de uma contradição fixo de X .

Exemplos

• O cálculo proposicional de Frege é um sistema de Frege.
• Existem muitos exemplos de regras sólidas de Frege na página de cálculo proposicional .
• A resolução não é um sistema de Frege porque opera apenas em cláusulas , não em fórmulas construídas de forma arbitrária por um conjunto funcionalmente completo de conectivos. Além disso, não é implicacionalmente completo, ou seja, não podemos concluir a partir de . No entanto, adicionar a regra de enfraquecimento : torna-o implicacionalmente completo. A resolução também é refutacionalmente completa. ${\ displaystyle A \ lor B}$${\ displaystyle A}$${\ displaystyle {\ frac {A} {A \ lor B}}}$

Propriedades

• O teorema de Reckhow (1979) afirma que todos os sistemas de Frege são p-equivalentes .
• A dedução natural e o cálculo sequencial (sistema de Gentzen com corte) também são p-equivalentes aos sistemas de Frege.
• Existem provas de Frege de tamanho polinomial do princípio do escaninho (Buss 1987).
• Os sistemas Frege são considerados sistemas bastante fortes. Ao contrário, digamos, da resolução, não há limites inferiores superlineares conhecidos no número de linhas nas provas de Frege, e os limites inferiores mais conhecidos no tamanho das provas são quadráticos.
• O número mínimo de rodadas no jogo provador-adversário necessárias para provar uma tautologia é proporcional ao logaritmo do número mínimo de etapas em uma prova de Frege . ${\ displaystyle \ phi}$${\ displaystyle \ phi}$

• 

  Pontos fortes de prova de diferentes sistemas.

Sistema Extended Frege

Uma extensão importante de um sistema de Frege, o chamado Extended Frege , é definido tomando um sistema de Frege F e adicionando uma regra de derivação extra que permite derivar a fórmula , onde abrevia sua definição na linguagem do F particular e o átomo não ocorrem em fórmulas derivadas anteriormente, incluindo axiomas e na fórmula . ${\ displaystyle p \ leftrightarrow D}$${\ displaystyle \ leftrightarrow}$${\ displaystyle p}$${\ displaystyle D}$

O objetivo da nova regra de derivação é introduzir 'nomes' ou atalhos para fórmulas arbitrárias. Permite interpretar provas em Extended Frege como provas de Frege operando com circuitos em vez de fórmulas.

A correspondência de Cook permite interpretar Extended Frege como um equivalente não uniforme da teoria PV de Cook e da teoria de Buss que formaliza o raciocínio viável (tempo polinomial). ${\ displaystyle S_ {2} ^ {1}}$

Referências

• Krajíček, Jan (1995). "Bounded Arithmetic, Propositional Logic, and Complexity Theory", Cambridge University Press.
• Cook, Stephen ; Reckhow, Robert A. (1979). "A eficiência relativa dos sistemas de provas proposicionais". Journal of Symbolic Logic . 44 (1): 36–50. doi : 10.2307 / 2273702 . JSTOR   2273702 . CS1 maint: parâmetro desencorajado ( link )
• Buss, SR (1987). "Provas de tamanho polinomial do princípio de escaninho proposicional", Journal of Symbolic Logic 52, pp. 916-927.
• Pudlák, P., Buss, SR (1995). "Como mentir sem ser (facilmente) condenado e os comprimentos das provas no cálculo proposicional", em: Computer Science Logic'94 (Pacholski e Tiuryn ​​eds.), Springer LNCS 933, 1995, pp. 151-162.