<p>An actual second-order logic programming language would allow you to use <strong>second-order quantifiers</strong> in a computationally meaningful way. Second-order logic without quantifiers ranging over second-order symbols is conservative over first-order logic (if I remember correctly, someone please correct me if I am wrong).</p>
<p>HiLog seems to be an old language, which to me it just looks like a precursor of <a href="https://en.wikipedia.org/wiki/%CE%9BProlog" rel="nofollow noreferrer">λ-prolog</a>, a modern way of adding higher-order features to prolog. I wouldn't spend too much time worrying about what someone thought about its semantics in 1989.</p>

CC BY-SA 4.0
2024-04-01T20:44:17.587Z
Logic programming is not really logic: https://math.stackexchange.com/questions/3894192/ . This is why I find appeals to properties of various logics rather unconvincing (and, but this is my fault, occasionally incomprehensible, as I never studied SOL). I'm hoping to see answers that illustrate what's missing in HiLog, from the programming language perspective.
MWB
CC BY-SA 4.0
2024-04-01T20:53:59.503Z
Haskell/Lisp/Scheme/ML let you define a `map` function over singly-linked lists. Is `maplist` in the question more limited in any way, and if so, how? Is there anything else that's conveniently done in functional programming languages, but cannot be done in HiLog?
MWB
CC BY-SA 4.0
2024-04-03T23:33:15.703Z
You have never studied second-order logic, and you're asking about it on a forum that is meant to be for research-level questions? I think your question is better suited for cs.stackexchange.com.
Andrej Bauer
CC BY-SA 4.0
2024-04-04T06:46:36.947Z
*"a precursor of λ-prolog"* λ-prolog predates HiLog by 2 years.
MWB
CC BY-SA 4.0
2024-04-04T16:23:50.820Z
*"allow you to use second-order quantifiers in a computationally meaningful way."* But HiLog allows you to use second-order quantifiers, and it's computationally meaningful (no other way to define `maplist` in pure Prolog)
MWB
CC BY-SA 4.0
2024-04-04T20:52:47.370Z
Where is `maplist` using a second-order `∀` or `∃`?
Andrej Bauer
CC BY-SA 4.0
2024-04-04T21:16:36.077Z
On the second line, `F` is a predicate, because it's used in `F(X, Y)`, and `∀F` is implied, because `F` is a variable.
MWB
CC BY-SA 4.0
2024-04-04T22:13:15.800Z
An outer universal quantifier is not an essential use because (if I remember my logic correctly), so long as you only have ∀'s on the outside, that's going to be conservative over first-order logic. An *essential* use would occur if you had ∀ nested somewhere inside a formula, and in particular to the left of an implication.
Andrej Bauer
CC BY-SA 4.0
2024-04-07T13:17:45.833Z
It's not clear to me which contexts the $\forall^2$ may actually be used, but if as @AndrejBauer says it is really just on the outside of everything then of course this is conservative over pure FOL. On the other hand, it binds variables in definitions of closed types which may themselves bes used in further definitions (etc.) then one should obtain all the finitely iterated inductive definitions (and not more). This is still far beneath full second-order logic.
Anupam Das
CC BY-SA 4.0
2024-04-07T16:30:59.417Z
+50 - the best answer so far!
MWB
CC BY-SA 4.0
2024-04-07T22:09:18.727Z
@AnupamDas I think you are thinking about descriptive complexity over finite structures. Logic Programming is more like resolution refutation proof/witness search I think, in first order theory. From the perspective of its computational power it is Turning complete.
Kaveh
CC BY-SA 4.0
2024-04-07T22:23:05.080Z
@Kaveh: yeah. I've been thinking how to improve the answer by inventing a computationally meaningful second-order quantifer for logic programming (that isn't monadic second-order), and anything I can think of is completely off the scale.
Andrej Bauer
CC BY-SA 4.0
2024-04-08T16:48:37.110Z
@AndrejBauer that is a very interesting idea. The witness in logic programming needs to be a finite object (like proofs are). We cannot represent an arbitrary infinite set, so we need to think about representations. what properties one would want from a useful representation, I don't know. Maybe computable membership plus a proof that it is actually a witness in some theory? I guess that depends on what one wants to achieve, since programming cannot go over Turning complete and Prolog is already Turning compete. ease of programming and expressiveness?provablity of statements about programs?...
Kaveh
CC BY-SA 4.0
2024-03-31T22:03:56.930Z
2024-03-31T22:03:56.930Z
Andrej Bauer
<p><a href="https://en.wikipedia.org/wiki/HiLog" rel="nofollow noreferrer">HiLog</a> is described as a logic programming language with higher-order syntax, but first-order model theory.</p>
<p>For example, it allows you to define a map over lists:</p>
<pre><code>maplist(F)([],[]).
maplist(F)([X|R],[Y|Z]) &lt;- F(X,Y), maplist(F)(R,Z).
</code></pre>
<p>On the second line, <code>F</code> is a predicate, because it's used in <code>F(X, Y)</code>, and <code>∀F</code> is implied, because <code>F</code> is capitalized.</p>
<p>I'm trying to develop an intuition for what's <em>missing</em> here. What would an actual second-order logic programming language let me do that HiLog does not?</p>
<p>It's worth noting that the limitations of first-order logic do not necessarily apply to first-order logic programming languages. For example, <a href="https://math.stackexchange.com/questions/3894192/">Prolog can express the <code>ancestor</code> relation easily, while it's impossible in the standard first-order logic</a>.</p>
<p>This question is about the limitations of HiLog, as a programming language.</p>

CC BY-SA 4.0
2024-03-30T17:54:43.057Z
the easiest way to see the difference between Second Order logic and First Order logic (like set theory) is that in the SO the second sort is semantically required to be really subsets of the first sort, and all of them; where in FO that is not true. E.g. in FO there is no way to define the set of natural numbers N, as there are always nonstandard models. In SO, it is easy to define N and the minimal inductive set. In FO this doesn't hold since the second sort might be interpreted to in nonstandard ways.
Kaveh
CC BY-SA 4.0
2024-03-30T17:55:28.567Z
See also https://en.wikipedia.org/wiki/System_F
Kaveh
CC BY-SA 4.0
2024-03-31T15:24:58.123Z
@Kaveh It's my understanding that ZFC axioms are FO. If you add them, this lets you express all (or almost all?) of mathematics (Not really my area of expertise)
MWB
CC BY-SA 4.0
2024-03-31T18:47:07.253Z
ZFC has nonstandard models, the set of natural numbers N is not definable in ZFC. Any formula you use to define natural numbers in ZFC will have models which contains nonstandard members that are not in N. You even have countable models for ZFC. In SO because the quantifier for the second order must be the actual power set of N, you can define N.
Kaveh
CC BY-SA 4.0
2024-03-31T21:57:43.287Z
@Kaveh: **Some people** "require" SO semantics to be a certain thing, but SO kicks & screams and wants to be freed. Henkin understood that, and so do categorical logicians.
Andrej Bauer
CC BY-SA 4.0
2024-03-31T23:17:36.370Z
@AndrejBauer yes, and some people say that Henkin semantics is just first order logic with two sorts.
Kaveh
CC BY-SA 4.0
2024-04-01T13:47:09.750Z
Can yo umake that a bit more precise? Will there be explicit coercions from sorts to formulas?
Andrej Bauer
CC BY-SA 4.0
2024-04-01T15:31:36.960Z
@AndrejBauer the languages and formulas are essentially the same. model theoretically, any model of the Henkin semantic second order theory is a model of the two sorted first order theory. So one needs to restrict the space if possible models somehow to get something other than two sorted first order theory with the same axioms. If one doesn't, it is essentially just first order logic. Of course, proof theoretically, imposing the second sort to be the actual powerset of the first sort is not very interesting, but model theoretically, it is interesting.
Kaveh
CC BY-SA 4.0
2024-04-01T19:59:20.723Z
Ok, I see I have to do it myself. So the two sorts would be $I$ (for individuals) and $S$ (for sets), with a binary relation symbol $E$ ("membership") relating $I$'s to $S$'s. We would probably throw in extensionality and other bits and pieces of "set theory". Is that what you have in mind? Do you know of a precise account of this sort of thing?
Andrej Bauer
CC BY-SA 4.0
2024-04-02T13:56:35.377Z
Simpson's Subsystems of Second Order Arithmetic studies various set existence axioms for the second sort required to prove various mathematical theorems.
Kaveh
CC BY-SA 4.0
2024-04-03T23:32:21.240Z
So what prevents me from defining full second-order logic as a first-order logic with two sorts?
Andrej Bauer
CC BY-SA 4.0
2024-04-05T00:43:46.523Z
it is a semantic restriction on models that cannot be expressed within the language of the first order logic. Definability of N is a good example. There is no set of axioms (even non-computable) that can prevent non-standard models of first order logic (by Henkin construction through compactness).
Kaveh
CC BY-SA 4.0
2024-04-05T00:53:25.167Z
to go beyond first order logic, one needs to violate one of the conditions of [Lindstrom Theorem](https://en.wikipedia.org/wiki/Lindstr%C3%B6m%27s_theorem). Henkin semantics SOL does not, so it is essentially just FOL.
Kaveh
CC BY-SA 4.0
2024-04-05T00:59:48.187Z
https://en.wikipedia.org/wiki/Higher-order_logic
Kaveh
<lo.logic><pl.programming-languages><first-order-logic><model-theory><logic-programming>
In logic programming, what would a language with second-order model theory gain?
MWB
# In logic programming, what would a language with second-order model theory gain?

(Asked by: username_0 on 2024-03-27)

HiLog is described as a logic programming language with higher-order syntax, but first-order model theory.
For example, it allows you to define a map over lists:
maplist(F)([],[]).
maplist(F)([X|R],[Y|Z]) <- F(X,Y), maplist(F)(R,Z).

On the second line, F is a predicate, because it's used in F(X, Y), and ∀F is implied, because F is capitalized.
I'm trying to develop an intuition for what's missing here. What would an actual second-order logic programming language let me do that HiLog does not?
It's worth noting that the limitations of first-order logic do not necessarily apply to first-order logic programming languages. For example, Prolog can express the ancestor relation easily, while it's impossible in the standard first-order logic.
This question is about the limitations of HiLog, as a programming language.

**Tags:** lo.logic, pl.programming-languages, first-order-logic, model-theory, logic-programming

> **Comments:**
> **username_1**: the easiest way to see the difference between Second Order logic and First Order logic (like set theory) is that in the SO the second sort is semantically required to be really subsets of the first sort, and all of them; where in FO that is not true. E.g. in FO there is no way to define the set of natural numbers N, as there are always nonstandard models. In SO, it is easy to define N and the minimal inductive set. In FO this doesn't hold since the second sort might be interpreted to in nonstandard ways.  
> **username_1**: See also https://en.wikipedia.org/wiki/System_F  
> **username_0**: @username_1 It's my understanding that ZFC axioms are FO. If you add them, this lets you express all (or almost all?) of mathematics (Not really my area of expertise)  
> **username_1**: ZFC has nonstandard models, the set of natural numbers N is not definable in ZFC. Any formula you use to define natural numbers in ZFC will have models which contains nonstandard members that are not in N. You even have countable models for ZFC. In SO because the quantifier for the second order must be the actual power set of N, you can define N.  
> **username_2**: @username_1: **Some people** "require" SO semantics to be a certain thing, but SO kicks & screams and wants to be freed. Henkin understood that, and so do categorical logicians.  
> **username_1**: @AndrejBauer yes, and some people say that Henkin semantics is just first order logic with two sorts.  
> **username_2**: Can yo umake that a bit more precise? Will there be explicit coercions from sorts to formulas?  
> **username_1**: @AndrejBauer the languages and formulas are essentially the same. model theoretically, any model of the Henkin semantic second order theory is a model of the two sorted first order theory. So one needs to restrict the space if possible models somehow to get something other than two sorted first order theory with the same axioms. If one doesn't, it is essentially just first order logic. Of course, proof theoretically, imposing the second sort to be the actual powerset of the first sort is not very interesting, but model theoretically, it is interesting.  
> **username_2**: Ok, I see I have to do it myself. So the two sorts would be $I$ (for individuals) and $S$ (for sets), with a binary relation symbol $E$ ("membership") relating $I$'s to $S$'s. We would probably throw in extensionality and other bits and pieces of "set theory". Is that what you have in mind? Do you know of a precise account of this sort of thing?  
> **username_1**: Simpson's Subsystems of Second Order Arithmetic studies various set existence axioms for the second sort required to prove various mathematical theorems.  
> **username_2**: So what prevents me from defining full second-order logic as a first-order logic with two sorts?  
> **username_1**: it is a semantic restriction on models that cannot be expressed within the language of the first order logic. Definability of N is a good example. There is no set of axioms (even non-computable) that can prevent non-standard models of first order logic (by Henkin construction through compactness).  
> **username_1**: to go beyond first order logic, one needs to violate one of the conditions of [Lindstrom Theorem](https://en.wikipedia.org/wiki/Lindstr%C3%B6m%27s_theorem). Henkin semantics SOL does not, so it is essentially just FOL.  
> **username_1**: https://en.wikipedia.org/wiki/Higher-order_logic  

---

## 1 answers

### Answer by username_2 on 2024-03-31. Score: 3

An actual second-order logic programming language would allow you to use **second-order quantifiers** in a computationally meaningful way. Second-order logic without quantifiers ranging over second-order symbols is conservative over first-order logic (if I remember correctly, someone please correct me if I am wrong).

HiLog seems to be an old language, which to me it just looks like a precursor of [λ-prolog](https://en.wikipedia.org/wiki/%CE%9BProlog), a modern way of adding higher-order features to prolog. I wouldn't spend too much time worrying about what someone thought about its semantics in 1989.

> **Comments:**
> **username_0**: Logic programming is not really logic: https://math.stackexchange.com/questions/3894192/ . This is why I find appeals to properties of various logics rather unconvincing (and, but this is my fault, occasionally incomprehensible, as I never studied SOL). I'm hoping to see answers that illustrate what's missing in HiLog, from the programming language perspective.  
> **username_0**: Haskell/Lisp/Scheme/ML let you define a `map` function over singly-linked lists. Is `maplist` in the question more limited in any way, and if so, how? Is there anything else that's conveniently done in functional programming languages, but cannot be done in HiLog?  
> **username_2**: You have never studied second-order logic, and you're asking about it on a forum that is meant to be for research-level questions? I think your question is better suited for cs.stackexchange.com.  
> **username_0**: *"a precursor of λ-prolog"* λ-prolog predates HiLog by 2 years.  
> **username_0**: *"allow you to use second-order quantifiers in a computationally meaningful way."* But HiLog allows you to use second-order quantifiers, and it's computationally meaningful (no other way to define `maplist` in pure Prolog)  
> **username_2**: Where is `maplist` using a second-order `∀` or `∃`?  
> **username_0**: On the second line, `F` is a predicate, because it's used in `F(X, Y)`, and `∀F` is implied, because `F` is a variable.  
> **username_2**: An outer universal quantifier is not an essential use because (if I remember my logic correctly), so long as you only have ∀'s on the outside, that's going to be conservative over first-order logic. An *essential* use would occur if you had ∀ nested somewhere inside a formula, and in particular to the left of an implication.  
> **username_3**: It's not clear to me which contexts the $\forall^2$ may actually be used, but if as @AndrejBauer says it is really just on the outside of everything then of course this is conservative over pure FOL. On the other hand, it binds variables in definitions of closed types which may themselves bes used in further definitions (etc.) then one should obtain all the finitely iterated inductive definitions (and not more). This is still far beneath full second-order logic.  
> **username_0**: +50 - the best answer so far!  
> **username_1**: @AnupamDas I think you are thinking about descriptive complexity over finite structures. Logic Programming is more like resolution refutation proof/witness search I think, in first order theory. From the perspective of its computational power it is Turning complete.  
> **username_2**: @username_1: yeah. I've been thinking how to improve the answer by inventing a computationally meaningful second-order quantifer for logic programming (that isn't monadic second-order), and anything I can think of is completely off the scale.  
> **username_1**: @AndrejBauer that is a very interesting idea. The witness in logic programming needs to be a finite object (like proofs are). We cannot represent an arbitrary infinite set, so we need to think about representations. what properties one would want from a useful representation, I don't know. Maybe computable membership plus a proof that it is actually a witness in some theory? I guess that depends on what one wants to achieve, since programming cannot go over Turning complete and Prolog is already Turning compete. ease of programming and expressiveness?provablity of statements about programs?...  

---

