Autocatalysis and the Deduction Theorem..Autocatálisis y el teorema de deducción
....There is a surprising connection between a simple result in mathematical logic and the notion of autocatalysis. It is surprising because logic and chemistry are two seemingly disparate fields, and yet the connection is both deep and simple. The reason for its profundity lies in the fact that autocatalysis is a concept that lies at the foundation of the mathematical understanding of self-organization, and hence holds significance for the study of life. In this post, we will explore the connection between the deduction theorem and autocatalysis, and then use it to shed light on the nature of life.
..Existe una conexión sorprendente entre un resultado simple de la lógica matemática y la noción de autocatálisis. Es sorprendente porque la lógica y la química son dos campos aparentemente dispares, y sin embargo la conexión es tanto profunda como simple. La razón de su profundidad radica en el hecho de que la autocatálisis es un concepto que se encuentra en la base de la comprensión matemática de la auto-organización, y por lo tanto tiene una importancia significativa para el estudio de la vida. En esta publicación, exploraremos la conexión entre el teorema de deducción y la autocatálisis, y luego la utilizaremos para arrojar luz sobre la naturaleza de la vida. ....
The Deduction Theorem in Logic..El teorema de deducción en la lógica.
....Logic, in particular proof theory, is about formalizing the process of proof in mathematics. Given a set of logical formulas \(\Gamma\) and a single logical formula \(A\), we can ask whether \(A\) can be deduced from \(\Gamma\). This means that there is a proof of \(A\) from \(\Gamma\) using some set of inference rules provided by the logic. Inference rules are the building blocks of proofs. They consist of a set of premises and a conclusion. For example, one of the most basic inference rules is modus ponens, which has two premises \(A\) and \(A \rightarrow B\), and a conclusion \(B\). It can be written as:
..La lógica, en particular la teoría de la demostración, trata sobre la formalización del proceso de prueba en matemáticas. Dado un conjunto de fórmulas lógicas \(\Gamma\) y una única fórmula lógica \(A\), podemos preguntarnos si \(A\) puede ser deducida de \(\Gamma\). Esto significa que existe una prueba de \(A\) a partir de \(\Gamma\) utilizando un conjunto de reglas de inferencia proporcionadas por la lógica. Las reglas de inferencia son los bloques fundamentales de las pruebas. Consisten en un conjunto de premisas y una conclusión. Por ejemplo, una de las reglas de inferencia más básicas es el modus ponens, que tiene dos premisas \(A\) y \(A \rightarrow B\), y una conclusión \(B\). Puede escribirse como:....
\[\begin{prooftree}\AxiomC{\(A\)}\AxiomC{\(A \rightarrow B\)}\BinaryInfC{\(B\)}\end{prooftree}\]
....This deduction rule reads as "if \(A\) is true, and \(A\) implies \(B\), then \(B\) is true." A simple proof assembled from various uses of modus ponens is given below:
..Esta regla de deducción se lee como "si \(A\) es verdadero, y \(A\) implica \(B\), entonces \(B\) es verdadero." Una prueba simple ensamblada a partir de varios usos del modus ponens se muestra a continuación: ....
\[\begin{prooftree}\AxiomC{\(A\)}\AxiomC{\(A \rightarrow B\)}\BinaryInfC{\(B\)}\AxiomC{\(B \rightarrow C\)}\BinaryInfC{\(C\)}\end{prooftree}\]
....Whereas modus ponens specifies how to "use" an inference rule–it can convert its premises into its conclusion–there is a result called the deduction theorem that specifies how to "make" an implication from a deduction. The deduction theorem states that if a formula \(B\) can be deduced from formulas \(\Gamma\) and \(A\), then the implication \(A \rightarrow B\) can be deduced from \(\Gamma\). In other words, if we can prove \(B\) from \(\Gamma\) and \(A\), then we can prove \(A \rightarrow B\) from \(\Gamma\). Some proof systems, such as type theory, simply take the deduction theorem as an axiom. In a type system, the implication symbol is associated with an introduction rule and an elimination rule. The introduction rule is the deduction theorem, and the elimination rule is modus ponens.
..Mientras que el modus ponens especifica cómo "usar" una regla de inferencia –puede convertir sus premisas en su conclusión– existe un resultado llamado el teorema de deducción que especifica cómo "crear" una implicación a partir de una deducción. El teorema de deducción establece que si una fórmula \(B\) puede ser deducida de las fórmulas \(\Gamma\) y \(A\), entonces la implicación \(A \rightarrow B\) puede ser deducida de \(\Gamma\). En otras palabras, si podemos probar \(B\) a partir de \(\Gamma\) y \(A\), entonces podemos probar \(A \rightarrow B\) a partir de \(\Gamma\). Algunos sistemas de prueba, como la teoría de tipos, simplemente toman el teorema de deducción como un axioma. En un sistema de tipos, el símbolo de implicación está asociado con una regla de introducción y una regla de eliminación. La regla de introducción es el teorema de deducción, y la regla de eliminación es el modus ponens. ....
Understanding Catalysis and Autocatalysis..Entendiendo la catálisis y la autocatálisis.
....How does this relate to autocatalysis, a concept from chemistry? To understand the connection, let's first clarify what we mean by autocatalysis. Consider a general chemical reaction in which a substance \(A\) is transformed into a substance \(B\):..
¿Cómo se relaciona esto con la autocatálisis, un concepto de la química? Para entender la conexión, primero aclaremos qué entendemos por autocatálisis. Considere una reacción química general en la que una sustancia \(A\) se transforma en una sustancia \(B\):....
\[A \to B\]
....A catalyst is typically a substance that speeds up a chemical reaction without being consumed in the reaction:
..Un catalizador es típicamente una sustancia que acelera una reacción química sin ser consumida en la reacción: ....
\[A + C \to B + C\]
....We are not so much concerned with the catalyst \(C\)'s ability to speed up the reaction, but rather the fact that it is "recycled" in the reaction, in a way that it can be used again and again. We will refer to any reaction in which a substance is "recycled" in this way as a catalytic reaction, and to the recycled substance as the catalyst. Also, we are not concerned with "reactions" in the traditional sense of a chemical reaction, but rather with processes in which an input is transformed into an output. As such, a reaction will not necessarily conserve the materials involved. It is possible for a reaction to create new materials as well as destroy existing ones. We will interpret this as a process in which materials that are readily available from the environment are used to create a desired output, in the case of creation of new materials, or in which materials are dissolved into the environment in the case of destruction of existing materials.
..No nos interesa tanto la capacidad del catalizador \(C\) para acelerar la reacción, sino más bien el hecho de que se "recicla" en la reacción, de manera que puede usarse una y otra vez. Nos referiremos a cualquier reacción en la que una sustancia se "recicla" de esta manera como una reacción catalítica, y a la sustancia reciclada como el catalizador. Además, no nos preocupan las "reacciones" en el sentido tradicional de una reacción química, sino más bien los procesos en los que una entrada se transforma en una salida. Como tal, una reacción no necesariamente conservará los materiales involucrados. Es posible que una reacción cree nuevos materiales y destruya los existentes. Interpretaremos esto como un proceso en el que los materiales que están fácilmente disponibles en el ambiente se utilizan para crear una salida deseada, en el caso de la creación de nuevos materiales, o en el que los materiales se disuelven en el ambiente en el caso de la destrucción de materiales existentes. ....
....An autocatalytic reaction is then a process in which a catalyst is used to create more of itself such as
..Una reacción autocatalítica es entonces un proceso en el que un catalizador se utiliza para crear más de sí mismo, como ....
\[A\to A+A\]
....Here, we are not so much concerned with the idea of a single autocatalytic reaction, but with the idea of a collection of reactions that can be collectively described as autocatalytic. For example, neither of the two reactions \(A\to B+B\) and \(B\to A+A\) are autocatalytic by themselves, but together they can form an autocatalytic cycle: applying the first reaction to \(A\) creates two \(B\)'s, one of which can then be used to create two \(A\)'s through the second reaction, leading to the overall reaction \(A\to A+A+B\), which is autocatalytic. Moreover, the pair of reactions can be said to be, in a sense, "collectively autocatalytic," because both \(A\) and \(B\) are autocatalytic, that is, they both appear in at least one autocatalytic cycle.
..Aquí, no nos interesa tanto la idea de una única reacción autocatalítica, sino la idea de una colección de reacciones que pueden describirse colectivamente como autocatalíticas. Por ejemplo, ninguna de las dos reacciones \(A\to B+B\) y \(B\to A+A\) son autocatalíticas por sí mismas, pero juntas pueden formar un ciclo autocatalítico: aplicando la primera reacción a \(A\) se crean dos \(B\), uno de los cuales puede usarse para crear dos \(A\) a través de la segunda reacción, llevando a la reacción general \(A\to A+A+B\), que es autocatalítica. Además, se puede decir que el par de reacciones es, en cierto sentido, "colectivamente autocatalítico", porque tanto \(A\) como \(B\) son autocatalíticos, es decir, ambos aparecen en al menos un ciclo autocatalítico. ....
....There is a stronger sense in which a collection of reactions can be said to be autocatalytic. In addition to each component being involved in an autocatalytic cycle, we can require that each reaction in the collection be catalyzed by the output of some other reaction in the collection. This stronger form of collective autocatalysis, and its variations, have been studied extensively for their potential role in understanding the origin of life. Indeed, a system of molecules that collectively exhibit this form of autocatalysis would have the potential to self-replicate, and thus would be a candidate for the origin of life. And there is no reason to stop at the level of molecules. Any collection of entities that are involved in processes that can be described as autocatalytic in this sense can be said to exhibit a form of self-organization. We can then envision various "origins of life" taking place at various scales, from the molecular to the cellular and all the way to the social and economic.
..Existe un sentido más fuerte en el que se puede decir que una colección de reacciones es autocatalítica. Además de que cada componente esté involucrado en un ciclo autocatalítico, podemos requerir que cada reacción en la colección sea catalizada por el producto de alguna otra reacción en la colección. Esta forma más fuerte de autocatálisis colectiva, y sus variaciones, han sido estudiadas extensamente por su papel potencial en la comprensión del origen de la vida. De hecho, un sistema de moléculas que exhibe colectivamente esta forma de autocatálisis tendría el potencial de autorreplicarse, y por lo tanto sería un candidato para el origen de la vida. Y no hay razón para detenerse en el nivel molecular. Cualquier colección de entidades que estén involucradas en procesos que puedan describirse como autocatalíticos en este sentido puede decirse que exhibe una forma de auto-organización. Podemos entonces visualizar varios "orígenes de la vida" ocurriendo en varias escalas, desde la molecular hasta la celular y hasta la social y económica. ....
The Bridge Between Logic and Chemistry..El puente entre la lógica y la química.
....But what in the world does this have to do with the deduction theorem, as the title of this post suggests? The answer requires us to bridge the gap between the world of logic and the world of chemistry, or more generally of processes. We have seen that modus ponens is an inference rule that specifies how to use an implication, namely, to convert its premises into its conclusion. We can envision an analogy between logic and chemistry by regarding the formulas of logic as "molecules" and the inference rules as "reactions". We can recast modus ponens as a reaction:
..Pero ¿qué tiene que ver esto con el teorema de deducción, como sugiere el título de esta publicación? La respuesta requiere que tendamos un puente entre el mundo de la lógica y el mundo de la química, o más generalmente de los procesos. Hemos visto que el modus ponens es una regla de inferencia que especifica cómo usar una implicación, es decir, cómo convertir sus premisas en su conclusión. Podemos visualizar una analogía entre la lógica y la química considerando las fórmulas de la lógica como "moléculas" y las reglas de inferencia como "reacciones". Podemos reformular el modus ponens como una reacción: ....
\[A+A\Rightarrow B\to B+A\Rightarrow B\]
....We have replaced the implication symbol \(\to\) with the arrow \(\Rightarrow\) to distinguish between the logical implication and the chemical reaction. Notice that we have preserved the implication \(A\Rightarrow B\) as a catalyst of the reaction, and that this does not affect the logical validity of the underlying inference rule. So the idea is that implication formulas act as catalysts for the reaction that transforms its premises into its conclusion.
..Hemos reemplazado el símbolo de implicación \(\to\) con la flecha \(\Rightarrow\) para distinguir entre la implicación lógica y la reacción química. Observe que hemos preservado la implicación \(A\Rightarrow B\) como un catalizador de la reacción, y que esto no afecta la validez lógica de la regla de inferencia subyacente. Así que la idea es que las fórmulas de implicación actúan como catalizadores para la reacción que transforma sus premisas en su conclusión. ....
....Under this analogy, the deduction theorem has a strong connection to autocatalysis. The deduction theorem implies that each valid deduction, hence each possible process, has a corresponding catalyst. The catalyst for the process \(A\to B\) is the implication \(A\Rightarrow B\). In more explicit terms, the deduction theorem implies that if we can prove \(B\) from \(A\)–that is, if we can transform \(A\) into \(B\)–then we can create \(A\Rightarrow B\) from components present in the environment. If, in addition, each component in the system is the product of some reaction in the system, then we can say that the system exhibits autocatalysis. For example, the components of the system can be all of the formulas that can be proved from the axioms, which is a set of formulas that can be readily produced from the environment, in which case all of the components are the result of some proof process, and hence the product of some reaction in the system.
..Bajo esta analogía, el teorema de deducción tiene una fuerte conexión con la autocatálisis. El teorema de deducción implica que cada deducción válida, y por lo tanto cada proceso posible, tiene un catalizador correspondiente. El catalizador para el proceso \(A\to B\) es la implicación \(A\Rightarrow B\). En términos más explícitos, el teorema de deducción implica que si podemos probar \(B\) a partir de \(A\)–es decir, si podemos transformar \(A\) en \(B\)–entonces podemos crear \(A\Rightarrow B\) a partir de componentes presentes en el entorno. Si, además, cada componente en el sistema es el producto de alguna reacción en el sistema, entonces podemos decir que el sistema exhibe autocatálisis. Por ejemplo, los componentes del sistema pueden ser todas las fórmulas que pueden probarse a partir de los axiomas, que es un conjunto de fórmulas que pueden producirse fácilmente desde el entorno, en cuyo caso todos los componentes son el resultado de algún proceso de prueba, y por lo tanto el producto de alguna reacción en el sistema. ....
Self-Organization and Proof Systems..Auto-organización y sistemas de prueba.
....What we have described here is a physical system, be it chemical or otherwise, that by virtue of behaving like a proof system, can exhibit autocatalysis and hence self-organization. Conversely, if a physical system exhibits autocatalysis, then we can describe it as a kind of generalized proof system. This suggests one approach for constructing elementary artificial life systems: implementing well-studied proof systems that can demonstrate self-organization. Additionally, by studying naturally occurring self-organized systems in biology, we can begin to understand the natural logic of life in its native language.
..Lo que hemos descrito aquí es un sistema físico, ya sea químico o de otro tipo, que en virtud de comportarse como un sistema de prueba, puede exhibir autocatálisis y por lo tanto auto-organización. A la inversa, si un sistema físico exhibe autocatálisis, entonces podemos describirlo como una especie de sistema de prueba generalizado. Esto sugiere un enfoque para construir sistemas de vida artificial elementales: implementar sistemas de prueba bien estudiados que puedan demostrar auto-organización. Además, al estudiar sistemas auto-organizados que ocurren naturalmente en biología, podemos comenzar a entender la lógica natural de la vida en su lenguaje nativo. ....
....These connections between logic, computation, and self-organization have been explored in various ways. Fontana's work on lambda calculus—a model of computation closely related to logic—directly investigates these relationships. Other research, such as Chemical Organization Theory, Kauffman's autocatalytic sets, and additional work on autocatalysis (including a collaboration I was involved in), has focused on understanding the role of autocatalysis in self-organization. However, these latter approaches have not fully explored the surprising connection between self-organization and the foundations of mathematics and computer science.
..Estas conexiones entre lógica, computación y auto-organización han sido exploradas de diversas maneras. El trabajo de Fontana sobre el cálculo lambda—un modelo de computación estrechamente relacionado con la lógica—investiga directamente estas relaciones. Otras investigaciones, como la Teoría de la Organización Química, los conjuntos autocatalíticos de Kauffman, y trabajo adicional sobre autocatálisis (incluyendo una colaboración en la que estuve involucrado), se han centrado en comprender el papel de la autocatálisis en la auto-organización. Sin embargo, estos últimos enfoques no han explorado completamente la sorprendente conexión entre la auto-organización y los fundamentos de las matemáticas y la ciencia de la computación. ....
Implications for Artificial Life and Biology..Implicaciones para la vida artificial y la biología.
....I picture a cell, whether natural or artificial, as a tiny mathematician that is constantly proving theorems. These theorems likely serve as abstract hypotheses about its own state and environment, allowing it to use its internal logic to reason predictively about its future and make decisions based on the outcomes of that reasoning.
..Me imagino una célula, ya sea natural o artificial, como un pequeño matemático que constantemente está demostrando teoremas. Estos teoremas probablemente sirven como hipótesis abstractas sobre su propio estado y entorno, permitiéndole usar su lógica interna para razonar predictivamente sobre su futuro y tomar decisiones basadas en los resultados de ese razonamiento. ....
