What would be involved in moving logic beyond FOL?

Carl Hewitt has opined that first-order logic (FOL) should not be regarded as logic of choice for various people such as computer scientists (e.g., he says "First-order theories are entirely inadequate for Computer Science" in a reply to me in Mathematics self-proves its own Consistency (contra Gödel et. al.). He recommends instead his Inconsistency-Robust Logic for mathematicians, computer scientists and others.

What would it take to really change our perspective to be grounded in a logic other than FOL? I think that looking at John Corcoran's First days of a logic course provides the beginnings of an answer (the article treats Aristotelian logic rather than FOL): an alternative logic should provide a natural basis grounding all of the concepts that we expect a new student of logic to grasp, and a rival to the kind of traditional logic course based on first-order logic should be comparably good or better for building on.

What would an introductory logic course look like for, e.g., Inconsistency-Robust Logic? Would it start with Aristotelian logic or would it start with something else? What would having taken such a course be good for, as a prerequisite?

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Why?

Are you talking about the post of Hewitt that gave the following reasons for the inadequacy?

First-order theories are entirely inadequate for Computer Science because, for example:
* A first-order theory cannot axiomatize the integers up to isomorphism
* A first-order theory cannot prove that a server always responds to the requests received by the server
* The Tarskian model theory semantics of a first-order theory cannot handle inconsistency

I don't find any of those reasons compelling. For example, it seems clear to me that the important difference between first order and second order logic is in the semantics used to interpret those logics. Multi-sorted FOL is just as expressive as SOL. The differences between logics for foundational purposes seems to me more about pragmatics.

You're more knowledgeable about logic than I am, so I'm really asking about your motivations here and not just trying to argue with you.

Beyond FOL

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.

set-theory-in-sheeps'-clothing semantics

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.

Syntax and semantics

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.

Syntax and semantics

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

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

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

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

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

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

> What do you mean it doesn't have a proof theory?

You say:

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.

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

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.

ZOL?

What is wrong with zeroth order logic, assuming it can describe logics beyond first and second order, up to higher order logics? I find your paper on this subject overlapping with my own conclusions, though I got it in my own, simplified way. I found a solid groundings in representing predicates by implications and conjunctions. For example, this could be a predicate "flies-some-being-at-some-altitude":

flies -> (
    what -> living &
    altitude -> number
)


Interpretation of implications and conjunctions as function operators and type products, extends this predicate to notions of functional programming. Only, what is missing in ZOL is an apply operator.

So, for newcomers, I'd start with Aristotelian logic, then ZOL, then I would extend ZOL by the apply operator and take some ready made examples from functional languages domain. Nevertheless, I found your paper from above overly complicated for beginners, so perhaps some simplifications should be made before the final step. Or perhaps it is just about chosen examples. But take it with a reservation, as I don't have any degree beyond a high school in any science. Also, this is fairly new ground for the computer science (from industrial aspect), so what concrete tools would students have after attending the course? Although I'm working on an implementation of such a language right now, I can't promise any specific publish date, so I guess this will remain an experimental area for a while.

Intuitionistic propositional logic

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.

It seems you ask both about

It seems you ask both about moving beyond FOL, and about paraconsistent logics (of which inconsistency-robust logic is just one). Let me separate these questions.

What would having taken such a course be good for, as a prerequisite?

That question applies to any other foundation. Type theory (of which I'm a fan) seems much more established than, say, paraconsistent logics, but I'm afraid few or no CS courses use type theory, hence paraconsistent logics face a harder road. I'm curious if anybody uses type theory in place of FOL.
The main problem seems simply that type theory is non-standard, and paraconsistent logics is less standard.

You know more about type theory than I do, but just to build a self-contained argument: It seems lots more such mathematics has been rebuilt on type theory than on inconsistency-robust logics. And if you want, you can also encode non-constructive reasoning in type theory, or add non-constructive axioms if you need them. While some form of proof by contradiction is still available in constructive math, it seems to disappear in paraconsistent logics.

Also, type theory probably/arguably avoids two problems Hewitt has with set theory:
> * A first-order theory cannot axiomatize the integers up to isomorphism

You can just define integers, but higher-order axioms are no problem/

* A first-order theory cannot prove that a server always responds to the requests received by the server

Assuming that's true and a big problem, Agda has a good model of coinductive computation, though that's a more recent result. I'm not sure what Hewitt means and if it applies to type theory.

== Inconsistency ==

He recommends instead his Inconsistency-Robust Logic for mathematicians, computer scientists and others.

I also think dealing with inconsistency through some paraconsistent logics would be an interesting goal. There's some interesting research on the topic, but I'd feel more is needed. I have only seen limited examples of what paraconsistent logics can do. My supervisor Klaus Ostermann did a bit of work on their applications (http://www.informatik.uni-marburg.de/~kos/papers/aosd08.pdf, https://www.cs.cmu.edu/~ckaestne/pdf/ecoop11_ereader.pdf), and I coauthored some of that work.

Also because of that work, I've come to be skeptical of Hewitt's claims (and I'm not alone). Since I find you more credible, did you get something out of his papers? Or can we just stick to published papers on other paraconsistent logics?

Why am I skeptical? Because of that work with my supervisor, I spent some time on Hewitt's (unpublished?) papers on the topic. I gave up trying to make sense of them or trusting his unpublished claims as a logician. I didn't find errors, but I found them unconvincing. I don't want to convince anybody (I consider discussion on Hewitt's de facto banned here). But I want to learn if somebody understood his papers. Hence my question.

The interest of Hewitt's work

> 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

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.

Google+

To give him the chance to respond without moderation, I have posted a link to this story on Google+ at plus.google.com/u/0/+CStewart1970/posts/CUPTuhCUyXf.

404

Link doesn't work

It works for me...

...maybe try again?

404

Doesn't work for me, either.

The link works if you're

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

Thanks

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

a first-generation whatever-he-is...

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

Possible

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).

IMO didn't circumvent Godel in an interesting way

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.

Creeping through the back door

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

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

Ignore Carl Hewitt

Carl Hewitt is a troll (or possibly a bot trying to emulate a troll).

He posts on ltu only to advertise his own papers. If you try to engage in the subject, you get what look like automated responses of word-salad that just reiterates phrases from the paper.

On your specific question, I agree with others: as a programmer, you'd darned better have a very firm grip on FOL (and why it deliberately limits expressive power) before you go to something "beyond".

And FOL is entirely adequate for large areas of programming: the Relational Algebra is First-Order; most commercial programming is FIrst-Order.

-

- wrong memory -

Aristotelian logic "rather than" FOL?

... Aristotelian logic rather than FOL ...

Eh? Aristotelian logic is First Order (and it's not "beyond"). There's a formal translation between Aristotelian and Predicate logic. (Admittedly that wasn't figured out until well into C20th.)

By "beyond" I assume you mean Second-Order or more? Or Intuitionistic? Aristotelian logic is not that.

Perhaps by "FOL" you mean specifically First-Order Predicate Logic? (Yes that's what "FOL" is usually taken to mean. But "First-Order" doesn't exclude Aristotelian 'Term Logic'.)

Aristotelian logic is not FOL

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.

First-class-ness

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).

My logic again

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.

sorts of terms

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.

Yeah

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.

Recursion

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

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?]

Undecidable

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.

How do you tell?

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.

Halting problem?

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.

Families of binders

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.

"beyond"?

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.

A starting point

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.

Relational database query languages

moved beyond FOL in the 1980s. First, it was recognized that there were all kinds of valid queries that couldn't be expressed in FOL but still can be answered efficiently, then, a characterization was given of what would be considered a valid query, and research went after query languages that could express as many such queries as possible without being unduly inefficient or becoming inconsistent. It would have been nice if some of this work had been in SQL from the start.

As someone who did a computer science master's degree at the time and has worked in various IT-related roles ever since, I would say first-order predicate logic is vital to teach in a CS curriculum, being a prerequisite for a wide range of CS subjects and a vital tool in an IT specialist's working life, while anything beyond that will only be important in specialized subject areas and probably isn't worth teaching at the undergraduate level.

SQL

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?

SQL recursion, procedures since 1999 (at least)

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 first-order

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.

HIgher order vs higher order

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

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.

Appear to not understand FOL

@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

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

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

Transitive closure and FOL

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.

Understanding

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).

Relational/Herbrand logic

I'm not sure if it's what you are looking for, but Stanford have some courses teaching logic using (finite) Herbrand semantics rather than traditional FOL Tarskian semantics. It makes quite a nice presentation to me, so is one approach "beyond FOL". See eg Herbrand Manifesto from this set of lessons. They have a Coursera course following this approach too, IIRC.