I've been asked to address this post directly.
First, a small disclaimer: I post this as a personal response, not as a representative of the Autonomic project. This post has not been discussed with the others, and does not necessarily reflect the views or official positions of our project.
As a result three questions / remarks which I found very interesting were left unanswered / undevelopped to my disappointment.
23:37 < HMC_a> so yes or no, is there a second(+) order expression which cannot be consistently proven in any mso framework? In general is full second/third order collapsible to msol, or isn't it?
I expect this one must be discussed somewhere in the works of Bruno Courcelle so you could point us to some theorem or conjecture if that can save you some time with the explanations. Don't worry about making it understandable for the mere mortals. I'm happy with an explanation that I can't fully comprehend so long as HMC and you seem to be on the same page.
Of course there are such expressions. Ohad's refusal to admit this (even contradicting himself by giving both answers) remains baffling to me.
Here is what is commonly considered one of the "canonical" examples, and it is commonly used to prove various meta-theoretical differences of second order logics:
F(Y) = forall X . (forall x,y,z . (X(x,y) -> X(y,z) -> X(x,z)) -> (forall x:Y . exists y:Y . X(x,y)) -> (exists x:Y . X(x,x))) or all x . not Y(x)
This is the class definition of finite structures. It has no mso or fol equivalents. Its' negation is the class definition of infinite structures, and ofc also has no mso/fol equivalents.
We've covered at least one or two dozen such examples in the autonomic channel over the past few months. Lately we've been discussing the expressibility boundary between full second order and Henkin semantics, as this is particularly relevant to the decidability of logics above first order. In that context, here is my favorite working example, due to its' amazing simplicity in illustrating:
forall x,y . exists P . P(x,y)
This is logically valid in full second order semantics, but does not collapse to first order as valid. Under Henkin sol semantics it is conditionally satisfiable.
22:17 < HMC_a> but maybe I'm missing some collapsability magics, somewhere, so perhaps you could give a concrete example of verification of such an example?
I concur wholeheartedly with this one. A simple example of a second or third order program in STLC+Y with limited inputs, executed against all input combinations and encoded as a tree, and then the demonstration of how msol verifies it would be hugely helpful getting some intuitive understanding of how it works. That would give us the tools to try to find a case where it doesn't work (there shouldn't be any). You can recycle that explanation for the whitepaper, so no time wasted here.
Note that his given example does not meet the request. It is a first order program, with unlimited/unconstrained inputs. His verification does not assert any property of the IO relation, for any inputs - it only verifies that the function is constant. (I agree that this property is first order expressible...)
He also seems to conflate order of functions of a signature with order of logics over a signature. (He doesn't seem to understand order of functions, either, for that matter...)
(EDIT: It was later pointed out to me that Ohad made a second post with a second example expression which was a higher order function. It still has unlimited/unconstrained input, asserts no property of IO relation, and he still verifies only a first order property of the output (as he points out at the end of his post) so this is also not an example that meets klosure's request.)
22:18 < naturalog> in bohm tree you dont have lambda terms
22:18 < naturalog> they're all reduced already
22:18 < naturalog> so the higher order rules disappear and remain only with true/false or other info
What kind of reduction are you talking about? How can the result not have lambda terms? Do you mean no lambda abstractions / bound variables? How do you guarantee that?
I'm afraid that I can't speak much to this one. Looks like
nonsense to me.
I understand that you probably don't want to bother making these explanations if you feel the tone of the conversation on IRC was not respectful, but please remember that IRC conversations are more or less supposed to serve as documentation and research log in the absence of actual documentation, and that they benefit the entire community, including investors and potential future devs who can help you on the code, so it would greatly help if technical questions are actually being answered.
You can find significant discussions of these topics in the #autonomic logs. I'm not following ##idni anymore but am told by others that it has devolved into a weird sort of echo chamber, mostly about (very old) solutions to transform problems and with very little to do with any particular logics. I'm guessing you would not find any clarifications there.
I'm also told that Ohad has now given up on mso entirely and moved to more expressive logics. From what I hear it sounds like he is lately exploring the region around/above the P-space logics, and in the "murky" area between the exptime algorithms and primitive recursion. (It is still unclear to those I've spoken to what the logic he "has in his head" actually is. AFAIK he still has not done anything to make concrete (or even further describe/qualify) his proposed framework.)
I like to joke that he is slowly making his way up the complexity families, and may even soon rejoin us in exploring "true" omega-order HOLs with full semantics, covering the full arithmetical hierarchy and in the existential N*N fragment of the analytic hierarchy.
(I can only hope that, along the way, he remembers/rediscovers why completeness and deductive proof inference should be considered
problems for the system, not features.)
As far as I'm concerned, the debate about "mso v mltt" has become entirely moot. There still seems to be room for debate wrt: completeness, decidability/term-inference, Lowenheim-Skolem/compactness/Lindstrom, (general) consistency of collapse of expressions between orders, consistency of LEM as axiomatic, or the necessity of general expression within the system. He still must disagree on one or more of these points, otherwise he'd inevitably have to just be back at MLTT as the only possible option - and back on track with the "oldtau" plan.
If he did "come around" it is unclear to me if our A.N.O.N. project members would welcome him back with open arms or tell him to go jump.
Personally, my position remains that all are welcome. Unlike newtau lately, we do not generally seek to moderate ideas or hide our design-detail information.
Edit: fixed typos
