Author: tomr Format: TextFrom the one side there ir algebraization of the logics [Algebraic logic - wiki](https://en.wikipedia.org/wiki/Algebraic_logic)] - contains nice table from the propositional logic up to First Order Logic and related algebras. Google gives some results about algebraization of the second order logic and this process seems to be hard and quite unfruitful as one can see from the answer to https://mathoverflow.net/questions/36683/algebrization-of-second-order-logic .
From the other side there is relation/duality between algebra and geometry https://ncatlab.org/nlab/show/duality+between+algebra+and+geometry but it can not be complete if this duality does not extends to the algebra that would correspond to the higher order logic.
I am just trying to put all this in order - can higher algebra be of help for the algebraization of HOL. Yes or No? If no, then what to do with this gap (no algebra - geometry duality for HOL-level expressions)?
It would be nice to establish this Rosetta stone:
computing/type theories <-> algebra <-> categories <-> geometry <-> physics
for the HOL as well.
If there is some nice text about this I wold be thankful to know about it and read it. Maybe Jacob Lurie is working on this currently. No new papers from him for the past few years.
From the one side there ir algebraization of the logics [Algebraic logic - wiki](https://en.wikipedia.org/wiki/Algebraic_logic)] - contains nice table from the propositional logic up to First Order Logic and related algebras. Google gives some results about algebraization of the second order logic and this process seems to be hard and quite unfruitful as one can see from the answer to https://mathoverflow.net/questions/36683/algebrization-of-second-order-logic .
From the other side there is relation/duality between algebra and geometry https://ncatlab.org/nlab/show/duality+between+algebra+and+geometry but it can not be complete if this duality does not extends to the algebra that would correspond to the higher order logic.
I am just trying to put all this in order - can higher algebra be of help for the algebraization of HOL. Yes or No? If no, then what to do with this gap (no algebra - geometry duality for HOL-level expressions)?
It would be nice to establish this Rosetta stone: computing/type theories <-> algebra <-> categories <-> geometry <-> physics for the HOL as well.
If there is some nice text about this I wold be thankful to know about it and read it. Maybe Jacob Lurie is working on this currently. No new papers from him for the past few years.
Author: tomr Format: TextSome (Google, AI) are suggesting combinatory logic as the algebraic structure for the HOL. But if one thinks about algebra-geometry duality, then one should start with the definition of ideal and spectrum for the combinatory logic to try to find the relevant topological space. And there may be not the notion of ideal for combinatory logic. So, maybe this relation should be generalized...
Some (Google, AI) are suggesting combinatory logic as the algebraic structure for the HOL. But if one thinks about algebra-geometry duality, then one should start with the definition of ideal and spectrum for the combinatory logic to try to find the relevant topological space. And there may be not the notion of ideal for combinatory logic. So, maybe this relation should be generalized...
Author: tomr Format: TextIt seems to me that the expansion of Rosetta stone to HOL may come up with lambda-calculus as the algebraic part (very approximately, because the algebraization is ongoing process which can be observed by recent book https://link.springer.com/book/10.1007/978-3-031-14887-3 'Universal Algebraic Logic. Dedicated to the Unity of Science') and the domain theory can be the geometric part. https://www.cambridge.org/core/books/nonhausdorff-topology-and-domain-theory/47A93B1951D60717E2E71030CB0A4441 'Non-Hausdorff Topology and Domain Theory. Selected Topics in Point-Set Topology' is probably the most complete recent overview. I see the entry for algebra-geometry duality does not include the HOL counterpart (if there is any) and that is why there is no entry (in this table of dualities) for the most expressive formalism possible. Boolean algebras have very modest expression power.
It seems to me that the expansion of Rosetta stone to HOL may come up with lambda-calculus as the algebraic part (very approximately, because the algebraization is ongoing process which can be observed by recent book https://link.springer.com/book/10.1007/978-3-031-14887-3 'Universal Algebraic Logic. Dedicated to the Unity of Science') and the domain theory can be the geometric part. https://www.cambridge.org/core/books/nonhausdorff-topology-and-domain-theory/47A93B1951D60717E2E71030CB0A4441 'Non-Hausdorff Topology and Domain Theory. Selected Topics in Point-Set Topology' is probably the most complete recent overview. I see the entry for algebra-geometry duality does not include the HOL counterpart (if there is any) and that is why there is no entry (in this table of dualities) for the most expressive formalism possible. Boolean algebras have very modest expression power.