# Questions tagged [higher-order-logic]

In mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and a stronger semantics. (Def: http://en.m.wikipedia.org/wiki/Higher-order_logic)

164 questions
Filter by
Sorted by
Tagged with
33 views

### Axiomizing meets/joins of a lattice directly instead of quantifiers

The usual strategy of axiomizing logic axiomizes quantifiers first and then defines joins and meets in terms of them later. Can you reverse the order of definitions? I know various logics can be ...
1 vote
33 views

### Is there any correspondence between higher and lower order logics vs higher and lower level programming languages?

I work as a programmer, and, outside of work, I sometimes dip into mathematical logic. My intuition alerted me to some possible connections between my job and my hobby, and I thought this might be a ...
• 145
1 vote
29 views

### What Are Some Reasonable Logical Consequences of a Logical Assertion?

First off, my experience is only with some applications of logic (in linguistics and knowledge representation), as opposed to formal logical analysis. But, I'm looking for a formal answer to my ...
• 111
52 views

### what is the order of the logic and the multi-sortedness of the structures required for rigorous math in ...

Might be a not well-posed question but I hope it makes sense and can be clearly answered. Iwant to know what is the order of the logic required to work with the following areas of mathematics, to ...
• 3,854
99 views

### Comparing "local compactness numbers" of two strong logics

Given a logic $\mathcal{L}$ (together with a fixed encoding of $\mathcal{L}$-sentences by sets), let $\beta_\mathcal{L}$ be the smallest limit ordinal $\beta>\omega$ such that every $\mathcal{L}$-...
• 218k
1 vote
102 views

### Löwenheim number of the logic $\mathrm{FOL}[L]$ ($(Lx)[\varphi,\psi]$ holds iff $|\{x:\varphi\}| \ge 2^{|\{x:\psi\}|}$)

What is the Löwenheim number of the logic $\mathrm{FOL}[L]$? Let $L$ be the quantifier with the intended reading a lot more, and the semantics shown at the end of this section. $D_1$ and $D_2$ are ...
• 6,391
110 views

### λP2, the Calculus of Constructions, and quantifying over propositions

In $\lambda P2$, we can write polymorphic functions like $\Lambda A. \lambda x. x: \Pi A. A \to A$. By Curry–Howard, this corresponds to the proposition "for all propositions $A$, $A$ implies $A$&...
• 123
1 vote
67 views

• 3,539
1 vote
164 views

• 103
89 views

### Existence of first-order and higher-order bayesian probability

As normal Bayesian probability could be thought of as zeroth-order or propositional logic where the truth values are real numbers between 0 and 1 inclusive, do there exist Bayesian probability ...
• 273
102 views

### Using a proof by contradiction with unprovable statement

In a standard proof by contradiction of the statement p => q “p implies q”, we can suppose the statement is false. If we then derive an absurdity then the statement is shown to not be false, hence it ...
• 909
56 views

### Sequent calculus for classical higher order predicate logic - why not?

I read that there is sequent calculus for second order substructural predicate logic https://link.springer.com/chapter/10.1007/978-3-319-08587-6_5 and sequent calculus for second order (what it means?)...
• 1,181
175 views

### Strategies for translating statements into formal logic language

I've seen many posts asking for help translating a specific statement (posed in natural language) into a formal logic language, and the answers are typically straightforward translations without much ...
• 2,427
1 vote
41 views

### Do non-monotonicity / higher-order / probabilistics / modalities / connectives exhaust all possible features of logical reasoning?

I am searching for all the possible features of reasoning (all of them can be expressed in logic), so far I have found the following features: non-monotonicity, defeasible reasoning (expressed by ...
• 1,181
897 views

### Exists infinitely many as a numerical-quantifier

On notation, at first I just write $\exists^{!\infty}$, later I changed to $\exists^\infty$, which one should I use $?$ And I'm thinking what does this really mean in first-order-logic$\dots$ My ...
• 5,100
1 vote
90 views

### Terminal object in a Cartesian Closed Category

Pierce's Basic Category Theory for Computer Scientists writes: 1.10.2 Definition A Cartesian Closed Category (CCC) is a category with a terminal object, binary products and exponentiation. I ...
• 595
72 views

• 2,740
537 views

### If Type Theories are all Logics.

So it sounds like Higher Order Logic (HOL) and Type Theory are equivalent. Then there is Intuitionistic Logic and Intuitionistic Type Theory, but I'm not sure of the connection there. I am just ...
• 3,156
1 vote
426 views

The expression(~p or p )is a Tautology. Consider this statement(p): This statement is false. Now here, Statement p is paradoxical. My question is :- Can we define paradoxes like this as statements ...
119 views

### 'Logically symmetric' expressions in lambda calculus

A popular idea among philosophers is that facts are built out of fundamental entities in something like the way that sentences are built out of elementary expressions. My question is motivated by a ...
• 509
183 views

### How do we get the converse of extensionality in Gödel's 1931 system?

Just had a look at a transcript of Gödel's 1931, On formally undecidable propositions of Principia Mathematica here. The original is found for example here. There is a particular axiom schema V on ...
85 views

### Finite axiomatizability of theories in infinitary logic?

I know that the use of axiom schema in first-order theories can usually be eliminated by allowing higher-order quantification. So, a theory that isn’t finitely axiomatizable in a first-order language ...
• 2,377
1 vote
301 views

### Having trouble Solving fourth order heat equation.

I am facing trouble solving this higher order heat equation \partial_t u +\partial_x^4 u = 0, \space \space \space \space \space \space \space \space \space \space \space -\infty<x<\infty, t&...
• 41
1 vote
625 views

### Axioms in Gödel's ontological proof are inconsistent?

So, my problem is with Axiom 5 of the proof, where Gödel considers necessary existence as a property. However, by his own definition, a 'property' applies to objects including those whose necessary ...
• 166
1 vote