On verifying that primitive-recursive functions are provably total in PA
Nadie ha tomado este issue todavía.
Evaluación
- Dificultad
- 4/5
- Tiempo estimado
- 3-5 días
- Aptitud para principiantes
- 25/100
- Tipo de issue
- Documentación
- Claridad
- Bastante claro
- Estado de actividad
- Estancado
- Stack tecnológico
- tex
- Área
- content, documentation
Línea de trabajo
Comienza revisando el lema de la función beta del libro y su uso de la función factorial. Compara la sustitución propuesta por lcm(1,...,j) y asegúrate de que la observación añadida explique, sin circularidad, que las funciones primitivas recursivas son demostrablemente totales en PA; se considerará terminado cuando el argumento sea completo y consistente con la demostración existente.
Escrito por el modelo de indexación a partir del texto del issue.
Descripción
As far as I see, the book doesn't state or prove that primitive-recursive functions are provably total in PA; but most of the ingredients are there! The only thing missing is an explanation that Peano arithmetic proves that one can append elements to lists (coded via the beta function as numbers). I'd like to write a remark sketching that argument. Is there interest in that?
There is, however, a slight problem. The construction given in the proof of the beta function lemma uses the factorial function. I don't know how to verify in a non-circular fashion that the factorial function is total. I'd therefore change j! to lcm(1,...,j). Unlike the factorial function, the function j \mapsto lcm(1,...,j) can be represented and verified to be total without recourse to the beta function. The rest of the proof can be adapted to this change with extremely minimal effort. Am I missing something? Should I go ahead with the change?
- Lenguaje dominante
- TeX
- Estrellas
- 1.4k
- Forks
- 289
- Métricas de merge de PR
- Sin PR fusionados en 30 d
Preparar el entorno
Este proyecto no incluye contenedor de desarrollo, Dockerfile ni guía de contribución, así que la configuración corre por tu cuenta: empieza por su README y consulta nuestra guía para la primera contribución para los pasos generales.
Primeros pasos
- Lee el issue completo y luego la guía de contribución del proyecto.
- Comenta en el issue que vas a ocuparte — evita que dos personas hagan lo mismo.
- Haz un fork del repositorio y trabaja en una rama.
- Abre un pull request que haga referencia al número del issue.
Más de OpenLogicProject/OpenLogic
-
Russel's Paradox typoAbierto
Dificultad 1/5 Menos de una hora Aptitud para principiantes 65/100
OpenLogicProject/OpenLogic#339 · 1 comentario ·
-
Dificultad 4/5 3-5 días Aptitud para principiantes 50/100
OpenLogicProject/OpenLogic#436 ·
-
Dificultad 3/5 1-2 días Aptitud para principiantes 68/100
OpenLogicProject/OpenLogic#435 · 1 comentario ·
-
Order-type of models of PAAbierto
Dificultad 5/5 Más de una semana Aptitud para principiantes 30/100
OpenLogicProject/OpenLogic#425 · 1 comentario ·
-
Improve docsAbierto
Dificultad 5/5 Más de una semana Aptitud para principiantes 25/100
OpenLogicProject/OpenLogic#390 ·
Todos los issues de OpenLogicProject/OpenLogic
Issues similares
-
community documentation first-timers-only good first issue hacktoberfest help wanted low hanging fruit up-for-grabs
Dificultad 1/5 Menos de una hora Aptitud para principiantes 70/100
lingdojo/kana-dojo#31864 · 1 comentario · 5 reacciones ·
Los mantenedores suelen responder en 1 día
-
[Server Submission]: loootAbierto
Dificultad 1/5 Menos de una hora Aptitud para principiantes 72/100
cline/mcp-marketplace#2866 ·
-
Add ZammadPosiblemente ocupada @Arslan-TR la tomó hoy. Abiertorequest
Dificultad 2/5 1-3 horas Aptitud para principiantes 66/100
endoflife-date/endoflife.date#11298 · 1 comentario ·
Los mantenedores suelen responder en 1 día
-
i18n lang:fr triage:deciding
Dificultad 2/5 1-3 horas Aptitud para principiantes 76/100
open-telemetry/opentelemetry.io#12000 · 1 comentario ·
Los mantenedores suelen responder en 1 día
-
bad link in rfc7519.htmlAbierto
Dificultad 2/5 1-3 horas Aptitud para principiantes 68/100
ietf-tools/rfc2html#80 ·