b'\n_START_ARTICLE_\nTeorema de Fagin\n_START_PARAGRAPH_\nTeorema de Fagin\xc2\xa0\xc3\xa9 um resultado da\xc2\xa0teoria da complexidade\xc2\xa0descritiva, que afirma que o conjunto de todas as propriedades que podem ser expressas na l\xc3\xb3gica de segunda ordem\xc2\xa0existencial, \xc3\xa9 precisamente a classe de complexidade NP. \xc3\x89 not\xc3\xa1vel, pois \xc3\xa9 uma caracteriza\xc3\xa7\xc3\xa3o da classe NP que n\xc3\xa3o invoca um modelo de computa\xc3\xa7\xc3\xa3o, tal como uma m\xc3\xa1quina de Turing._NEWLINE_Foi provado por Ronald Fagin em 1973, em sua tese de doutorado. A aridade exigida pela f\xc3\xb3rmula de segunda ordem foi melhorada (em uma dire\xc3\xa7\xc3\xa3o) no teorema de \xc2\xa0Lynch,\xc2\xa0e v\xc3\xa1rios resultados de Grandjean\xc2\xa0forneceram limitantes mais pr\xc3\xb3ximos em m\xc3\xa1quinas de acesso aleat\xc3\xb3rio n\xc3\xa3o determin\xc3\xadsticas .\n_START_SECTION_\nProva\n_START_PARAGRAPH_\nImmerman em 1999, fornece uma prova detalhada do teorema. \xc3\x89 simples, para mostrar que toda f\xc3\xb3rmula existencial de segunda ordem pode ser reconhecida em NP, escolhendo n\xc3\xa3o deterministicamente o valor de todas as vari\xc3\xa1veis\xc2\xa0existencialmente qualificadas, de modo que a parte principal da prova \xc3\xa9 mostrar que cada linguagem em NP pode ser descrita por uma f\xc3\xb3rmula existencial de segunda ordem. Para fazer isso, pode-se usar de quantificadores existenciais de segunda ordem para escolher arbitrariamente uma tableau de computa\xc3\xa7\xc3\xa3o. Em mais detalhe, para cada itera\xc3\xa7\xc3\xa3o de uma hist\xc3\xb3ria de execu\xc3\xa7\xc3\xa3o de uma m\xc3\xa1quina de Turing n\xc3\xa3o determin\xc3\xadstica, este tableau codifica o estado da m\xc3\xa1quina de Turing, a sua posi\xc3\xa7\xc3\xa3o na fita, o conte\xc3\xbado de cada c\xc3\xa9lula da fita, e cuja escolha n\xc3\xa3o determin\xc3\xadstica a m\xc3\xa1quina faz nessa etapa. Restringindo esta informa\xc3\xa7\xc3\xa3o codificada de forma que ela descreve uma hist\xc3\xb3ria de execu\xc3\xa7\xc3\xa3o v\xc3\xa1lida em que o conte\xc3\xbado da fita e o estado\xc2\xa0da m\xc3\xa1quina de Turing \xc2\xa0e sua posi\xc3\xa7\xc3\xa3o em cada itera\xc3\xa7\xc3\xa3o da itera\xc3\xa7\xc3\xa3o anterior pode ser feita com uma f\xc3\xb3rmula de primeira ordem. _NEWLINE_Um lema chave utilizado na prova disso \xc3\xa9 que \xc3\xa9 poss\xc3\xadvel codificar uma ordem linear de comprimento n\xe1\xb5\x8f (tais como as ordens\xc2\xa0lineares de itera\xc3\xa7\xc3\xb5es e conte\xc3\xbado da fita, a qualquer tempo) como uma rela\xc3\xa7\xc3\xa3o 2k-\xc3\xa1ria\xc2\xa0R em um universo A\xc2\xa0de tamanho n. Uma forma de conseguir isto, \xc3\xa9 escolher uma ordena\xc3\xa7\xc3\xa3o linear L de A\xc2\xa0e, em seguida, definir \xc2\xa0R\xc2\xa0 para ser a ordena\xc3\xa7\xc3\xa3o lexicogr\xc3\xa1fica de k-tuplas de A\xc2\xa0com rela\xc3\xa7\xc3\xa3o a L.'