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
4 votes
1 answer
180 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 ...
Jonathan Gallagher's user avatar
3 votes
1 answer
343 views

How to understand quantifier without predication " ∀(λφ. (φ x m→ φ y))"?

I am reading about embedding/automation of modal logics in classical higher order logic (http://page.mi.fu-berlin.de/cbenzmueller/papers/C46.pdf) and Goedels proof of God's existence is prominent ...
TomR's user avatar
  • 1,381
3 votes
2 answers
226 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 ...
Opt's user avatar
  • 1,276
3 votes
1 answer
162 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 ...
DinosaurHunter's user avatar
2 votes
3 answers
135 views

Uncurrying and Polymorphism

How do we uncurry functions when they are polymorphic? For example, is it possible to uncurry the following types? If so what is the uncurried type? $\forall X. X \rightarrow int \rightarrow X$ ? $...
Ram's user avatar
  • 31
2 votes
1 answer
43 views

How would you model Rust procedural macros?

In Rust programming language one can write a compiler extension function that works on abstract syntax tree, effectively modifying source code before it gets converted into machine instructions. In ...
Andrew Butenko's user avatar
2 votes
1 answer
39 views

Why is the satisfiability of ESO formulas not equal to the satisfiability of FO formulas?

Existential second-order logic (ESO) formulas have the form $$\Phi = \exists R_1 ... \exists R_k. \phi$$ where $R_1...R_k$ are relation symbols and $\phi$ is a FO formula, which can use the relation ...
Ayrat's user avatar
  • 1,065
2 votes
0 answers
73 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 ...
Joey Eremondi's user avatar
1 vote
0 answers
27 views

Why structural rules define the "smallest relation" satisfying the rules?

I'm following a university course based on these slides, and I have a question about structural operational semantics. As you can see at page 7 (4-th slide), a structural rule is interpreted logically ...
user402843's user avatar
1 vote
0 answers
26 views

Impredicativity example in HOL

From these notes pages 37-38. In HOL, I'm giving the task of proving: $\vdash \forall x^T. \forall y^T. (=_T x^T y^T) \implies (=_T y^T x^T)$ applying forall and implication introduction and the ...
user1868607's user avatar
  • 2,194
1 vote
0 answers
90 views

Do forward chaining (Rete) business rules (Drools, ILOG) / production rules support higher order rules and compositionality?

There is this talk http://andrewcropper.com/pubs/jelia19-typed.pdf about higher order Prolog, about use of higher-order predicates (that takes other predicates as arguments) and compositionality of ...
TomR's user avatar
  • 1,381
1 vote
0 answers
57 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 ...
Ignat Insarov's user avatar