Lambda the Ultimate

I think that FOL is a necessary part of the education of a logician (that is, it is an indispensable tool in the toolkit of a logician), but it might not be necessary for people who study logic with an eye to applications in another discipline.

Multisorted logic is expressive, but with Henkin semantics it fails to have the properties that Hewitt is after, and with the set-theory-in-sheeps'-clothing semantics it fails to have a proof theory. Which is what led Hewitt to propose a non-monotone, paraconsistent logic for foundations, but I don't know what Logic 101 would look like if it subsititued that logic for FOL.

What do you mean it doesn't have a proof theory? The FOL encoding of SOL makes things ugly, but I don't see how it changes anything substantive.

SOL the language has one syntax but two semantics. The encoding you talk about is for one of those semantics, the Henkin semantics, but the other semantics is non-first-orderisable.

My point is that SOL and a particular multi-sorted FOL are basically isomorphic. You give me a sentence or a proof in one and I can convert it to the other. Just as you can study Henkin semantics for SOL, you can study a full semantics (contains all functions) for FOL. The important distinction between first order and second order is therefore about semantics, whereas the difference between FOL and SOL as logics is just syntax.

The topic is semantics, but completeness also involves semantics.
If you restrict FOL to models with full semantics, you lose completeness by Gödel's theorem. And to define the semantics you want you need to know which sorts to handle specially—that is, to look at the original SOL you're encoding. This answer claims that "treat some sort specially at the semantic level" is all there is to SOL:
https://math.stackexchange.com/a/24004/79293

Citation needed. I suspect that you might be right in a sense even though what you say contradicts most stated facts around, but that sense is not interesting. In particular, it doesn't make proof theory complete — but I suspect completeness of proof-theory for FOL is useless anyway. I'm also not sure you can really define your semantics without reference to a second-order logic anyway—you need to know what sorts must be treated specially, and those are the sorts generated by the translation.

Take a logic L that includes Peano arithmetic. By Gödel, L can't show all facts that are true in all "intended/standard models" for Peano arithmetic. A complete logic (that is, a logic with a complete proof theory) must show all facts that are true in all models.

So either you allow non-standard models (as FOL does) or you lose completeness (as SOL with full semantics does). In particular, say you translate your SOL formulas to FOL, but still give the same semantics. You are ruling out some non-standard models—more facts are true for all remaining models, yet you haven't extended your proof theory, so your FOL logic is now incomplete for this new class of models. And by Gödel's theorem you can't fix this up.

Nevertheless, who cares about completeness, since SOL proves everything that FOL proves? We can't check SOL didn't forget rules by proving completeness, but we can check it's as powerful as FOL. Might be annoying for SOL metatheory, but seems fine for using SOL.

Caveat: I'm no expert, and this confused me for a while, but I remember I confirmed it in Peter Smith's book on Gödel's theorem (borrowed copy). Which is to say, I might still be in error, but I did a basic sanity-check of the idea.

I think I agree with what you've written, which is confusing since you seem to be arguing with me. You write this:

Just as you can study Henkin semantics for SOL, you can study a full semantics (contains all functions) for FOL.

Citation needed. [...]

Hmmm, I think I was just trying to say the same thing you quoted off of stack exchange. Namely, SOL is the same as FOL with extra structure required in the model.

But look at the context. Dr. Hewitt (and now Charles?) was claiming that FOL is deficient as a logic. That seems to contradict the above observation. How can FOL be deficient and SOL not when the two are really just the same logic with different default interpretations?

I wasn't proposing FOL as a way of obtaining completeness, which you seem to have assumed. I agree there's no significant advantage there. You can obtain a similar completeness result for SOL if you just restrict to Henkin models. The real reason FOL is complete and SOL is incomplete is that "complete" means different things for the two because of the more restrictive models required (just by convention!) of SOL.

I might get the confusion—if so, the point is subtle. The original question was:

You say:

I think if you change the semantics without getting a matching proof syntax, you don't have a (good) proof theory, at least for logicians that prefer FOL. Logics is defined by having matching syntax and semantics—hence SOL is a perfectly good thing but isn't logics, just set theory.

I agree with the first part:
> The important distinction between first order and second order is therefore about semantics

but the second part is not true in the right sense:
> whereas the difference between FOL and SOL as logics is just syntax.

The problem is that FOL as logics is the combination of "first order (semantics)" + first order syntax; similarly, SOL as a logics is second order semantics + second order syntax. You can encode that syntax into the syntax of first-order logics, and I trust you that the proof still works, but the encoding is not sound enough (because it doesn't impose the extra restrictions on the models).

I'm no logician, but I understand logics is about having matching syntax and semantics. If you drop that requirement, the word "logic" becomes void of meaning. When people build program logics (often on top of some existing semantics), they build a proof theory matching some model theory, so that you can reason within the proof theory of the logic without needing extra assumptions about models. If you can't, you don't have a (good) proof theory. And that's annoying. Compare using Hoare logic, where you reason directly on programs, against reasoning in some complicated model using crazy mathematics we don't get—say bfagh theory. Let's say that Hoare logics is proven sound using bfagh theory. If its proof theory is complete, we can forget about bfaghs and stick to the proof theory. (This argument appears often in papers about program logics for FOO).

Again, using an embedding of syntax that doesn't respect semantics is not doing logics.

After explaining this, maybe I get why Gödel results are claimed to mean that the reduction of mathematics to logics (as Gödel wanted) has failed. By the above discussion and Gödel, we can't study natural numbers purely via proof theory, because it's not complete—we *have* to move to model theory. That is, we can't study naturals within the boundaries of logic. It also follows that FOL is a perfectly good logics, but for classes of models of limited interest — hence we use set theory.

Or we follow a different school and use intuitionistic logics (where we also reject completeness).

The same way, you could also go to a category theorist, give him an isomorphism between the objects of two categories that doesn't preserve the arrows, and claim the categories are isomorphic as categories, it's just the arrows that don't match. That's more clearly false — but even once you fix the terminology and do something interesting with this isomorphism, you still aren't doing category theory.

I can only respond from a phone this weekend so I'll keep it short. I agree logic is syntax + semantics. But when someone talks about FOL or SOL I assume they're talking about the formal system. However you make these definitions, the idea that we can't use FOL as a formal system because it can pin down the naturals seems wrong. It can prove all the same things that SOL can. ZFC uses FOL.

I think you could use intuitionistic propositional logic (IPL), and such a logic has a nice proof theory, within the grasp of a first-year bachelor's student, and it leads naturally into Horn-clause logic and higher-order logic programming. So if ZOL=IPC, then I think your idea would be feasible.

> did you get something out of his papers? Or can we just stick to published papers on other paraconsistent logics?

I had trouble with his papers, but I did narrow down that he is talking about something resembling a second-order linear logic-ish type theory, which is in the space of things that I find interesting.

This led me to the conclusion that while Hewitt's work is fringe and his style of presentation sets off all sorts of alarm bells, he is not pushing something absurd.

> I consider discussion on Hewitt's de facto banned here

I missed the memo, sorry...

As I recall, Ehud had remarked that he sometimes puts people under moderation; that is, they can still comment on LtU but their comments don't appear until cleared; and in principle such a person can continue to contribute as long as they behave themselves but in practice such people only linger for a while and then choose to leave and are heard from here no longer. And then, later, Ehud stepped in, saying he felt he'd been more than patient, and did that to Hewitt. And Hewitt did make a few (visible) comments on some things after that, but soon was heard from here no longer.

Personally, I went through a very gradual (and painful) process of downgrading my opinion of Hewitt until I finally reached the point where I no longer considered his work worth bothering to read.

On style of presentation, I note that once upon a time, browsing in a university library (the physical kind, with dead-tree books in it), I came across a physics title that sounded absolutely fascinating to me. So I cracked it open, and found that it was written in an extremely fringe, conspiracy-theory-heavy style. Like, the author was talking in the preface about how the theories of his mentor, which the book further developed, had been shamefully suppressed by the physics elite who apparently feared they would lose their jobs if their work was revealed to be a sham. Hard-core conspiracy stuff. But it looked as if the actual theories might be rather interesting --- and then I had this flash of insight. Thomas Kuhn, in talking about scientific paradigms, notes (iirc) that the paradigm itself is an exemplar of research; it defines not only sorts of entities to be studied, sorts of questions to ask, sorts of answers, sorts of methods --- it also sets the style for how things will be expressed. In other words, this researcher whose work I was looking at was, quite possibly, a serious researcher doing interesting work, who was unfortunately also poisoning his own work, making it sound fringe, not because he was by nature a conspiracy theorist, but because he had learned to write in that style by his mentor who was a natural. I don't think Hewitt is like that; I tend to think Hewitt is a first-generation whatever-he-is. But I acknowledge that such a phenomenon can occur.

Link doesn't work

...maybe try again?

Doesn't work for me, either.

The link works if you're currently signed into Google, but it returns 404 if you try to load it in an incognito tab.

...for figuring this out. I was puzzled. I guess that isn't intended behaviour on Google's part.

...seems along the right lines. It is possible that his work might be fruitful.

Possible is a low bar, logically. Considering available evidence to judge whether I think it likely enough to justify studying his work, I think not. There are a variety of different ways one could violate Gödel's premises so that the theorem(s) wouldn't hold; these tend to involve producing things that can't be constructed; and when someone comes up with something that seems to get around Gödel, and it's not clear why, one tends to suspect that one of these unconstructable thingies has crept into their treatment through the back door while no-one was looking — but in Hewitt's case, it seems he not only does such a thing up front, he does lots of them up front, as if he wasn't sure if what he'd done was really enough to bury Gödel so he kept adding more on for good measure. This suggests to me (as circumstantial evidence) someone who doesn't really understand the underlying principles at all. Could there be something to it? Maybe. But I've past the point of suspending disbelief, and now to change my mind I'd really like to see a simple and lucid explanation of why what he's doing is worthwhile (yes, I realize that's a tall order).

My conclusion from the last Hewitt mega-thread was that his logic is probably consistent (or could be made consistent once the bugs were ironed out) but doesn't contradict anything Godel proved and probably wouldn't have been surprising to Godel. It's straightforward to a logic and add a symbol that is intended to represent a provability relation. But unless you also provide sufficient axioms to pin down exactly what that symbol means (i.e. that there is a tree of concrete proof objects that are related to each other according to the rules of inference and terminate with the theorem to be proved) then it's easy to remain consistent while ostensibly proving "there is no proof of false". Caveat: As you know, the exact state of affairs was quite difficult to determine so the above is a best guess. And to respond to Charles, I recall that Thomas Lord thought he was on to something, so you could try him.

I did at one point suspect that the calculus might be set-theory-in-sheep's-clothing second order, so reducing the consistency proof to one that assumes the consistency of mathematics and thereby being trivial. It is an easy mistake to make if you are not careful. I was not sure, though.

"Progress in mathematics almost demands a complete disregard of logical scruples." — Morris Kline, Mathematical Thought from Ancient Through Modern Times, §18.4.

- wrong memory -

FOL has first-class quantification (and implication), Aristotelian logic does not. There is an easy embedding of Aristotelian logic in FOL but it only goes one way. It is not difficult to give satisfactory constructive interpretations of Aristotelian logic, unlike FOL.

The notion of first-class-ness interweaves with Gödel in some deep way that I don't grok in fullness, although various facets of it seem clear enough. The natural next step, beyond first-class quantifiers, seems to me to be what Church did with them in his logic: he didn't like having different kinds of variables with different kinds of semantics, so he envisioned a single variable binder that would be the only one in his logic, called λ, and for quantification he used higher-order operators Σ and Π, where proposition (ΣF) provable means there is some X such that (FX) is provable, and (ΠF) provable means for every X, (FX) is provable. So the quantifiers don't themselves bind variables, instead farming out the variable-binding task to the first-class function they're applied to. But Church's logic does then have to have first-class functions, which in programming are rather the holy grail of first-class-ness. Antinomies apparently need self-reference, closely related to computational recursion/iteration which is facilitated by first-class functions; a particularly simple antinomy, Curry's Paradox, is afforded by a logic with first-class functions, an implication operator, and just a few seemingly innocuous axioms; so λ itself apparently provides all the brute-force part of what's needed for antinomies. As remarked, λ is really about variable binding. And the notion of first-class-ness was devised, in programming, by Christopher Strachey who synthesized it (as Peter Landin recounted) from W.V. Quine's dictum "To be is to be the value of a variable" (as I recall, he said that in the context of an exercise where he had a sentence something like "Pegasus has wings", transformed it into logic where the nouns get represented by variables, something like "for all X, if X is Pegasus then X has wings", and then noted that this gives a perfectly clear semantics to the sentence regardless of whether Pegasus exists, but the question of whether Pegasus exists then becomes a question of whether there is a value for X that makes "X is Pegasus" true).

I've remarked before about my logic which I will describe with a couple of papers to be released soon. Actually, I would have already done so if not for this nagging feeling that if I just tweak things slightly a couple of last pieces will fit perfectly into place that right now feel a bit awkward. One hope I have is that with a slight tweak, the logic will be able to encode its own meta-theory (in a natural way... rather than by brute force bolting it on as I've described elsewhere). But I should probably just publish what I have. Someone else can probably explain how to fix it.

Anyway, the reason I wanted to respond is that the core part of my logic works just like Curry's logic in the way that you describe above. Quantification converts a theory of N parameters to a theory of N-1 parameters. But one difference from what you describe above is that I don't use the same binder for theories & functions. I use λ for functions and have a different binder, π for partition, that I use to build theories. This allows functions to remain parametric, so that you can't write λn. n:Nat, which would break everything nice about functions. But you can write πn. n:Nat. So this distinction makes some sense to me. And this distinction is important for avoiding paradoxes, BTW.

Edit: Many years ago I went down the path of having everything use a single binder, but once it became clear how I wanted to model theories and functions semantically - as different things - have them separated in the surface syntax just made sense.

Sounds interesting. Curry's Paradox does imho raise a suspicion that the difficulty has something to do with how casually various terms are treated as logical propositions; it seems rather plausible that some sort of type separation as you describe might help.

I think I actually had variants of my logic that had only a single binder and for which I didn't know of any antimony (but I didn't have a model in mind, either). To avoid Curry's paradox we just need to avoid assuming that an arbitrary expression can be used as a sensible proposition.

I think you might be interested* in my logic because I think we have similar concerns about the directions of type systems. I'm guessing you and I find Curry's logic appealing for similar reasons ... it separates computation from types that classify computation.

* Assuming my soundness proof isn't shown to be wrong and my logic isn't shown to be inconsistent.

I've been having a trouble with self referring terms also. I've solved it by strictly separating each recursion step in the process. This leads to a theory where a function result can't be used as its parameter unless the recursion terminates at some step.

Thinking logically, the problem is similar to deciding if a forever-self-recursing term is true. It seems that such a term is simply not valid and should be considered as an error, if I'm not wrong.

a function result can't be used as its parameter unless the recursion terminates at some step.

But that would be undecidable... [...wouldn't it?]

a function result can't be used as its parameter unless the recursion terminates at some step.

But that would be undecidable... [...wouldn't it?]

That's exactly the point. Recursion steps should be isolated one from another. Otherwise we would have a reactive infinite loop between a parameter and a result.

In other words, I mean that a recursive function is undecidable if it doesn't terminate in finite number of steps, which is a case in Curry's paradox.

Of course, in some cases we can rewrite a recursive function definition in some higher order notation to embrace infinite set of results, but I believe this is not possible for Curry's paradox.

I think John was asking how you tell that the recursion is going to terminate. Most languages that worry about this do it by structural induction -- the parameter has to get smaller on each recursive call, ensuring termination. Actually doing the termination check at compile time is going to be quite limiting, because it means the parameter can't depend on run-time data.

I'm afraid that a complete compile time check is not possible. Doesn't sound cool, but detecting run-time infinite loops by user observation is all we can get here. Still, some partial detection engine could exist, but I wouldn't count on its completeness.

For a while now I'm having an idea of automatic converting set formation infinite loops to higher order definitions that don't need loops to check some element existence. But I didn't get too far, as I ended up again in internal loops whose time of execution depends on a number of iterations for constructing checked element, and sometimes never ends (i.e. in a case of pseudo-random numbers). I think what I need here is a kind of set of universal term-rewrite rules that do the magic before the result set even gets to the interpreter.

Parigot was led to separate out from the single binder syntax of call/cc to have an additional kind of binder to handle what can be viewed as negative assumptions: doing so led to a lot of clarity. The minimum number of concepts is not always the most intelligible place to be.

Thanks Charles, your reply rocked me back in several ways.

There is an easy embedding of Aristotelian logic in FOL but it only goes one way.

So FOL (Predicate Logic) is beyond (more expressive than) Aristotelian. And your O.P. quotes "First-order theories are entirely inadequate". Are you suggesting Aristotelian is more adequate? You must be using "beyond" in some sense I wasn't previously aware of.

(Also why are you reviving a thread from ~4 years ago? I do not believe for one moment that Hewitt has overturned Gödel. Remember that a "eventually consistent" system is a sometimes-inconsistent system. And from an inconsistency you can infer anything, including potentially contradicting well-established theorems. Hewitt has not shown that calling some system Inconsistency-robust makes it robust for programming purposes.)

FOL has first-class quantification (and implication), Aristotelian logic does not.

The classic Aristotelian "all ...", "some ..." quack like quantifiers to me. If you mean the standard A-form "all men are mortal" doesn't exactly correspond to ∀ because the A-form carries existential import, all that means is it's a different system of quantifiers.

The forms of syllogism are essentially expressing the transitivity of implication, to take "Barbara":

All humans are animals
All animals are mortal
-------------------------------
All humans are mortal


The A-form is an implication; The Barbara form requires the second term of the first line to be the first term of the second line. Then we eliminate that shared term in the conclusion, which is an implication from first term of the first line to the second term of the second line.

Are the quantification or the implication "first-class"? You'll have to explain what that means in the context of a system of logic. But anyway why does it matter?

In what way does being "second class" or whatever put Aristotelian "beyond" Predicate Logic?

It's quite true that Predicate Logic is not adequate for Computer Science: it's not Turing Complete/can't express recursion; isn't second-order so can't express e.g. continuations or monads; etc; etc. But that doesn't seem to be the substance of your objections to it.

It is not difficult to give satisfactory constructive interpretations of Aristotelian logic, unlike FOL.

OK, constructivist interpretations are applicable -- particularly for type theory and the Curry-Howard correspondence. I'd like to see how you get from Aristotelian logic to Higher-Order types without explicit quantification.

Aristotelian logic is a starting point from which many paths may be taken, leading to many different perspectives on what logic is, with FOL being the most important destination at present.

Both quantification and implication exist in Aristotelian logic, but they cannot be nested, which is why I say these concepts are not first class there.

What parts of SQL are you referring to? I don't think I ever use queries that don't fit into Codd's original model of relational algebra. I think SQL is first order because you cannot abstract/quantify over tables?

Oh dear, Keean. Possibly in SQL you do stick with RA-expressible queries; then good on you. But have you been living under a rock?

What parts of SQL are you referring to?

CTEs (Common Table Expressions) have been in the standard since 1999. With them you express recursive queries/transitive closure, typically spanning parent-child hierarchies. They (in effect) take a relational expression as parameter, so they're definitely second order.

I agree with @rp they should have been there from the start. But Codd always talked of a data manipulation "sub-language" as if SQL should be embedded in something else that was Turing complete.

Various procedural features (such as Oracle PL/SQL) have been de facto in SQL for a long time, although I'm surprised to see only in the standard since 1999, says wikipedia. These features support looping and cursor-based access to rows. So also Turing complete.

Very often the procedure stays within first order, but there's no way to guarantee that. And very often what it's doing could be expressed using ordinary SELECT statements and set operators, but ditto.

I disagree with this 'RBAR' approach. It offends against Codd Rule 7 (and probably 12). Furthermore it's usually horribly less efficient than giving the whole statement to the query optimiser.

Edit:Errk! How could I have forgotten aggregate operators? (COUNT, SUM, MAX, etc) Again Codd didn't consider these in his original RA. (So the RA's G operator is a later addition.) We can give the semantics for these using, for example, a fold (map-reduce) over a partitioning of a relation. A fold is second-order. A partitioning is not a relation, but a set of relations, needing a second-order predicate to give its semantics.

I don't think I ever use queries that don't fit into Codd's original model of relational algebra. I think SQL is first order because you cannot abstract/quantify over tables?

Er, how to untangle that claim? I wonder what you mean by "abstract over"? Being able to parameterise over tables and especially column names would be really, really, really, really useful. You could parameterise the columns to project on; you could write generic queries to (for example) find all the tables with a user/timestamp to build an audit trail.

In no way would that be second-order.

Re quantifying: Relational division corresponds to universal quantification; projection corresponds to existential quantification (of the attributes projected away).

Second-order means abstracting over functions/expressions -- i.e. what a CTE does.

Other warts that have always been in SQL, also corrupt its semantics as compared with RA. Are they second order? Who knows?

Duplicate rows: what on earth is the semantics for them?

Anonymous columns or duplicate column names: what do they mean?

Nulls: what's the relation predicate when nullable fields are included? How does the Closed World Assumption work? What does a null in an Outer Join 'mean' (using the term loosely), as compared to a null in a base table?

Yes I know Codd sanctioned nulls. See also how many versions of nulls he invented and dis-invented and tried to make sense of with its two-and-a-half-value logic.

CTEs are not second order. They just define names for sub-queries. They can also define recursive queries, but these are also first-order (recursion in SQL is also limited to linear recursion, I believe, although some DBs go beyond that). The SQL standard aggregates are all first-order too, I believe, but I haven't checked them all. The fact that you can define them in terms of a higher-order fold is irrelevant.

FOL is "Turing complete" (semidecidable) already - no need to add anything.

I'm not sure second-/higher-order logic has anything to do with higher-order functions—those "orders" are about different things.
Typed higher-order functions can be expressed using ML polymorphism. I'm no FOL expert, but I think at least in the usual foundations (FOL + set theory) they're no problem.
If you want to go beyond ML polymorphism, there's System F. Also called second order lambda calculus, and arising from second-order arithmetic minus dependent types. (Source: Proof and types, J.Y. Girard, Chapter 15. Might be one of the easiest chapters in that book to skim, still not easy).

They are the same orders. Functions are just a particular type of relation. First-order languages only allow variables to range over individuals in the domain of discourse, while second-order allows variables to range over sets of individuals, and so on. You may be able to axiomatise some higher-order function theories in a first-order logic (I'd like to see), but that is not the same thing (proof theory vs semantics): those functions are still higher-order because their arguments denote functions, which are themselves sets (of sets ...) of (tuples of) individuals.

@Neil, I disagree with all of your claims. Are you trolling?

Do you have reference? Even wikipedia (on FOL) disagrees with you.

Yes, FOL is decidable, which is why it's a Good Thing. A Turing complete system is not decidable: you might note Turing developed the abstraction precisely to arrive at an answer for the Entscheidungsproblem -- that is, a negative answer.

Codd developed the Relational Calculus, and then the Relational Algebra as 'executable' counterparts to FOL interpreted into the Relational Model.

Explain to me how you express transitive closure or an aggregate like SUM(r, a) in FOL.
Wikipedia on Transitive closure: "The transitive closure of a binary relation cannot, in general, be expressed in first-order logic (FO)."

Well, if you are going to be rude I am not going to continue debating with you. I suggest you find a better reference on the expressivity and semantics of FOL than wikipedia.

What do you mean that FOL is decidable? The question of whether a given proposition is provable is undecidable.

For the record, I was careful not to say that FOL can express transitive closure. The correct statement of TC requires expressing "the smallest set such that...". This is inherently a second-order statement, and cannot be correctly stated in FOL (or SQL). The fact that you can compute transitive closure in SQL (and Datalog) is due to the minimal model semantics of those languages: that is, a *restriction* they place on the FOL semantics to achieve decidability. This restriction doesn't make them second-order languages.

I find my understanding of relational algebra is similar to yours. Stored procedures are not part of SQL, so as far as I know there is no way to quantify over relations in SQL, so it is first order. There are recursive queries, but there can be recursive statements in FOL too I think (if you think how you can have recursion in Prolog, which does not have functions, and is first order).

Keean, you've not defined which parts of SQL you restrict yourself to. Neither have you defined which set of RA operators you count as "original". (Do you include RENAME, although Codd omitted it? Do you include relation-to-relation comparisons, like is-subset-of or is-empty? Do you include the G group-by operator? Presumably you don't include recursive CTEs?)

So I find your claims unsubstantiated so far.

Stored procedures are not part of SQL, ...

Maybe you don't use SProcs or the other procedural programming features, but if they're "not part of SQL", what are they? And why does the SQL standard spend so many pages specifying them?

For recursive CTEs, evaluating them to obtain the 'output' relation needs iterating (or recursing) the self-referencing disjunct until no further tuples are produced. That seems to me to be quantifying over that disjunct (a relation expression, so second-order quantification).

On recursion, I'm still researching Neil's (rather alarming) claims. Neil's remarks seem to be limited to a specific form of recursion (linear). And yet he also claims FOL is "Turing complete" (his scare quotes: what do they mean?).

I can't reconcile that claim: Turing complete includes expressing multiple recursion. As I understand it, you can express the Ackermann function (I mean the Peter & Robinson variant) in a Turing-complete algebra, but not in FOL.

What language are SQL stored procedures in? SQL does not define say 'Java' as part of the SQL standard. Although PSM is defined I don't know any two databases with compatible implementations, so therefore PSM seems a failed part of the standard, seeing as most of ANSI SQL is usable across multiple database.

Personally I think PSM is a mistake, as the whole point of relational algebra is to specify the operations without explicit iteration, so the database query engine can optimise the query, and is free to change the storage format based on usage statistics.

The other point is that made elsewhere that higher order logic is not the same as a higher order function. So even if we admit PSM permits higher order functions, this does not mean that SQLs relational part is based on higher order logic. As this topic was about logic, you had to pick up which definition of "higher order" was being used from the context.

What language are SQL stored procedures in?

Typically SQL or SQL/PSM, PL/SQL, etc. An SProc could be as simple as a SELECT statement(with parameters).

Although PSM is defined I don't know any two databases with compatible implementations, so therefore PSM seems a failed part of the standard, ...

PL/SQL and similar have been around for a long time. We're talking about expressive power, so it doesn't matter whether different vendors implement the standard in different ways. It takes SQL beyond FOL.

Personally I think PSM is a mistake,

I agree. I've already said as much. You go on to repeat the observations I already made.

... this does not mean that SQLs relational part is based on higher order logic.

My message specifically asked what part you define as "SQL's relational part". And what you mean by "Codd's original RA".

Relational algebra has the following operators

restrict
project
join
union
difference

The join can be a natural join or a cross-product both result in a complete algebra as far as I know. I think Codd's original relational algebra used the cross-product, not the natural join, and I prefer Codd's original formulation.

In SQL the database schema, and the relation operators (a table is also a relation) form the "relational part of SQL". So select, insert, update, delete. All of these commands operate on relations, and select also produces a relation as its result, allowing nesting of relational statements.

In general the relational part of SQL functions with relations as the first-class object, so how to iterate the collections is implicit, not explicit.

The comments about recursion have nothing to do with linear recursion. Recursion does not make a language higher-order.

However, the scare quotes around "Turing complete" were a hint that I was playing fast and loose with terminology. For a start, FOL is a logic not a computational model, so the term does not directly apply. What I meant was that the theorems of FOL are only semidecidable and so already require a Turing machine to compute. I was sloppy though, as this does not imply that FOL has the same expressive power as a universal TM, and it does not. For instance you need to add some axiom of induction (either second order or a first-order axiom schema) to FOL to represent arithmetic over the natural numbers, which famously (Gödel) makes FOL incomplete (edit: or inconsistent).

The comments about recursion have nothing to do with linear recursion. Recursion does not make a language higher-order.

Then I'm now completely bemused. I do have a question about recursion and expressivity.

Codd's RA is a set of operators over relations, designed to be 'executable'. He chose those particular operators as counterparts to the operators/quantifiers in FOL. His claim was this choice of operators made the RA 'complete' (in a certain sense); and could therefore express 'any query' (scare quotes). Furthermore, being no more expressive than FOL means that deducing answers to such queries is sound and complete (taking the facts represented in the database as axioms).

Codd explicitly made a couple of restrictions to keep query execution tractable: domains (types) must be finite; queries must be domain-independent. Domain independence means (loosely speaking) you can't ask for an absolute complement x such that NOT( P(x)), only a relative complement x such that Q(x) AND NOT( P(x)). Where P( ), Q( ) are predicates whose extension is recorded in the database.

The restriction to finite domains means (I think) the RA can't represent the Peano Naturals. So it doesn't need recursion to implement the arithmetic operators. Rather, the operators can be represented as relations over every pair of Integer values within that type. (That's very large, but not infinite.) Similar remarks for operators over the Reals, over CHAR strings (up to some large but not infinite maximum length), over dates/times, enumerated types, etc.

It is generally taken that the RA is not Turing complete (and that's deliberate to keep queries tractable). And a symptom of non-Turing completeness is it can't express recursion. Up to a point that's no restriction, because domains must be finite.

Whether or not recursion can be expressed in FOL, and whether or not it needs Turing-completeness to actually compute a result, is beside the point: the RA cannot express recursion. So if Neil's claims are correct, then RA is less expressive than FOL, and Codd's claims for "relational completeness" can only prompt the question: complete for what?

But ... databases can be infinite, in several dimensions: arbitrarily many relations; arbitrarily many attributes in those relations; and especially arbitrarily many tuples in those relations. So operators on relations can't use the trick of a finite domain. What does that affect?

Firstly, aggregate operators: we could implement those as a fold over arbitrarily many tuples. (Sometimes described as an "iterated dyadic operator".) That's second-order. But according to Neil, that's not necessary. OK how else to do it? Do we notionally have a distinct operator for each of SUM/MAX/etc for each possible attribute in each possible relation (schema) whose domain is every possible relation value for that schema?

Transitive closure similarly needs to join over arbitrarily many tuples. Recursive CTEs rely in an essential way on being able to refer to themselves by name. But the RA has no way to name queries: they're just expressions composed of operators, table names and column names. And the RA has no binding mechanism such as the lambda calculus or Combinators.

So how is Keean going to express transitive closure in Codd's "original" RA?

TC can be expressed in SQL, and without using the procedural/PSM features. (As Neil pointed out earlier, perhaps SQL cannot express generalised TC, but that's not needed for parent-child type hierarchies.)

However, the scare quotes around "Turing complete" were a hint that I was playing fast and loose with terminology. For a start, FOL is a logic not a computational model, so the term does not directly apply.

OK. The RA does have a computational model. The RA's operators are supposed to be equivalent to operators/quantifiers in FOL. But it seems FOL has an additional 'feature' to express recursion, namely name-binding for functional forms, so it can express recursion. (I think I should also point out as a good Haskell programmer it appears to have pattern matching/name binding for arguments. That's how it expresses recursive descent over the Peanos.)

I'm finding that deeply mysterious: how come it's less expressive than the lambda calculus? OK I'm making another category error: the LC is computable.

... What I meant was that the theorems of FOL are only semidecidable and so already require a Turing machine to compute. I was sloppy though, as this does not imply that FOL has the same expressive power as a universal TM, and it does not. ..

It seems to me that if we need a universal TM to compute the result of queries, tying our hands in the expressivity of queries is pointless. Perhaps there is merit in having a sound-and-complete layer embedded inside a computationally-complete layer. I see no point in constraining ourselves to Codd's "original" RA.

Note I am not arguing for the procedural features in SQL/PSM. They break all sorts of abstractions inside the RM (like set-at-a-time not row-at-a-time); they're not declarative like SELECT statements. I do see a place for the expressive power of recursive CTEs and/or generalised TC. I do see a place for Stored (and named) Procedures, providing they use only declarative statement forms.

So if Neil's claims are correct, then RA is less expressive than FOL, and Codd's claims for "relational completeness" can only prompt the question: complete for what?

RA is very much less expressive than FOL (deliberately). For instance, consider the following statements in FOL that express uncertain knowledge:

FatherOf(Mary, John) ∨ FatherOf(Mary, Peter).
∃x.FatherOf(Mary, x).

Neither of these statements can be represented in the relational model and neither can be the result of an SQL query, and yet FOL has no problem with them. A view in SQL corresponds to an implication in FOL, for example:

∀x.∀y.FatherOf(x, y) ∨ MotherOf(x, y) ⇒ ParentOf(x, y).

Roughly corresponds to the view:

CREATE VIEW parents(child, parent) AS
    (SELECT child, father AS parent FROM fathers)
    UNION
    (SELECT child, mother AS parent FROM mothers)

However, what view corresponds to the following FOL?

∀x.∀y.ParentOf(x, y) ⇒ FatherOf(x, y) ∨ MotherOf(x, y).

RA doesn't just limit FOL a little bit to gain decidability, but enormously to ensure all queries can be answered in polynomial time. There is a huge chasm of expressivity between RA and FOL. Read the extensive literature on variants of Datalog for some background.

Firstly, aggregate operators: we could implement those as a fold over arbitrarily many tuples. (Sometimes described as an "iterated dyadic operator".) That's second-order. But according to Neil, that's not necessary. OK how else to do it? Do we notionally have a distinct operator for each of SUM/MAX/etc for each possible attribute in each possible relation (schema) whose domain is every possible relation value for that schema?

Essentially, yes. You end up with something like the following:

CREATE VIEW TotalSalaryBill AS
    SELECT SUM(salary) FROM salaries;

becomes:

TotalSalaryBill(s) ⇔ Salary(John, x) ∧ Salary(Mary, y) ∧ ... ∧ s = x + y + ....

(Where + can be axiomised via the normal first-order Peano axiom schema). It's not pretty, and only works for finite domains (as in RA—otherwise you'd end up with infinite formulae), but it's a perfectly valid first-order account of SUM.

You could also fully reify the account and represent SQL relations in FOL as lists (function symbols). Something along the lines of:

salaries = Cons(Salary(John, 105000), Cons(Salary(Mary, 203500), ..., Nil)...)
∀t.sumSalaries(Nil, t) = t.
∀xs.∀s.∀t.sumSalaries(Cons(Salary(_, s), xs), t) = s + sumSalaries(xs, t).
∀s.TotalSalaryBill(s) ⇔ s = sumSalaries(salaries, 0).

This reduces the aggregate to normal recursion over first-order data structures and more accurately models the bag semantics of SQL relations, but isn't quite in the spirit of the original.

So how is Keean going to express transitive closure in Codd's "original" RA?

Original RA cannot express transitive closure, but I don't see that anyone has made such a claim.

FatherOf(Mary, John) ∨ FatherOf(Mary, Peter).

PROJECT(JOIN(FATHEROF,REL(TUP(Mary,John)TUP(Mary,Peter))),())

∃x.FatherOf(Mary, x).

PROJECT(RESTRICT(FATHEROF,EQ(child,'Mary')),())

Not SQL (because SQL does not tolerate the columnless table, which is a severe violation of relational thinking, see Andrew Warden, The Nullologist in Relationland) but very much RA, and very basic RA at that, in modern relational thinking.

The two RA expressions yield the extensions of the respective predicates

There exists a (c,f) such that f is the father of c and ((c is Mary and f is John) or (c is Mary and f is Peter))

There exists a (c,f) such that f is the father of c and c is Mary

Your RA expressions do not express the same information. In the first case we are expressing that the father of Mary is either John or Peter (or both as I haven't constrained FatherOr to be functional) but that we do not know which is the case. Likewise in the second case we are expressing that Mary has some father, but we cannot name the individual at all. RA and SQL are simply incapable of making such uncertain statements. For a good reason: once you allow disjunctive or existential conclusions then you enter a combinatorial explosion of possible models and query answering takes exponential time or worse.

In either case, if the proposition is true, then the relational query yields REL{}{TUP{}} and if the proposition is false, then the relational query yields REL{}{}.

In either case, this nilary relation has the property that we can indeed infer from it that "the father of Mary is either John or Peter (or both)" (or that it is not the case) respectively that "Mary has some father" (or that it is not the case). And in either case, if the proposition is true and the (singleton) nilary relation we get as a result reflects that, it won't be possible from the empty tuple we got to "know which is the case" (John or Peter or both) or to "name the individual at all".

(All of this is disregarding "fails to denote" cases but even then the query results should match the logical outcome, which is false.)

Let's say there are no rows at all in the FatherOf base relation. The only information you know is that either Peter or John is Mary's father. Your expression yields REL{}{} - i.e., it can conclude nothing. There are no useful queries you can ask of this system, because I can only formulate the disjunctive statement as a query or as a constraint, not as an assertion.

In FOL, I can ask (for instance) "does Mary have a father": ∃x.FatherOf(Mary, x)?. From just the disjunctive sentence and no other facts I can infer that this must be true in FOL: there is no model of FatherOf(Mary, John) ∨ FatherOf(Mary, Peter) in which Mary does not have a father.

There is an extensive literature on the expressive power of various logics, query languages and database languages. Rather than restate that literature via a tiring back and forth of comments, I'll just point you at Foundations of Databases, which does a good job of describing the various points on the spectrum of expressivity of query languages.

Which is not the case if the database relation is empty and you manifestly know there is some father. You *can* query the db and you *should* conclude from the result you get that based on the db axioms, neither Peter nor John is Mary's father, which in turn should lead you to the conclusion that it's time for a db update. Depending on the precise predicate associated with the predicate symbol FatherOf, it might be the case that your knowledge isn't sufficient to determine which update to apply (if the predicate is "f is the father of c") so then you'd have to go out and refine your knowledge of the real world before coming back to the db. (If the concerned predicate were "f may be a father of c" then your knowledge is sufficient and you should be inserting two new rows.)

∀x.∀y.ParentOf(x, y) ⇒ FatherOf(x, y) ∨ MotherOf(x, y).

No SQL view and no relational view at that can possibly "represent" that right-hand thing because views still correspond to a single predicate while that right-hand thing of yours is not a single predicate but a disjunction of two.

That is not a bug it is a feature. If you spell out that right-hand thing of yours as a *single* predicate using a *single* predicate symbol then you will inevitably find that the definition itself is entirely redundant and useless, because semantically identical to ParentOf(x,y).

Your logic formula could very well, otoh, be the definition of a database constraint on a database with three tables FatherOf etc.

It wouldn't be enough to ensure all desired integrity on that database, e.g. this constraint per se would still allow, say, certain FatherOf(x,y) where there is no corresponding ParentOf(x,y), but that's just a matter of defining the additional constraint.

Point being : your example here looks like a use case for CREATE ASSERTION, not a use case for CREATE VIEW.

The fact that SQL cannot represent uncertainty in this way is very much a limitation of SQL. It doesn't make SQL "bad": it's a perfectly reasonable trade-off. But it is still an expressive limitation.

It's getting rather unclear whether you're still trying to make a point that is relevant. If the three predicate symbols of your example are rel...s in the db then a truly relational DBMS can perfectly well express your FORALL or its equivalent NOT(EXISTS ...). If not all three predicate symbols of your example are rel...s in the db then there is simply nothing to debate. Neither SQL nor any other DML applies.

The fact that SQL cannot represent uncertainty in this way ...

You've not shown that SQL (or the RM) cannot represent that uncertainty. You've only shown that your schema cannot represent it.

I'm uncertain which particular uncertainty you're wishing to represent, but we could have a relation whose predicate is 'PossiblyFatherOf(x, y)', containing ((Mary, John), (Mary, Peter), ...). But not containing (Mary, George), because we are sure George is not Mary's father. Let's be very careful: if there are no tuples for Mary (we've tracked down John and Peter and eliminated them), that is not saying (we are sure that) Mary has no father. If you want to represent: we are sure Mary has a father, but we don't know of any possible names, you need a separate relation. And a constraint with the PossiblyFatherOf relation.

... But it is still an expressive limitation.

No I'm not seeing any limitations on expressing/representing base facts. We've been discussing limitations on what sort of conclusions can be drawn from those facts, because of the (lack of) expressive power in the RA.

It should be obvious that this isn't the same. It should be obvious that these kind of tricks could only take you so far. It should be obvious that a formalism (RA) which can answer queries in polynomial time is not as expressive as one that is only semidecidable. Apparently not. Maybe there is a world in which all of the published literature about logic and knowledge representation is wrong. A world in which pointers to (free!) comprehensive textbooks describing that literature are ignored. It appears I live in that world. All hail the all-expressive Relational Algebra!

Goodbye LtU...

Neil, I asked quite a long way back in the thread for some citations to support your claims. I know the Alice book thoroughly, so does Erwin. So I don't think citing that is helping much.

Yes the RA is not Turing-complete. Nobody is claiming it's "all-expressive". But the RA is expressive enough to capture the semantics of these 'uncertainties' you're talking about.

I think you've missed the importance of the CWA in the RM. If the FatherOf( ) relation is empty (or has no tuples for Mary), that is asserting: not(FatherOf(Mary, John)) and not(FatherOf(Mary, Peter)). So the disjunction that either of them is her father comes out false. And the formulation Erwin gave yields an empty relation (of no attributes); which asserts the same. (Some of what Alice says about the CWA I disagree with; or at least it's confusingly explained.)

Are you actually using the CWA (i.e., the assumption that there is no incomplete information) to argue that RA can represent incomplete information? You may want to think about that a bit more...

There are two minimal models of FatherOf(Mary, John) ∨ FatherOf(Mary, Peter), namely {FatherOf(Mary, John)} and {FatherOf(Mary, Peter)}. Neither of those are models of your RA "equivalent", and there is no way there can be because RA admits only a single unique minimal model, and here there are two.

If you need citations spelling out that there is a unique minimal model for relational algebra, c.f.:

1. Theorem 5.3.10 of the Alice book proves that the relational algebras and calculus are equivalent to non-recursive Datalog with negation.
2. See e.g. the end of section 2.3 of this chapter for a reference that stratified Datalog programs have a unique minimal model (non-recursive programs are trivially stratified).

There cannot be a unique minimal model for the sentence I gave you, and therefore RA cannot express it. There is no ambiguity or wiggle room here. 2 ≠ 1.

For even more background, from the Alice book that you know so well (ch.12, p.282):

Importantly, the CWA is not so simple to use in the presence of negation or disjunction. For example, suppose that a database holds {p ∨ q}. Under the CWA, then both ¬p and ¬q are inferred. But the union {p ∨ q, ¬p, ¬q} is inconsistent, which is certainly not the intended result.

Interesting! Who could have known...

There are two minimal models of FatherOf(Mary, John) ∨ FatherOf(Mary, Peter), ...

Not so much. Before you start making such claims, consider what is this disjunctive 'fact' and how you'd represent it in Datalog. Hint: you won't find it in Alice, but you should be able to find why I've put scare quotes round 'fact'. Further hint: look at extensions of Datalog such as DLV.

Or if you want to represent that disjunction directly in a relation it would have to be FatherOfOrFatherOf(Mary, John, Mary, Peter). And that admits of all sorts of other 'facts' like FatherOfOrFatherOf(Mary, Peter, Mary, John).

So we could represent the same 'fact' in differing ways. Poor schema design, because not minimal and not orthogonal. These considerations are not "tricks". And schema design is not trickery. It is a discipline of logic. We're looking for a minimalist representation that is information-equivalent (that's a long-winded way of saying normalisation).

We could represent this disjunction with a single relation FatherOf; plus a constraint it include at least one of {(Mary, John), (Mary, Peter)}. Which is what Erwin put above. All expressed within the RA. The relation without the constraint is not information-equivalent. The logician's term for that would be: wrong.

... from the Alice book that you know so well ... Who could have known...

I knew, which is why I already said:

Some of what Alice says about the CWA I disagree with; or at least it's confusingly explained.

Alice says "the CWA is not so simple to use ...". IOW: if you try to use it simplistically, you can end up with inconsistency. Perhaps it expects its readers to be smart enough to realise: then don't do that. Or perhaps the lesson is: be cautious with free stuff you get off the internet. Contrast that wikipedia on the CWA has a clearer treatment of this same example.

Again, if you're going to represent a disjunction as a single tuple like FatherOfOrFatherOf(Mary, John, Mary, Peter), then the CWA works fine: the absence of that tuple means the denial of its disjunction; which is a conjunction of denials. Now if there is a tuple in the relation like FatherOfOrFatherOf(Mary, Peter, Mary, John), we have a contradiction. Further evidence this is a poor design. And we got there purely by applying logic, as expressed in the RA.

Again, no "tricks"; nothing up my sleeve.

The howling error in that passage is: "suppose that a database holds {p V q}." No I'm not going to suppose that until I know how it holds a disjunction: If there are separate relations for holding p, q, then to "hold" the disjunction, there must be a constraint between them. Then we must take that constraint into account when applying the CWA. If held in a single relation with a disjunctive predicate, we must pay attention to whether p or q appear in other tuples in that relation. (For example if the database also holds {p V p}, again the CWA yields a contradiction. Need more contraints.)

A good demonstration for why your database should be normalised to hold only (conjunctions of) atomic facts, and not disjunctions.

This is, again, merely applied logic. No "tricks".

You seem completely unable to think outside of the relational algebra box, so I cannot see how we can possibly proceed with rational argument. Good luck counting those models.

I think the important part is that the expression "higher order" is used in two different ways:

Higher order logic
Higher order functions.

In a discussion about second order logic "going beyond" first order logic, it is clearly the first type of higher order.

As such higher order functions, recursion etc are not relevant to the original topic.

A higher order logic quantified over collections as well as individuals.

Forall X where X has four legs

Quantifies over individuals, and is first order, and is expressable in SQL.

Forall X where exists Y in X, Y has four legs.

Quantifies over collections too, and is essentially asking "find all the tables that contain a row that has the "four legs" property.

Hence my assertion that SQL is not a "higher order logic", because you cannot quantify/abstract over tables and relations. (Note even if you could do this procedurally in PSM, it does not make SQL a higher order logic, that would require these expressions being handled natively in the algebra, although with SQL syntax).

I'm not sure what decidable properties of FOL you might be talking about here.

Transitive closures can be expressed in multi-sorted FOL by quantifying over paths (that is, existentially quantifying over a sequence of individuals which are the "hops" of the path). Usually we want finite paths, so you don't lose first-orderisability doing this.

Because what's an infinite path? :)

Quantifying over paths of arbitrary length in FOL means you have to have some kind of approximation to induction, which means you'll get nonstandard first order models.

But they can be constructed.

I was being flip, but I really am curious as to what you meant by infinite path. Maybe: v1 -> v1 -> v1 -> v1 -> ... v2 ? :)

I thought the difference is like that in arithmetic. With FOL we can have a path of any finite length, and given a path of any length I can always give you back one that is longer. This is like the step in an inductive proof that given N there is always N + 1. What you cannot do in FOL is take that abstract leap to infinity, you cannot say "forall paths", you can only deal in concrete paths.

So to me an infinite path implies quantifying over paths.

Edit: unless we are talking about paths with loops in?

FOL already has trouble modeling finite paths in general, in the sense that first order semantics don't pin them down (since all finite paths is an infinite set; see Löwenheim–Skolem). I'm asking what an infinite path even is. I don't think it just means a cycle :).

In a decidable logic there would be no infinite paths/proofs? So an infinite path corresponds to the halting problem, and represents non-halting, or a proposition that can neither be proved true or proved false within the logic.

Could infinite paths/proofs be expressed in some kind of higher order notation, maybe?

If you have a countable infinity of vertices, then there are a countably infinite number of finite paths over them. If the definable subsets of the vertices are first-orderisable, then the definable finite paths are too.

Any particular finite path isn't a problem, but trying to state that a property holds for all finite paths is a problem in FOL, in the sense that you have unintended models.

There's a nice puzzle about infinite paths in systems engineering too. Strong fairness says "Every process that is infinitely often enabled should be executed infinitely often in a state where it is enabled."

Right, so I need to look infinitely into the future to decide whether I should take this transition sometime, maybe? How does that work out?

It's a nice brain teaser if you consider potential and actual infinities.

"What are infinite paths?" I knew this!

But I forgot. I once did a type-rich formalization for potentially infinite paths in PVS for my PhD studies. That turned out to be such a bad idea that, among other reasons, I never ended up with a thesis.

I forgot most of what I thought then. I remember having a constructive view on infinity then; i.e., an infinite path is a (non-existent) idealization of a finite preamble which can grow liberally through appending functions - a limit. (Though the formalization was classical.)

Let the vertices be the integers and let the arcs hop from each number that encodes a Turing machine that doesn't halt to the next largest. This is an example of an infinite path that isn't recursive.

What's the endpoint of this path? why would you call that a path?

Oops, yes, that path does not have an endpoint.

I think you can generalise the finite-dimensional hypercubes to the infinite case (the vertices V being the functions from Nat to Bool), where the order relation < is defined: f<g if g differs from f at one point n, where f(n)=False and g(n)=True. By the axiom of choice, we have the existence of a function F a subset of < where dom(F) is a subset of V containing the constant False function, ran(F) differs from dom(F) is having the constant True function instead of the constant False function, so F gives a successor relation whose startpoint is the constant False function, endpoint the constant True function and each vertex f in dom(F) is on an arc from f to F(f).

Does F count as giving an infinite path?

That works. The vertices have an additional structure in this case that allows you to take limits on a sequence of vertices. This answers my question about what the "..." might mean for paths. Thanks.

Can you clarify how you are defining TC in multisorted FOL? The non-definability of TC in FOL is provable (see e.g., this note) and I'm not quite sure I see how multisorted logics escape that.

Multi-sorted FOL doesn't escape that result. I think we just have to be careful about what "express" means, because multi-sorted FOL and SOL can state and prove all of the same facts about TC.

I'm not sure that is true. Consider this SOL formula that states that X is the transitive closure (R*) of R:

    R*(X) ≡ ψ_R(X) ∧ ∀Y(ψ_R(Y) ⇒ ∀x∀y(X(x,y) ⇒ Y(x, y)))

where

    ψ_R(X) ≡ ∀x∀y(R(x, y) ⇒ X(x, y)) ∧ ∀x∀y∀z((X(x, y) ∧ X(y, z)) ⇒ X(x, z))

(taken from Example 1.11 of the Second-Order Logic part of the Open Logic Project)

The ψ_R part defines transitivity, but you need the second clause of the definition of R* to define transitive closure. I don't see how you can state anything like that in multi sorted FOL.

You just reify relations as objects in the second sort, and have a relation R r x y that asks whether reified relation r holds for x, y. Then you quantify over objects r rather than relations in the formula for TC, etc.

The multi-sort part isn't really even that important. It's just cleaner. See ZFC, upon which all mathematics can be formalized, which is defined in one-sorted FOL.

This is the confusion I was complaining about earlier in the thread between limitation of first order semantics vs. limitations of first order logic as a deductive system.

I can see your point that there is a difference between using FOL directly and using it as a meta-language for a theory of reified relations. But I'm still not sure that this escapes the limitations.

While I can see that e.g. you can prove that every set has a transitive closure in ZFC, I'm not sure that you can actually express the transitive closure of a set in ZFC itself. From what I can tell, people seem to prove that for every set there exists a transitive closure, and then just use TC(x) to denote that object. I'd be happy to be proved wrong on that though, as it's not an area I know very well.

Likewise, I'm skeptical that you can axiomatise your R relation in FOL in the way that you want—i.e., so that the only models of R(r, x, y) are ones in which (x, y) ∈ r. Again, I'd be happy to be proved wrong as that would definitely deepen my appreciation of FOL. I'm happy to admit that we are exploring the fringes of my ignorance here. (Apologies to other LtU readers if this is not the right forum—happy to take this conversation to email if so).

so that the only models of R(r, x, y) are ones in which (x, y) ∈ r.

You certainly can't do that, per Godel's incompleteness theorem. And so there will be unintended models of your theory in FOL whereas models of SOL won't have that problem. But if you look at why that is, it's just because we require more of a model of SOL -- propositions that quantify over all relations are supposed to actually hold for all set theoretic relations in the model.

But my claim above didn't have to do with models. I claimed that we can state and prove the same propositions in FOL and SOL. By this I mean that when you can prove a SOL proposition about there existing relation R such that etc., you can prove the FOL proposition such that there exists object r such that etc.

And I also observed earlier in this thread that it's possible to interpret propositions in first order logic with second order semantics (it's particularly easy to do this with relations confined to a special second sort) and it's possible to interpret second order logic with first order semantics (Henkin models).

My point is that FOL and SOL are the same strength as deductive systems and the main differences between them arise from conventions for assigning semantics to their sentences.

Right - I understand now, and I agree. The difference is in what you can express from a a semantic point of view, not in the deductive power.

I taught FOL to AI students using Herbrand models as semantics, so with a logic programming approach. It is nice to be able to construct models, rather than reason about the class of models that provide potential interpretations. It seems to solve Hewitt's complaint about nonstandard models if you say the Herbrand model is the intended model.

Can you provide a citation for a higher order logic being the same as a higher order function? You cannot quantify over functions in first order logic, and anything with a function can be rewritten without it. It seems to me you can pass relations(functions) as arguments in first order logic, you just can't quantify over them.

As for SQL's relational part, group by, sort by and rename are all part of the subset, as are recursive queries (and therefore transitive closure). Any stored procedure that is not simply a named SQL statement is outside.

Transitive Closure is part of first order logic, as finding a proof is finding the transitive closure from A to B over axioms. For example proving a Heyting algebra is commutative using only it's axioms in first order logic. This can be solved in a pure subset of Prolog, which is first order - and Prolog doesn't even have functions, but it does support recursion.

Can you provide a citation for a higher order logic being the same as a higher order function? ... It seems to me you can pass relations(functions) as arguments in first order logic, you just can't quantify over them.

No you can't pass functions (or predicates) as arguments.

Look at the Formation Rules for Predicate calculus. Terms must be formed from function symbols applied to variables; not from variables applied to variables.

So FOL cannot have higher-order functions.

... anything with a function can be rewritten without it

Yes by turning a function into a predicate, with an extra argument representing the result. Then look at the formation rules for Formulas. A Predicate symbol (not variable) must be applied to a Term. If you've removed all the functions, then all Terms must be variables.

As for SQL's relational part, group by, sort by and rename are all part of the subset, ...

Keean, you started by saying you restrict your SQL to equivalents to the "original" RA. You listed those RA operators above. You did not include RENAME (even though I strongly suggested you should). GROUP BY was never in "original" RA. SORT BY is not and never will be in RA, because a relation is unordered. (IOW a sorted thing is not a relation.)

So I can make no sense of your earlier claim

I don't think I ever use queries that don't fit into Codd's original model of relational algebra.

.

Even if you cannot pass functions as arguments, you can pass a symbol that represents a function (as you would in Prolog), but I think this is a distraction from the core argument.

I guess I should admit that I was inaccurate when I said Codd's original RA, as I do use group by, sort by, and rename - but they are relational operators in that they operate on relations. An unordered relation can be turned into an ordered relation by adding an order column.

I am not convinced they are the same orders. I can agree they are parallel, and express the same concept of order, but in relational algebra the objects are relations and individuals, so higher order would quantify over relations not functions. In lambda calculus the objects are functions, and higher order would quantify over functions. Relations are not functions, so to say they are the same would appear to be a category error. To admit higher order functions does not make the relational algebra higher order, that would require quantifying over relations.

The original point was that SQL is not a higher order logic. To qualify as such it needs to quantify over relations which it does not. Admitting recursion and transitive closure does not make it higher order.