Una prueba de integridad para una lógica de predicado regular con un valor de verdad indefinido

Por • 21 dic, 2021 • Sección: Leyes

Antti Valmari , Lauri Hella

Ofrecemos un sistema de prueba sólido y completo para una extensión de la lógica ternaria de Kleene a los predicados. El concepto de teoría se amplía con, para cada símbolo de función, una fórmula que especifica cuándo se define la función. La noción de «está definido» se extiende a términos y fórmulas mediante un sencillo algoritmo recursivo. Las fórmulas «está definido» se construyen de modo que ellas mismas estén siempre definidas. La prueba de integridad se basa en la construcción Henkin. Para cada fórmula, precisamente una de la fórmula, su negación y la negación de su fórmula «está definida» es verdadera en el modelo construido. Muchas otras lógicas ternarias de la literatura pueden reducirse a la nuestra. Las funciones parciales son omnipresentes en la informática e incluso en la resolución (in) de ecuaciones en las escuelas.

 arXiv:2112.04436v1 [math.LO]
Logic (math.LO); Logic in Computer Science (cs.LO)

Post to Twitter

Escribe un comentario