# 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)

143 questions
Filter by
Sorted by
Tagged with
61 views

34 views

### How to express ''there exists a subset $X$ of $\Delta$ which is such that at least $50$ percent of $X$ satisfy a property''

In first-order logic, we can use counting quantifier to express ''there exists at least k elements that satisfy a property '', i.e., $\exists_{\geq k} x\colon\varphi(x)$ where $k$ is a integer. For ...
27 views

### When can and when cannot a second-/higher-order formula be written as (a countable family of) first-order formulas?

Clearly, not all second-/higher-order formulas can be written as a family of first order formula's. Otherwise we could write the induction axiom for arithmetic as a set of first order formula's and ...
13 views

### Theory to Signature Mapping?

So let’s say that I have a theory T with a signature Σ. I want to make another signature Σ’. The logic behind Σ is one/non-sorted, while the logic Σ’ I want to be many-sorted. Is there any means of “...
19 views

### What can we do with nonenumerable sets of formulas (e.g. formulas of Higher order Logic)?

It is well known textbook fact, that the set of (grammatically correct) sentences/formulas of higher order logic (even of the second order logic) are not enumerable. My question is - what can we do ...
23 views

115 views

### ZFC plus HOL-Standardness

I was wondering what happens if we extend ZFC by the assumption that $U$ is a model of ZFC that is 'standard' relative to every definable higher-order theory that is categorical. Specifically: Let ...
94 views

### Weak second order Logic

I was reading the other day (Chapter 3 Introduction) , that sequential calculus is also called weak second order monadic logic with one successor or WS1S. I understand the difference between ...
39 views

### Is this kind of high order logic of individual predicates inconsistent?

Lets permit quantification over predicate symbols in formulas, so the formula formation rules would the same as those of first order logic, but with allowing quantification over predicates, and ...
531 views

### Is many sorted logic really a unifying logic?

I am reading "Extensions of First Order Logic" by Maria Manzano (1996). It develops the thesis that "[M]ost reasonable logical systems can be naturally translated into many-sorted ...
80 views

### Atomic Formulas in Second Order Logic

I'm studying second-order logic and I would like to know if the phrase about atomic formulas in Figure 1 is correct. If addition, I would like to know what means a second-order predicate like $P^n_k$ ...
117 views

### Understanding The First Axiom Of Gödel's Ontological Proof

On Wikipedia, the first Axiom of Gödel's ontological proof is $$(P(\phi)\land\square\forall x(\phi(x)\Rightarrow\psi(x)))\Rightarrow P(\psi),$$ I assume there are implicit quantifiers present for \$\...
230 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 ...
248 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 ...
91 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 ...
162 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 ...
43 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 ...