Skip to main content

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
2 votes
0 answers
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 ...
C D's user avatar
  • 43
2 votes
1 answer
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 ...
Link L's user avatar
  • 703
3 votes
1 answer
87 views

Proof that $x \in O \wedge y \in H_x$ is $\Pi_1^1$

I am trying to read G.E. Sacks's book on higher order recursion theory, and he has this result (where $O$ is Kleene's $O$ and $H_x$ is a hyperarithmetic set, i.e. where we have sets of the form $H_{2^...
Link L's user avatar
  • 703
1 vote
1 answer
68 views

Defining Church numerals in higher order logic.

I'm looking for some help with Exercise 5.11. in Bacon's A Philosophical Introduction to Higher-Order Logics. Construct an explicit definition of the finite Church numerals, Num$_{\sigma}$, in higher-...
C D's user avatar
  • 43
1 vote
1 answer
60 views

Combinatory Logic Problem With Partial Reductions

I'm working through Bacon's Philosophical Introduction to Higher Order Logic. I am looking for help on the following problem: Exercise 3.17 Calculate the following, assuming that $\wedge : t \to t \...
C D's user avatar
  • 43
0 votes
0 answers
55 views

Logic Puzzle: Every 2nd-order Injection has a Left Inverse

I have been stuck on this problem for a couple days. We know that every set theoretic injections have a left inverse: $$\forall x,y(f(x)=f(y)\implies x=y)$$ Iff ... $$\exists g:\text{im}(f)\to\text{...
Isaac Sechslingloff's user avatar
2 votes
1 answer
77 views

A seemingly tautological derivation

In Luo's type-theoretical semantics of natural language, he represents, for example, the verb "talk" as having this type: $talk: Human \to Prop$ Unfortunately, Luo doesn't expand much on ...
user avatar
0 votes
0 answers
25 views

About the Errors in Finite Approximation

I am reading up on finite approximation recentlyenter link description here, can someone help me explain why the author expressed the interval h as a sinusoidal function in this paper? And how did ...
Ili a's user avatar
  • 19
0 votes
1 answer
27 views

How to show that Second Order Logic is more expressive than Weak Second Order Logic

Im following the definitions from the book Mathematical Logic by Ebbinghaus. Definition of Second Order Logic Definition of Weak Second Order Logic Definition of 'Expressiveness' I'm trying to show ...
nom's user avatar
  • 579
0 votes
1 answer
62 views

Can you exhibit a 3rd-or-higher order logical formula that has no "Prenex normal form"?

The Prenex normal form is a canonical form for logical formulas in 1st & 2nd order logic. I've read that higher order logic has no such thing that can be computed. However, I'm wondering what ...
HighAsAKiteOnMath's user avatar
0 votes
0 answers
37 views

If a logic first-order one if it allows variables to range over functions?

Perhaps a stupid question but important to me: I know that a second-order logic allows predicates as variables, such as: $$\forall P. P(x) \to P(y).$$ But how about functions? For example, $$f(x) + 1 &...
yrZhang's user avatar
  • 51
1 vote
1 answer
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 ...
Zlotz's user avatar
  • 41
1 vote
1 answer
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 ...
SmileyCraft's user avatar
  • 6,797
2 votes
3 answers
117 views

Do Hindley-Milner theories have a Deduction Theorem?

Deduction Theorem: Given $\Gamma \cup \{A\} \vdash B$, we can deduce $\Gamma \vdash A \to B$ HM Counter-Example (?): Take $A$ to be $\forall f : \alpha \to \alpha, \forall x : \alpha, f(x) = f(f(f(x)))...
user1636815's user avatar
0 votes
0 answers
52 views

what is the reasoning behind $\sqrt{x^2}=\lvert x\rvert$ [duplicate]

My math teacher told us that 'The square root of a positive number is always positive' and then he gave this relation to us $\sqrt{x^2}=\lvert x\rvert$. I have been previously taught that any positive ...
Agrim Tripathi's user avatar
1 vote
0 answers
45 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 ...
Tom Hosker's user avatar
1 vote
0 answers
33 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 ...
davypough's user avatar
  • 111
0 votes
0 answers
56 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 ...
Physor's user avatar
  • 4,616
6 votes
1 answer
108 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}$-...
Noah Schweber's user avatar
1 vote
1 answer
121 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 ...
Greg Nisbet's user avatar
  • 11.8k
3 votes
1 answer
280 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$&...
cjquines's user avatar
  • 133
1 vote
1 answer
85 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> \...
mcoulont's user avatar
0 votes
2 answers
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 ...
Greg Nisbet's user avatar
  • 11.8k
0 votes
1 answer
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?
Sheikh Muhammad's user avatar
0 votes
0 answers
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 ...
al-Hwarizmi's user avatar
  • 4,310
0 votes
1 answer
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 ...
user107952's user avatar
  • 20.9k
0 votes
1 answer
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 ...
nKandel's user avatar
  • 153
3 votes
1 answer
154 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.\...
Couchy's user avatar
  • 2,720
-1 votes
1 answer
116 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 ...
Roman's user avatar
  • 533
1 vote
0 answers
134 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: ...
user65526's user avatar
  • 1,383
1 vote
3 answers
181 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+...
Gean's user avatar
  • 45
2 votes
1 answer
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$ ...
user56834's user avatar
  • 13.1k
1 vote
1 answer
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 ...
MWB's user avatar
  • 565
0 votes
0 answers
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 ...
holmes's user avatar
  • 403
2 votes
0 answers
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 ...
Zuhair's user avatar
  • 4,565
0 votes
1 answer
111 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} \...
Zuhair's user avatar
  • 4,565
1 vote
1 answer
276 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,\...
leloji6493's user avatar
1 vote
1 answer
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 ...
Marvin's user avatar
  • 151
3 votes
0 answers
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 ...
user56834's user avatar
  • 13.1k
0 votes
0 answers
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 “...
mizejonathan17's user avatar
0 votes
1 answer
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 ...
TomR's user avatar
  • 1,323
1 vote
2 answers
255 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+...
James R's user avatar
  • 113
2 votes
0 answers
108 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 ...
1103_base_6's user avatar
2 votes
3 answers
132 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 ...
H_1317's user avatar
  • 1,085
0 votes
0 answers
61 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?)...
TomR's user avatar
  • 1,323
1 vote
1 answer
484 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 ...
RyRy the Fly Guy's user avatar
1 vote
0 answers
49 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 ...
TomR's user avatar
  • 1,323
3 votes
3 answers
1k 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 ...
Ethan's user avatar
  • 5,303
1 vote
0 answers
113 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 ...
Gergely's user avatar
  • 665
2 votes
0 answers
83 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 $...
Jeremy's user avatar
  • 529