Questions tagged [higher-order-logic]
Questions about higher-order logic, that is logic that allows arbitrary quantification, e.g. over sets of functions.
12
questions
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 ...
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 ...
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 ...
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 ...
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$ ?
$...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...