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)

learn more… | top users | synonyms

1
vote
3answers
105 views

$\exists x ~ \forall y ~ f(x, y) \iff \forall y() ~ \exists x~ f(x, y(x))$ Name? Proof?

I was looking at potential theorems, and this one came up: $$\bigg(\exists x ~ \forall y ~:~ f(x, y) \bigg) \iff \bigg(\forall y() ~ \exists x ~:~ f(x, y(x))\bigg)$$ (where the second $y$ is ...
2
votes
3answers
54 views

Formulating that the universe is finite without establishing an upper limit

There is a fairly common example of a 2nd order formula that is only true in a universe with infinite domain: $$\begin{align} \exists R \quad & \forall x && \lnot xRx \\ \land ...
0
votes
1answer
40 views

Can monadic second-order logic characterize finiteness?

Is there a monadic second-order (MSO) theory, or even formula, T over some signature $\Sigma$, such that for every structure M for $\Sigma$, M satisfies T if and only if M is finite? (Note that this ...
3
votes
0answers
25 views

Extensionality of a hierarchy of functionals over $\mathbb{N}$

Let $H$ be the complete hierarchy of functionals over $\mathbb{N}$. To be precise: let the set $T$ of 'simple types' be the smallest set such that '0' $\in T$ and $(α→β) \in T$ whenever $α, β \in T$. ...
0
votes
3answers
59 views

A course on Logic.

I'm looking for a selection of books, in order to properly learn logic, starting from the most basic principles of propositional calculus and going up the ladder, up to higher order logic. My number ...
1
vote
2answers
100 views

Higher-Order Logic in ordinary Mathematics?

Do we use the language of higher-order logic in ordinary mathematics? (If yes: Can you give some examples?) Or are we always working with first-order logic? Comment: Maybe you are going to say that ...
0
votes
0answers
46 views

Calculating high order moments

All the information I can find about "higher order" moments seems to stop at Kurtosis which is only the 4th moment. What about the 5th, 6th, 7th, etc? I get that the formula is basically the same, but ...
1
vote
0answers
47 views

What logical resources does one need to distinguish $\mathbb{R}\hspace{-0.05 in}-\hspace{-0.04 in}\mathbb{Q}$ from $\mathbb{Q}$?

(I'm inspired by this question.) As a strict lower bound, having just the order relation is not enough, since $\mathbb{R}\hspace{-0.05 in}-\hspace{-0.04 in}\mathbb{Q}$ and $\mathbb{Q}$ are both ...
3
votes
1answer
132 views

How to show incompleteness of second order logic?

I'm trying to see/show that second order logic (with full semantics) is incomplete - i.e. that there are sentences that are true in all models of some theory $T$, and yet still can not be proved from ...
0
votes
2answers
94 views

Sound deductive systems with biggest set of provable sentences in second-order logic?

In second-order logic (with standard semantics), we know that there are sound deductive systems, and we know that no sound deductive system can derive all true statements. I was wondering whether ...
1
vote
1answer
61 views

Axiomatizability in monadic second-order logic

For my thesis in finite model theory I'm considering some basic classes of structures, and I want to show in which logical systems they can or cannot be axiomatized. I now consider the class ...
2
votes
1answer
90 views

Is there a 'largest' second-order categorical axiomatization of set theory, extended from ZFC2

While it's possible to obtain categorical second-order axiomatizations of set theory by extending ZFC2 with additional axioms (see [1]), these axioms seem somewhat arbitrary (e.g. adding an axiom that ...
2
votes
2answers
87 views

Are categorical second-order axiomatizations of set theory inconsistent due to the axiom of replacement

Second-order ZFC is nearly categorical, except that it does not determine the 'height' of the cumulative hierarchy (intuitively speaking). However, additional axioms can be added to second-order ZFC ...
5
votes
1answer
142 views

Is there any formula of monadic second-order logic that is only satisfied by an infinite set?

Is there any formula, of monadic second-order logic, that is only satisfied by an infinite set?
4
votes
1answer
81 views

How high up do kinds go in type theory?

I understand this is a bit naive, but I just learned how types can have types that we call 'kinds,' in system F$\omega$ as a sort of extended higher order lambda calculus. The wiki article on it ...
2
votes
1answer
133 views

Do I really need lambda abstraction for type theory?

So I think I somewhat understand the type theory of the various lambda calculi in the lambda cube, from the simply typed lambda calculus to the calculus of constructions, but looking at it I'm ...
0
votes
0answers
48 views

How do we express higher arity predicates and functions in terms of membership?

It's been noted by others that higher order logic is similar to set theory. We can express the second order statement $\forall$R$\forall$x(R(x)) as a first order statement $\forall$R$\forall$x (x ...
2
votes
0answers
37 views

What strongly normalizing lambda calculi exist that can be integrated with/as logic?

If I'm trying to implement a logical system for deduction based on propositional reasoning, I can start with predicates and quantifiers and functions to obtain first order logic. I can further extend ...
1
vote
2answers
163 views

What does a prime (apostrophe) mean before a predicate?

I found this statement in a paper by John McCarthy: $$ \forall x.ostrich\ x \supset species\ x ={}^\prime{}ostrich $$ I can't figure out what the prime indicates.
5
votes
1answer
87 views

Is there a syntax for type quantification in higher order logic?

I'm trying to understand higher order logic deduction, and I sort of understand how after going to third order logic and higher you have a type explosion; predicates and functions can have a large ...
0
votes
0answers
61 views

Are proofs for many-sorted first order logic shorter than single sorted first order logic?

I understand that the expressive power of first order logic with one sort is the same as any many sorted first order logic, and that higher order logic with general semantics is the same as a many ...
6
votes
4answers
507 views

Why aren't valid higher order logic sentences recursively enumerable in full semantics?

It's said (proven in some reduction to the Gödel–Rosser theorem?) that second order logic and higher fails to be complete for full semantics; that is there isn't any semi-algorithm for determining if ...
1
vote
2answers
101 views

For which subsystems T of 2nd order arithmetic is there a model of T + $\neg$Con(T)?

A theory T might have the following property: there is a model of T + $\neg$Con(T) 1st order PA has this property, but full 2nd order PA doesn't. Among subsystems of 2nd order arithmetic, which ones ...
6
votes
2answers
219 views

Defining addition in second order logic

(before saying it's duplicate, read whole question) I was told by someone that we can define addition and multiplication purely in terms of successor function, provided that we work in second order ...
1
vote
0answers
69 views

If full semantics higher order logic is set theory, which set theory is it?

I've been trying to get a handle on how higher order logic interacts with set theory. It's been stated convincingly that higher order logic with full semantics is set theory in sheep's clothing. For ...
2
votes
1answer
68 views

Flattening quantification over relations

I already asked this question in stack overflow here and somebody suggested to post it here. I repeat the question again: I have a Relation f defined as $f: A \to B × C$. I would like to write a ...
1
vote
1answer
121 views

What syntax exists for higher order logic?

I know this is sort of a broad question, but I'm having trouble getting a handle on the syntax for higher order logic, when going from first order logic. Basically I want to be able to do resolution ...
2
votes
1answer
99 views

How is quantifier elimination accomplished in second and higher order logic?

In first order logic we can eliminate existential quantifiers using a second order equivalence relation: $\forall$x$\exists$y P(x, y) $\iff$ $\exists$f$\forall$x P(x, f(x)) Dropping the existential ...
4
votes
2answers
901 views

What are some examples of third, fourth, or fifth order logic sentences?

I know this seems like an obvious question, but I haven't been able to find any examples of sentences in logic higher than second order, so my intuition on how it's supposed to behave is failing me. ...
1
vote
1answer
38 views

higher order ODE convert problem

I have $$y'''- 3\,y'- x\,y = 0.$$ How to convert this to three first order differential equations? I got stuck for using Let $z=y''$
0
votes
1answer
620 views

Can somebody please help me with math problems for 8th grade?

1) Determine if the following statement is true or false. If false, provide a counterexample: "An equation with an integer coefficient will always have an integer solution.". 2) Write a rel-world ...
1
vote
0answers
55 views

Characterizability in $L^2_{\kappa^+\omega}$

I'm reading an article on second order characterizability. At some point in the article it proves that any model $A$ of cardinality $\kappa$ must be characterizable in $L^2_{\kappa^+\omega}$. I.e. ...
2
votes
0answers
122 views

Can “tit for tat” strategy be defined in monadic second-order logic?

Prisoner's dilema game can be represented as a game tree, which could be infinite game with corresponding infinite game (binary) tree in common case. There is well-known tit for tat strategy, which ...
12
votes
2answers
1k views

What's an example of a theory that's consistent yet has no model?

By the completeness theorem for first order logic, if a theory is consistent then it has a model. But what's a counterexample to this : what's an example of a logic where some theory is consistent ...
3
votes
2answers
141 views

Is the first-order incompleteness of a theory (like arithmetics, set theory or logic itself) avoidable in a second or higher-order axiomatizations?

Can we avoid the first-order incompleteness of a theory (like arithmetics or set theory) in a second-order theory which contains the previous? How does it depend on the chosen semantics or models? If ...
1
vote
1answer
52 views

Second order universal quantifier elimination restriction

Dirk van Dalen in his Logic and Structure gives following universal elimination rule: from $\forall_{X^n} \phi$ infer $\phi^*$ where $\phi^*$ is $\phi$ in which every occurence of $X^n(t_1, ..., ...
0
votes
1answer
80 views

What is the difference between logical and iterative set

Saphiro in his "foundations without foundationalism: a case for second-order logic" defends second-order logic by claiming that talking about subsets of domain is not problematic in case of SOL. He ...
0
votes
1answer
110 views

Logic question in Real Analysis

I thought about posting some minor insecurities and some main doubts i have on a particular topic. Let R with the usual metric be a metric space, $A \subseteq R$ , $f:A\to R$ and p is a limit ...
3
votes
2answers
125 views

Are higher order logics substantially stronger than second order

Do we get much by using logics of order higher that 2? Does each transition to next level provides much power?
0
votes
1answer
99 views

Proving property for all predicates in first order logic

Let's consider language with predicate $P$ and following derivation $${{{[P[a/x]]^1} \over {P[a/x] \rightarrow P[a/x]}}\rightarrow I^1 \over {\forall_x (P(x) \rightarrow P(x))}}\forall I$$ Doesn't ...
3
votes
1answer
103 views

Completness in higher order logic and Interpretations

It´s known that for first order theories, it holds $\mathbf{ZFC} \vdash T \vdash \varphi \leftrightarrow T \models \varphi$. Why does this not hold in the higher order case (any simple example?)? ...
1
vote
2answers
116 views

Is it possible to prove that the encoding of existentials in System F is valid?

In Girard's Proofs and Types, under item 11.3.5, second-order existential quantification is encoded in System F using universal quantification as follows: $$ \Sigma X.V \equiv \Pi Y. (\Pi X.(V \to ...
2
votes
2answers
143 views

Types versus kinds and sorts

In the context of logic, especially Higher‑Order‑Logic and Calculus‑of‑Construction, what is a kind and how does it relates to and differs from a type? My raw guess if that a kind is the higher level ...
6
votes
4answers
249 views

Why aren't there any first-order sentences which have the property of being true in all non-standard models of PA and false in the standard one?

I'd like to know where the following result comes from (that is, whether there is a more general result from which it follows or else how it can be proven): There is no first-order sentence which is ...
2
votes
0answers
87 views

A consistent first-order theory whose impredicative second-order variant is inconsistent

Let's assume that we have a consistent first-order theory, which was derived from a second order theory by replacing universal quantification over second order variables by axiom schemes for ...
1
vote
2answers
315 views

annihilator method confusion

I have a final in the morning and I am extremely confused on the annihilator method. I have been googling different explanations all night and I just dont get it at all. I am looking at an example: ...
3
votes
1answer
109 views

Does second-order arithmetic (Z2) prove soundness and uniform reflection for first-order arithmetic (PA)?

(1) Does full second-order arithmetic (Z2) prove soundness and uniform reflection schemas for first-order arithmetic (PA)? That is, do we have for all formulas $\phi$: $$ \underset \phi \forall \; ...
7
votes
2answers
319 views

There is a second-order sentence that is valid in standard semantics but not valid in Henkin semantics?

Let $\Sigma^\mathrm{ST}$ be a set of sentences that is valid in standard semantics and $\Sigma^\mathrm{Henk}$ be a set of sentences that is valid in Henkin semantics. Since ...
1
vote
0answers
47 views

How is it possible that the well-ordering theorem is strictly stronger than the axiom of choice in second-order logic? [duplicate]

If I am not wrong, the well-ordering theorem is strictly stronger than the axiom of choice in second-order logic. I am not sure to understand how this is possible. The reason is that second order ...
6
votes
1answer
318 views

Why is better to work with first-order Peano's axioms than with second-order Peano's axioms?

In the case of Peano's axioms the second-order version is categorical, but the first-order is not. Besides, with the second-order version the operations: addition, multiplication and exponentiation ...