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)

Filter by
Sorted by
Tagged with
0
votes
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?
0
votes
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 ...
0
votes
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.) ...
0
votes
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 ...
0
votes
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 ...
3
votes
1answer
85 views

Is the existential quantifier commutative in intuitionistic higher order logic?

In higher order logic, one sometimes defines the existential quantifier by $$(\exists x. \phi(x)) := (\forall \rho.(\forall x.\phi(x)\to\rho)\to\rho).$$ I am having trouble proving that $$(\exists x.\...
-1
votes
1answer
72 views

How foundation of mathematics can be based on a first order logic system?

Let's assume that we have an axiomatic system that utilises the second order logic. Can this system be reformulated in terms of first order logic? I guess, it is not the case, since the second order ...
1
vote
0answers
126 views

On a definition in a proof

In https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/intensional-logic-and-twosorted-type-theory/00A76E2304DE453C11F6626B712DB662 the following proposition is presented: ...
0
votes
0answers
29 views

Can I learn and potentially make any contributions to the field of Chaos theory if I don't pursue higher education?

I am a Computer Science student right now, and I'm currently perusing my bachelors. Most of my classes are related to programming, algorithms, and logic. I have a desire to learn Chaos theory for ...
1
vote
3answers
60 views

d^2y/dy^2 expressed in t

Given that $$ x = tln(4t) $$ $$ y = t^3 + 4t^2 $$ Find $ \frac{d^2y}{dx^2} $ in terms of t For this question is it right for me to say $$ dx/dt = tln(4t)dt=1+ln(4t) $$ $$ dy/dt = t^3dt+4t^2dt = 3t^2+...
2
votes
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$ ...
1
vote
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 ...
0
votes
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 ...
1
vote
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 ...
0
votes
1answer
81 views

Would this argument support logicism?

Notice the following theory written in multi-sorted first order logic with equality and membership, with axioms of: Comprehension:$\small k=1,2,..,\omega, \omega+1,..$ $\forall x^{i_1},...,x^{i_n} \...
1
vote
1answer
105 views

Expressing binary quantifiers like 'most' and 'finitely many' in second-order logic

I'm revising for a logic exam and in one of the past papers they have a question about the formalisation of quantifiers in first and second-order logic. [In the question, the notation $\phi^{M,g,\...
1
vote
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 ...
2
votes
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 ...
0
votes
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 “...
0
votes
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 ...
1
vote
2answers
30 views

Faster Higher-Order Derivatives

so I'm taking a calc class and I got a question to calculate a derivative similar to this one: $\ln((x+1)^4(x+2)^7(x+8)^4)$. I used chain rule and power rule to find that the answer was: $\frac{15x^2+...
2
votes
0answers
72 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 ...
2
votes
3answers
83 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 ...
0
votes
0answers
42 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
votes
1answer
96 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 ...
1
vote
0answers
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 ...
3
votes
3answers
785 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 ...
1
vote
0answers
73 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 ...
2
votes
0answers
70 views

An equation involving multisets

For multisets $A, B, C, A', B', C'$, if $A \uplus B \uplus \{B \uplus C\} \uplus \{A \uplus \{C\}\}$ = $A' \uplus B' \uplus \{B' \uplus C'\} \uplus \{A' \uplus \{C'\}\}$, must $A=A',B=B',C=C'$, where $...
2
votes
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 ...
1
vote
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-...
0
votes
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 ...
13
votes
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 ...
0
votes
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$ ...
2
votes
0answers
127 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 $\...
2
votes
2answers
327 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 ...
1
vote
2answers
326 views

Paradox vs Tautology.

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 ...
2
votes
1answer
99 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 ...
4
votes
1answer
172 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 ...
3
votes
1answer
73 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 ...
1
vote
1answer
224 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&...
1
vote
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 ...
1
vote
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 ...
4
votes
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-, ...
2
votes
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-...
1
vote
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-...
1
vote
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. ...
4
votes
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. ...
1
vote
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 ...
1
vote
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 ...