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

178 questions
Filter by
Sorted by
Tagged with
94 views

### (weak necessity) proof a collection is closed under Modus Ponens from prior assumptions

I am looking for help understanding Exercise 7.3 from A Philosophical Introduction to Higher-order Logics by Bacon. The ultimate goal of the exercise is to prove the right-to-left direction of the ...
• 43
166 views

### Help in understanding proof for: There exists recursive $f$ such that for all $e$, if $R_e$ is well-founded then $f(e) \in O$ (G.E. Sacks book)

I am trying to read G.E. Sacks's book on Higher Recursion Theory. Let: $$R_e(x,y) \iff \{e\}(x,y) \text{ is defined }$$ be the $e$th recursively enumerable binary relation. In Lemma 4.3, we have ...
• 703
87 views

• 43
55 views

• 51
1 vote
58 views

### Definition of integers in higher-order logic

There's the classical of natural numbers in higher-order logic (see the introduction of this page for example). Is there something similar for integers (elements of $\mathbb{Z}$) ? I didn't find this ...
• 41
1 vote
153 views

### Can you define a countable set containing undefinable elements?

Is it possible to construct a countable set that contains an undefinable set as an element? Consider a set $X$ to be definable if there exists a parameter-free formula $\varphi$ in the language of ZFC ...
• 6,797
117 views

• 11
142 views

### (How) do theories of higher-order arithmetic have non-$\beta$ models?

I was reading this question about $\beta$-models of $\mathsf{NFU}$ and noticed that models theories of higher-order arithmetic can be or not be $\beta$-models. My understanding is that a $\beta$-model ...
• 11.8k
154 views

### Annihilator Method. Getting wrong answer

I am doing by this method Annihilate this function: $(7x^2+5)e^{2x}.$ I am getting the answer $(D^2-2)^5$, but this doesn't annihilate the function. What am I doing wrong?
115 views

### Gödel's proof: What if all axioms of a formal system are Gödel sentences

By proof, we know that Gödel's first Theorem applies to certain formal/axiomatic system, while the unprovable statement to which Gödel refers, the so-called "Gödel Sentence", is designed to ...
• 4,310
64 views

### Are more classes of structures axiomatizable as you increase the order of the logic?

This is similar to a question I asked before, but slightly different. Is it the case that $n+1$-th order logic can axiomatize more classes of structures than $n$-th order logic? So, for example, are ...
• 20.9k
56 views

### finding the shape of the higher order equations

Is there any way to find the shape of the higher-order equation like this one? I am more interested in making an initial guess about the shape (fast prediction) and then the process to find it. Any ...
• 153
154 views

• 45
201 views

### Strongly constructive proofs: Proofs that don't make use of decidability?

I was thinking about counting argumens from the perspective of constructivist / intuitionistic logic: A typical counting argument might have the following pattern: Suppose we have a finite set $S$ ...
• 13.1k
1 vote
420 views

### Is it fair to say that ZFC axioms can not even be stated in FOL?

The separation axiom of ZFC states Suppose some set $x$ exists, and let $C$ be any condition. Then there exists a set $y$ consisting of all and only the members of $x$ that satisfy $C$. To translate ...
• 565
228 views

### Higher order arithmetic, hierarchies and proof theoretic ordinals

I would like to consider a generalization of the notation $\Pi$ and $\Sigma$ used for the arithmetical hierarchy $(\Pi^0_n$, $\Sigma^0_n)$ and the analytical hierarchy $(\Pi^1_n$, $\Sigma^1_n)$ to ...
• 403
148 views

### Can we blend logic and set theory into ONE system?

Why we cannot coin a logical system without this dicotomy of predicate and terms, that is to say a single sorted logic. So we only have term symbols that at the same time act as predicate symbols. So ...
• 4,565
111 views

1 vote
224 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 ...
• 151
34 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.1k
19 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 “...
51 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 ...
• 1,323
1 vote