Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
A higher-order logic is any logic which features higher-order predicates
One can and should probably pin it down to those logic also having quantifiers ranging over predicates.
In particular, I’m thinking of FOL systems with individual predicates expressing e.g. syntactic aspects such as rules like
Bounded(P) |- Bounded(not P)
Such a logic “features” higher order predicates, but it wouldn’t count as higher order logic just because of that.
Just to record that someone anonymously added
Higher-order logic in general could be thought of as a first order theory with dependent types. There is a type $V$ called the domain of discourse, and for each type $T$ and each term $t:T$, a dependent type $\mathcal{P}(t)$ whose terms $P(t):\mathcal{P}(t)$ are higher-order predicates depending on $t$. The system $(\mathcal{U}, V:\mathcal{U}, \mathcal{P}:\mathcal{U}\rightarrow\mathcal{U})$ consisting of the type universe $\mathcal{U}$, the domain of discourse $V$, and the power type functor $\mathcal{P}$ is a natural numbers object.
They made similar additions at predicate logic and second-order logic.
Added reference:
- Colin Rothgang, Florian Rabe, Christoph Benzmüller, Theorem Proving in Dependently-Typed Higher-Order Logic – Extended Preprint (arXiv:2305.15382)
Anonymouse
1 to 6 of 6