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
0 answers
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 ...
user avatar
1 vote
0 answers
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 ...
user avatar
1 vote
0 answers
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 ...
user avatar
  • 111
0 votes
0 answers
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 ...
user avatar
  • 3,854
6 votes
1 answer
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}$-...
user avatar
1 vote
1 answer
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 ...
user avatar
  • 6,391
2 votes
1 answer
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$&...
user avatar
  • 123
1 vote
1 answer
67 views

A "set" containing objects of diffrent types in higher order logic

In higher order logic, we can model a set as a function whose images lie in the type of propositions. For example, the singleton $\{0\}$ can be modeled as the function $f: <type\ of\ 0> \...
user avatar
0 votes
2 answers
93 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 ...
user avatar
  • 6,391
0 votes
1 answer
70 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?
user avatar
0 votes
0 answers
86 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 ...
user avatar
  • 3,746
0 votes
1 answer
51 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 ...
user avatar
  • 13.2k
0 votes
1 answer
53 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 ...
user avatar
  • 153
3 votes
1 answer
104 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.\...
user avatar
  • 2,544
-1 votes
1 answer
93 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 ...
user avatar
  • 453
1 vote
0 answers
129 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: ...
user avatar
  • 1,363
1 vote
3 answers
90 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+...
user avatar
  • 35
2 votes
1 answer
114 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$ ...
user avatar
  • 11.8k
1 vote
1 answer
337 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 ...
user avatar
  • 555
0 votes
0 answers
130 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 ...
user avatar
  • 341
2 votes
0 answers
126 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 ...
user avatar
  • 3,539
0 votes
1 answer
91 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} \...
user avatar
  • 3,539
1 vote
1 answer
164 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,\...
user avatar
1 vote
1 answer
79 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 ...
user avatar
  • 141
2 votes
0 answers
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 ...
user avatar
  • 11.8k
0 votes
0 answers
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 “...
user avatar
0 votes
1 answer
40 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 ...
user avatar
  • 1,181
1 vote
2 answers
51 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+...
user avatar
  • 103
2 votes
0 answers
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 ...
user avatar
2 votes
3 answers
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 ...
user avatar
  • 909
0 votes
0 answers
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?)...
user avatar
  • 1,181
0 votes
1 answer
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 ...
user avatar
1 vote
0 answers
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 ...
user avatar
  • 1,181
3 votes
3 answers
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 ...
user avatar
  • 5,100
1 vote
0 answers
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 ...
user avatar
  • 595
2 votes
0 answers
72 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 $...
user avatar
  • 509
0 votes
0 answers
156 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 ...
user avatar
  • 53.2k
1 vote
1 answer
208 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-...
user avatar
0 votes
0 answers
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 ...
user avatar
  • 3,539
13 votes
2 answers
842 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 ...
user avatar
0 votes
1 answer
118 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$ ...
user avatar
2 votes
0 answers
132 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 $\...
user avatar
  • 2,740
3 votes
2 answers
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 ...
user avatar
  • 3,156
1 vote
2 answers
426 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 ...
user avatar
3 votes
1 answer
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 ...
user avatar
  • 509
4 votes
1 answer
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 ...
user avatar
3 votes
1 answer
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 ...
user avatar
  • 2,377
1 vote
1 answer
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&...
user avatar
  • 41
1 vote
2 answers
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 ...
user avatar
  • 166
1 vote
0 answers
119 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 ...
user avatar
  • 166