Estou procurando trabalho em sistemas semelhantes às sequências de ordem superior de K. Dosen ("Sequent Systems for Modal Logic", JSL 50 ). O único trabalho que conheço é o trabalho recente de Iemhoff e Metcalfe ("Teoria da prova de regras admissíveis", Annals of Pure and Applic Logic 159 (1-2), 2009).
Existem outros documentos sobre esses sistemas?
Respostas:
Mais uma vez, não sei exatamente o que você está procurando, porque há potencialmente muitos sistemas "semelhantes", mas, para trabalhos recentes que eu acho muito relacionados, você pode ler a Parte II ("Derivabilidade de mistura e admissibilidade") da tese de Dan Licata , bem como lógica de provabilidade construtiva de Rob Simmons e Bernardo Toninho.
fonte
Não consigo encontrar o artigo on-line, mas, com base nas referências a ele, o sistema de Dosen altera o contexto de uma sequência ou multiset para uma estrutura gráfica mais geral. Isso é uma reminiscência de várias coisas.
A lógica de exibição de Belnap, na qual muitos conectivos (e não apenas conjunção / disjunção) são internalizados na estrutura sequencial.
É também uma reminiscência da dedução rotulada, na qual a estrutura gráfica é simulada adicionando rótulos a hipóteses e julgamentos e exigindo concordância entre os dois para descarregar uma hipótese. A tese de doutorado de Alex Simpson investiga aplicações desses sistemas à lógica modal.
Noam Zeilberger investigou interpretações da regra ômega de Buchholz (e generalizações dela) como uma regra de inferência literalmente de ordem superior, na qual a premissa de uma regra se torna uma função (isto é, um objeto de ordem superior) que gera as premissas. Veja seu artigo sobre o POPL 2008, "Focando e sintaxe abstrata de ordem superior".
fonte
Veja o levantamento dos cálculos de prova da lógica modal no capítulo 3 da tese de Phiniki Stouppa de mestrado em Design de teorias modais de prova: o caso de S5 .
No IIRC, ela discutiu como 11 sistemas lidaram com a formalização do S5.
fonte