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

157 questions
Filter by
Sorted by
Tagged with
1answer
48 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?
0answers
61 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 ...
0answers
12 views

### How to prove the existense of minimal element in any subset of positive integers?

How to prove the existense of minimal element in any subset of positive integers? Could you please recommend some approach for proving this theorem about integers? (I just don't know where to start.) ...
1answer
45 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 ...
1answer
47 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 ...
1answer
85 views

1answer
96 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$ ...
1answer
301 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 ...
0answers
77 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 ...
0answers
113 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 ...
1answer
81 views

1answer
45 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 ...
0answers
31 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 ...
0answers
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 “...
1answer
33 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 ...
2answers
30 views

0answers
131 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 ...
1answer
151 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 first-...
0answers
42 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 ...
2answers
681 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 ...
1answer
100 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$ ...
0answers
127 views

2answers
551 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 ...
0answers
116 views

### Modal logic formulation

Introduction So, I want to prove that the decisions that any being makes are either predetermined or are chosen at random - basically, disproving libertarianism. I have already formulated it using ...
1answer
1k views

### Type theory vs higher-order logic

This is a question about terminology, as I am clearly confused on the topic. The Wikipedia page on higher-order logic defines it as follows: Higher-order logic is the union of first-, second-, ...
1answer
95 views

### Classifying topos for higher order logic

Chapter X of Mac Lane and Moerdijk's Sheaves in Geometry and Logic focuses on Classifying topoi. The basic concept in the early pages is the one of geometric formula, which is by definition a first-...
1answer
42 views

### A rule in the recursive clauses governing type formation in a higher order logic

My question regards the theory of types, as augmented and formalised by Richard Montague. On page 10 of Gallin's "Intensional and Higher order modal logic" https://www.elsevier.com/books/intensional-...
1answer
65 views

### Translation of an argument in logical notation.

I have to formulate the following argument into logical notation : All accused are guilty.All who are convicted will hang.Therefore if all who are guilty are convicted then all the accused will hang. ...
1answer
345 views

### The place of lambda abstraction in internal and Mitchell-Bénabou languages

It appears that most cases of an internal language/logic/type theory of a category have an appropriate notion of implication/function types and a notion of lambda abstraction that makes use of them. ...
1answer
165 views

### Third order logic: quantifying sets of sets or relations of …?

I'm reading a book that uses first- and second-order logic. The author defines first-order logic normally, but then defines second-order logic as "quantification on relations." Almost everywhere else ...
1answer
157 views

### Is it possible to express Coq Calculus of Constructions in terms of Isabelle/HOL or vice versa?

Is it possible to express Coq Calculus of Constructions in terms of Isabelle/HOL or vice versa? If that could be done then we would be able to import Coq axioms and theorems in Isabelle/HOL. Coq has ...