## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthortomr
• CommentTimeApr 17th 2023
• (edited Apr 17th 2023)
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.
• CommentRowNumber2.
• CommentAuthortomr
• CommentTimeApr 17th 2023
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...
• CommentRowNumber3.
• CommentAuthortomr
• CommentTimeApr 17th 2023
• (edited Apr 17th 2023)
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.