Questions tagged [higher-order-logic]

Questions about higher-order logic, that is logic that allows arbitrary quantification, e.g. over sets of functions.

Filter by
Sorted by
Tagged with
2
votes
0answers
49 views

Are there any interesting terms in pure LF or $\lambda\Pi$?

In my searching, I've seen that if Church numerals are encoded in a dependently typed Lambda calculus, that we can't derive induction or that $0 \neq 1$. I know that LF and the dependently typed ...
2
votes
0answers
41 views

How can I prove impossibility of generalizing a given higher order function from pure to monadic or applicative?

There is a great divide in Haskell between pure and monadic algorithms. While the latter are indistinguishable from their usual imperative counterparts, the former can get much more magical. What this ...
4
votes
1answer
71 views

Higher order rewriting theory and critical pairs with the beta rule

In a higher-order pattern rewrite system, one specifies rewrites on beta normal forms of terms. Is it possible to have a rewrite like: $\gamma := \lambda x . F(m) \to F(\lambda x . m)$ for some ...
3
votes
1answer
154 views

Modelling using propositions, syntax and standards

One of the first programs I wrote when learning Java was a console application modelling the operation of an elevator. I'm trying to teach myself propositional logic and so I thought, why not use the ...
3
votes
2answers
202 views

Underlying language to specify various types of logic

There exist several different types of logic -- 1st order, 2nd and higher order with many different sets of inference rules possible. What I'm having trouble understanding is what's the "underlying ...