Lógica do functor predicado

Em lógica matemática, predicado functor lógica (PFL) é uma das várias maneiras de expressar o que a lógica de primeira ordem (também conhecida como lógica de predicado) puramente algébrica significa, por exemplo, sem variáveis quantificáveis. PFL emprega um pequeno número de corpos finitos, dispositivos de chamada de predicado ficheiro (ou modificadores de predicado) que operam em termos de rendimento termos. PFL é principalmente a invenção do lógico e filosofo Willard Quine.

Motivação

A fonte para esta seção, bem como para grande parte do movimento, é Quine (1976). Quine propôs o PFL como uma forma de algebrizar a lógica de primeira ordem em uma maneira análoga a como álgebra Booleana algebriza a lógica proposicional. Ele projetou o PFL, para ter exatamente o poder expressivo de a lógica de primeira ordem com identidade. Daí a metamatemática do PFL, são exatamente aqueles de lógica de primeira ordem, sem i letras de predicados intepretadas: ambas as lógicas são som, completo, e indecidíveis. A maior parte do trabalho que Quine publicou sobre lógica e matemática nos últimos 30 anos de sua vida tocou no PFL de alguma forma.^{[carece de fontes]}

Quine tomou "functor" a partir dos escritos de seu amigo Rudolf Carnap, o primeiro a empregá-lo em filosofia e lógica matemática, e definiu-o da seguinte maneira:

"A palavra functor, gramatical em importar, mas lógico no habitat... é um sinal de que a atribui a um ou mais expressões de determinado tipo(s) gramatical  para produzir uma expressão de um determinado tipo gramatical." (Quine 1982: 129)

Forma diferentes para PFL algebrizar a lógica de primeira ordem incluem:

• Álgebra Cilíndrica por Alfred Tarski e seus estudantes Americanos. A Álgebra cilíndrica simplifica  proposta em Bernays (1959) levou Quine escrever o documento com o primeiro uso da expressão "predicado functor";
• Álgebra polivalente  de Paul Halmos. Em virtude de sua econômicos primitivos e axiomas, está álgebra se assemelha mais ao PFL;
• A relação algébrica algebraizar o fragmento da a lógica de primeira ordem consiste nas que não tem nenhuma fórmula atômica no âmbito de mais de três quantificadores.  Esse fragmento que é o suficiente, no entanto, para a aritmética de Peano e a axiomática da teoria dos conjuntos ZFC; daí a relação algébrica, ao contrário do PFL, é incompletable. A maior parte do trabalho em relação à álgebra desde cerca de 1920 foi feita por Tarski e seus estudantes Americanos. O poder da relação algébrica não se manifestou até a monografia de Tarski e Givant (1987), publicada depois de três importantes artigos sobre o PFL, nomeadamente Bacon (1985), Kuhn (1983), e Quine (1976);
• Lógica Combinatória baseia na ferramenta, de ordem superior cujo domínio é um outro combinador ou função, e cujo alcance é ainda outro combinator. Daí combinatória lógica ultrapassa a lógica de primeira ordem por ter o poder expressivo da teoria dos conjuntos, o que torna combinatória lógica vulnerável a paradoxos. Um predicado functor, por outro lado, simplesmente mapeia predicados (também denominado termos) em predicados.

PFL é, sem dúvida, o mais simples destes formalismos, mas também é o que menos tem sido escrito.

Quine tinha um fascínio ao longo da vida com a combinatória lógica, atestada por sua (1976) e sua introdução à tradução em Van Heijenoort (1967) do papel pelo lógico, o russo, Moisés Schönfinkel fundando a lógica combinátoria. Quando Quine começou a trabalhar no PFL, a sério, em 1959, a combinatória lógica era comumente considerado um fracasso pelos seguintes motivos:

• Até Dana Scott começou a escrever sobre o modelo de teoria da lógica combinatória no final da década de 1960, quase somente Haskell Curry, seus alunos, e Robert Feys na Bélgica trabalharam nessa lógica;
• As formulações axiomáticas satisfatória da lógica combinatória foram lentas. Na década de 1930, algumas formulações de lógica combinatória foram encontrados para ser inconsistente. Curry também descobriu o paradoxo de Curry, peculiar combinação da lógica;
• O cálculo lambda, com o mesmo poder expressivo que a combinatória lógica, era visto como um superior formalismo.

Kuhn formalização

O PFL sintaxe, primitivos e axiomas descritos nesta seção são em grande parte Kuhn (1983). A semântica dos functores são Quine (1982). O resto desta entrada incorpora algumas terminologia de Bacon (1985).

Sintaxe

Um termo atômico é uma letra latina em letras maiúsculas, I e S exceto, seguido por um superíndice numérico chamado seu grau, ou por variáveis ​​em maiúsculas concatenadas, coletivamente conhecidas como lista de argumentos. O grau de um termo transmite a mesma informação que o número de variáveis ​​seguindo uma letra de predicado. Um termo atômico de grau 0 indica uma variável booleana ou um valor de verdade. O grau de I é invariavelmente 2 e assim não é indicado.

 Os functores predicados "combinatórios" (a palavra é Quine), todos monádicos e peculiares de PFL, são Inv, inv, ∃, + e p. Um termo é um termo atômico, ou construído pela seguinte regra recursiva. Se τ é um termo, então Invτ, invτ, ∃τ, +τ, e pτ são termos. Um funtor com um superíndice n, n um número natural> 1, denota n aplicações consecutivas (iterações) desse functor.

 Uma fórmula é um termo ou definido pela regra recursiva: se α e β são fórmulas, então αβ e ~ (α) são igualmente fórmulas. Portanto, "~" é outro functor monádico, e a concatenação é o único functor predicado diádico. Quine chamou esses functores de "aletico". A interpretação natural de "~" é negação; O de concatenação é qualquer conectivo que, quando combinado com a negação, forma um conjunto funcionalmente completo de conectivos. O conjunto funcional funcionalmente completo de Quine era conjunção e negação. Assim termos concatenados são tomados como unidos. A notação + é de Bacon (1985); Todos os outros notação é Quine's (1976, 1982). A parte aletica de PFL é idêntica aos schemas booleanos do termo de Quine (1982).

Como é bem sabido, os dois funtores altéticos poderiam ser substituídos por um único functor diádico com a seguinte sintaxe e semântica: se α e β são fórmulas, então (αβ) é uma fórmula cuja semântica é "não (α e / ou β) "(Ver NAND e NOR).

Axiomas e semântica

A Quine não estabeleceu nem axiomatização nem procedimento de prova para PFL. A seguinte axiomatização de PFL, uma das duas propostas em Kuhn (1983), é concisa e fácil de descrever, mas faz uso extensivo de variáveis ​​livres e não faz justiça ao espírito de PFL. Kuhn dá outra axiomatização dispensando variáveis ​​livres, mas que é mais difícil de descrever e que faz uso extensivo de functores definidos. Kuhn provou ambas as suas axiomatizações PFL consistência e completo.

Esta seção é construída em torno dos functores predicados primitivos e alguns definidos. Os functores aléticos podem ser axiomatizados por qualquer conjunto de axiomas para lógica sentencial cujos primitivos são negação e um de ∧ ou ∨. Equivalentemente, todas as tautologias da lógica sentencial podem ser tomadas como axiomas.

 A semântica de Quine (1982) para cada functor de predicado é indicada abaixo em termos de abstração (notação de construtor de conjuntos), seguida pelo axioma relevante de Kuhn (1983) ou por uma definição de Quine (1976). A notação {x_1 ... x_n: Fx_1 ... x_n } denota o conjunto de n-tuplas que satisfazem a fórmula atômica Fx_1 ... x_n.

"A palavra functor, gramatical em importar, mas lógico no habitat... é um sinal de que a atribui a um ou mais expressões de determinado tipo(s) gramatical  para produzir uma expressão de um determinado tipo gramatical." (Quine 1982: 129)

Identidade, I, é definida como:

A identidade é reflexiva (Ixx), simétrica (Ixy→Iyx), transitiva ( (Ixy∧Iyz) → Ixz), e obedece a substituição de propriedade:

${\displaystyle }$

• Preenchimento, +, adiciona uma variável à esquerda de qualquer lista de argumento.

${\displaystyle }$

${\displaystyle }$

•  Recortar, ∃, apaga a variável mais à esquerda em qualquer lista de argumentos.

${\displaystyle }$

${\displaystyle }$

O recorte permite que dois functores úteis :

• Reflexão, S:

${\displaystyle }$

${\displaystyle }$

 S generaliza a noção de reflexividade para todos os termos de qualquer grau finito maior que 2. N.B: S não deve ser confundido com o combinador primitivo S da lógica combinatória.

• Produto cartesiano, ${\displaystyle }$;

${\displaystyle }$

 Aqui apenas, Quine adotou uma notação infix, porque esta notação infix para produto cartesiano é muito bem estabelecida na matemática. O produto cartesiano permite reajustar a conjunção como segue:

${\displaystyle }$

Reordene a lista de argumentos concatenados de modo a deslocar um par de variáveis ​​duplicadas para a extrema esquerda e, em seguida, invoque S para eliminar a duplicação. Repetir isso quantas vezes for necessário resulta em uma lista de argumentos de comprimento max (m, n).

Os próximos três functores permitem reordenar a lista de argumento.

• Grande inversão, Inv, gira variáveis em uma lista de argumentos para a direita, de modo que a última variável torna-se a primeira.

${\displaystyle }$

${\displaystyle }$

• Menor inversão, inv, troca as duas primeiras variáveis em uma lista de argumentos.

${\displaystyle }$

${\displaystyle }$

• Permutação, p, roda a segunda a última variável em uma lista de argumentos à esquerda, de modo que a segunda variável se torne a última.

${\displaystyle }$

${\displaystyle }$

 Dada uma lista de argumentos consistindo de n variáveis, p trata implicitamente as últimas n-1 variáveis ​​como uma cadeia de bicicletas, com cada variável constituindo um elo na cadeia. Uma aplicação de p avança a cadeia por uma ligação. K aplicações consecutivas de p para F(elevado a n) move a variável k + 1 para a posição do segundo argumento em F.

 Quando n = 2, Inv e inv simplesmente trocam x1 e x2. Quando n = 1, eles não têm efeito. Assim, p não tem efeito quando n <3.

Kuhn (1983) considera inversão maior e inversão menor como primitiva. A notação p em Kuhn corresponde a inv; Ele não tem nenhum análogo à permutação e, portanto, não tem axiomas para ele. Se, seguindo Quine (1976), p é tomado como primitivo, Inv e inv podem ser definidos como combinações não triviais de +, ∃ e iteradas p.

Regras

 Todas as instâncias de uma letra predicada podem ser substituídas por outra letra predicada do mesmo grau, sem afetar a validade. As regras são:

• Modus ponens;
• Seja α e β fórmulas PFL em que ${\displaystyle }$ não aparece. Em seguida, se ${\displaystyle }$ é um teorema  de PFL, em seguida, ${\displaystyle }$ também é um teorema de PFL.

Alguns resultados úteis

Em vez de axiomatizar a PFL, Quine (1976) propôs as seguintes conjecturas como axiomas candidatos.

• ${\displaystyle }$

n-1 iterações consecutivas de p restaura o status quo ante:

• ${\displaystyle }$

+ e ∃ aniquilar uns aos outros.

• 

Negação distribui mais de +, ∃, e p.

• 
• 
• 

+ e p distribui mais de conjunção.

• 
• 

A identidade tem a interessante implicação:

• ${\displaystyle }$

Quine também sugeriu a regra: Se ${\displaystyle }$ é uma teorema PFL, então, são ${\displaystyle }$ ${\displaystyle }$ e ${\displaystyle }$.

Trabalho de Bacon

Bacon (1985) leva a condicional, de negação, de Identidade, de Preenchimento, e Maior e Menor inversão como primitivo, e de Corte definidos. Empregando a terminologia e notação um pouco diferentes do acima exposto, Bacon (1985) define duas formulações do PFL:

•  Uma formulação de dedução natural no estilo de Frederick Fitch. Bacon prova esta formulação consistente e completo em detalhes. 
• Uma formulação axiomática que Bacon afirma, mas não prova, equivalente à precedente. Alguns desses axiomas são simplesmente conjecturas de Quine reafirmadas na notação de Bacon

Bacon também:

• Discute a relação do PFL com o termo lógica de Sommers (1982), e argumenta que a reformulação de PFL usando uma sintaxe proposta em Lockwood no apêndice Sommers, deve tornar a PFL mais fácil de  "ler, utilizar e ensinar";
• Toca no grupo teórico de estrutura de Inv e inv;
• Menciona que a lógica proposicional,  a predicado monádico lógica, a lógica modal S5, e a lógica Booleana (onu)para a troca de relações, são todos os fragmentos do PFL.

Desde a lógica de primeira ordem para a função PFL

O seguinte algoritmo é adaptado a partir de Quine (1976: 300-2). Dada uma fórmula fechada da a lógica de primeira ordem, primeiro faça o seguinte:

• Anexar um índice numérico para cada predicado carta, declarando seu grau;
• Traduzir todos os quantificadores universal em quantificadores existencial e negação;
• Refaça todos as atômica fórmulas da forma x=y como Ixy.

Agora, aplicar o seguinte algoritmo para o resultado anterior:

1. Traduzir as matrizes mais profundamente aninhadas quantificadores em forma normal disjuntiva, consistindo de disjuntos de conjunções  de termos, negando termos atômicos  conforme requerido. A sub-fórmula resultante contém apenas negação, conjunção, disjunção, e quantificação existencial.

2. Distribuir os quantificadores existencial sobre o disjuntos na matriz usando a regra de passagem (Quine 1982: 119):

${\displaystyle }$

3. Substituir o conjunto pelo produto Cartesiano, invocando-se o fato de:

${\displaystyle }$

4. Concatene as listas de argumentos de todos os termos atômicos, e mover a lista concatenada para a extrema direita da sub- fórmula.

5. Use Inv e inv para mover todas as ocorrências da variável quantificada (chamá-lo de y) para a esquerda da lista de argumento.

6. Invocar S quantas vezes forem necessárias para eliminar todas, exceto a última instância de y. Elimine y prefixando a sub-fórmula com uma instância de ∃.

7. Repetição (1) - (6) até que todas as variáveis ​​quantificadas tenham sido eliminadas. Eliminar quaisquer disjunções abrangidas pelo escopo de um quantificador invocando a equivalência:

${\displaystyle }$

A tradução inversa, da PFL à lógica de primeira ordem, é discutida em Quine (1976: 302-4).

A fundação de matemática canônica é a teoria de conjuntos axiomáticas , com um fundo de lógica que consiste na lógica de primeira ordem com identidade, com um universo de discurso constituído inteiramente de conjuntos. Exite uma única letra predicado de grau 2, interpretado como o conjunto de membros. A tradução do PFL da teoria setorial axiomática canônica ZFC não é difícil, pois nenhum axioma ZFC requer mais do que 6 variáveis quantificáveis.

Veja também

• lógica algébrica
• combinatória lógica
• cilíndrica álgebra
• a relação algébrica
• prazo de lógica

Referências

• Bacon, John, 1985, "A integralidade de um predicado-functor lógica," Journal of Symbolic Logic 50: 903-26.
• Paul Bernays, De 1959, "Uber eine naturliche Erweiterung des Relationenkalkuls" em Heyting, R., ed., Constructivity em Matemática. Holanda Do Norte: 1-14.
• Kuhn, s. T., 1983, "Uma Axiomatização de Predicado Functor Lógica," a catedral de Notre Dame Diário da Lógica Formal 24: 233-41.
• Willard Quine, De 1976, "Lógica Algébrica e Predicado Ficheiro" em Formas de Paradoxo e Outros Ensaios, ampliada, ed. Harvard Univ. Prima: 283-307.
• --------, 1982. Métodos de Lógica, 4ª ed. Harvard Univ. Prima. Cap. 45.
• Sommers, Fred, 1982. A Lógica da Linguagem Natural. Oxford Univ. Prima.
• Alfred Tarski e Givant, Steven, 1987. Uma Formalização da Teoria dos conjuntos, Sem Variáveis. AMS.
• Jean Van Heijenoort, 1967. A partir de Frege para Gödel: A Origem do Livro de Lógica Matemática. Harvard Univ. Prima.

Ligações externas

• Uma introdução ao predicado-functor lógica (um-clique em baixar arquivo PS) por Esteiras Dahllöf (Departamento de Linguística, Universidade de Uppsala)